AutoSamplingTheory.SALD.cycle17FirstAppendixMiddleAuditContract

Data definition / provenance and workflow record

Meaning and type

The result has data type AutoSamplingTheory.SALD.FirstAppendixMiddleAuditContract. A value of this type stores descriptions; it is not a proof of the statements in those descriptions.

def cycle17FirstAppendixMiddleAuditContract :
    FirstAppendixMiddleAuditContract

Construction and field-by-field explanation

Construct a data record from explicit fields and the audited defaults shown below.

This Lean definition constructs provenance or workflow data. It does not prove the mathematical statements stored as text. Status labels, named dependencies and citations are data, not compilation, proof or source certificates.

sourceIndexPath : String (explicit)

Descriptive text even when field names say formula, theorem, inequality, derivative, source gap, or proof.

research-wiki/source-index/SALD_original.jsonl

focusLabels : List String (explicit)

Ordered descriptive/naming checklist, not logical conjunction or compiler dependency list.

Ordered data items

1. lem:gronwall
2. lem:dv_variation
3. def:PI
4. eq:LSI-KL-FI

sourceReadWindows : List String (explicit)

Ordered descriptive/naming checklist, not logical conjunction or compiler dependency list.

Ordered data items

1. appendix.tex:47-71: Gronwall statement, integrating-factor derivative, integration from 0 to t1, and exponent rewrite at lines 63-69.
2. appendix.tex:73-79: Donsker--Varadhan variational formula cited from Boucheron Cor. 4.15 with finite log-mgf tests.
3. appendix.tex:86-94 plus appendix.tex:96-151: PI definition and the downstream Sobolev/Riesz velocity-norm route.
4. main_body.tex:202-215: LSI definition, the phi=sqrt(rho/pi) bridge, KL/FI vocabulary, and the coefficient 1/(2*C_LSI).

sourceStepMap : List String (explicit)

Ordered descriptive/naming checklist, not logical conjunction or compiler dependency list.

Ordered data items

1. lem:gronwall: the middle target is the final display rewrite, after multiplying by exp(-int_0^t1 a), from exp(-int_0^t1 a)*exp(int_0^t a) to exp(-int_t^t1 a).
2. lem:dv_variation: keep the equality as a cited formula and expose only common-space, measurable-test, and finite-log-mgf interfaces for later SALD instantiations.
3. def:PI: keep the definition contract-only and route the mean-zero Sobolev, bounded-functional, Riesz, weak-PDE, and velocity-bound steps to sald.pi.velocity_norm_backend.
4. eq:LSI-KL-FI: preserve the paper substitution phi=sqrt(rho/pi), density normalization, entropy rewrite, FI chain rule, and final coefficient audit.

leanStepMap : List String (explicit)

Ordered descriptive/naming checklist, not logical conjunction or compiler dependency list.

Ordered data items

1. lem:gronwall -> SALD.saldGronwallExponentRewriteContract, SALD.gronwallExponentRewriteObligation, and the parent SALD.saldGronwallEndpointCalculusContract.
2. lem:dv_variation -> SALD.dvContract, SALD.saldDvFiniteLogMgfContract, probability.dv_variational_formula, and sald.dv_variation.finite_log_mgf_interface.
3. def:PI -> SALD.saldPIContract, SALD.piDefinitionContract, SALD.saldPiVelocityNormDependencyContract, and sald.pi.velocity_norm_backend.
4. eq:LSI-KL-FI -> SALD.saldLsiKlFiBridgeContract, SALD.saldLsiKlFiDensityTestContract, SALD.lsiKlFiVocabularyContract, sald.lsi_kl_fi.density_test_interface, and probability.lsi_to_kl_fi.

citedResultMap : List String (explicit)

Ordered descriptive/naming checklist, not logical conjunction or compiler dependency list.

Ordered data items

1. DV remains the only externally cited result in this focus window; it is still Boucheron Cor. 4.15 / possible SLT entropy_duality pattern only, not a local import.
2. Gronwall exponent rewriting is local real interval-integral and Real.exp algebra; the scalar Real.exp product substep is compiled locally, and no SLT result applies.
3. PI and LSI/KL/FI use local measure, Sobolev, and density-test obligations; no SLT theorem is marked formalized.

obligationMap : List String (explicit)

Ordered descriptive/naming checklist, not logical conjunction or compiler dependency list.

Ordered data items

1. sald.gronwall.exponent_rewrite: interval-integral additivity on 0<=t<=t1, compiled scalar exponent algebra, compiled outer-integral congruence, and remaining theorem-specific adjacent interval-integrability.
2. sald.dv_variation.finite_log_mgf_interface: common measurable space, measurable Z, finite log E_mu[exp Z], and theorem-specific alpha-complexity witnesses.
3. sald.pi.velocity_norm_backend: weighted mean-zero Sobolev Hilbert backend, bounded T_mu, Riesz representation, weak PDE interpretation, and boundary regularity.
4. sald.lsi_kl_fi.density_test_interface: Radon-Nikodym density, smooth/admissible sqrt test, entropy identity, FI chain rule, and coefficient audit.

lowerPacket : List String (explicit)

Ordered descriptive/naming checklist, not logical conjunction or compiler dependency list.

Ordered data items

1. Target SALD.saldGronwallExponentRewriteContract / sald.gronwall.exponent_rewrite only.
2. Preserve appendix.tex:63-69 exactly: no sign assumption on a or b, no change to the additive b_t integral, and no change to the final Gronwall bound.
3. If the interval-integral backend is not ready, keep the scalar exponent lemma as the only formalized substep and refine the remaining obligation rather than proving lem:gronwall or changing theorem statements.
4. Leave DV source-cited, PI contract-only, and LSI/KL/FI as obligations.

reviewerChecklist : List String (explicit)

Ordered descriptive/naming checklist, not logical conjunction or compiler dependency list.

Ordered data items

1. SALD_original.jsonl indexes the four focus labels and excludes sald_version_2.tex.
2. SALD.saldFirstProofDag dependencies for the four labels include the cycle-17 middle rebaseline.
3. Conversion window, proof-obligation ledger, and SLT audit name this middle packet and its Gronwall exponent-rewrite lower target.
4. No analytic backend is promoted to formalized and the mandatory check passes.

status : AutoSamplingTheory.ProofStatus (explicit)

Stored workflow tag; honor the exact default but do not infer mathematical certification.

AutoSamplingTheory.ProofStatus.obligation — stored label only; no proof certification

def cycle17FirstAppendixMiddleAuditContract :
    FirstAppendixMiddleAuditContract where
  sourceIndexPath := "research-wiki/source-index/SALD_original.jsonl"
  focusLabels := [
    "lem:gronwall",
    "lem:dv_variation",
    "def:PI",
    "eq:LSI-KL-FI"
  ]
  sourceReadWindows := [
    "appendix.tex:47-71: Gronwall statement, integrating-factor derivative, integration from 0 to t1, and exponent rewrite at lines 63-69.",
    "appendix.tex:73-79: Donsker--Varadhan variational formula cited from Boucheron Cor. 4.15 with finite log-mgf tests.",
    "appendix.tex:86-94 plus appendix.tex:96-151: PI definition and the downstream Sobolev/Riesz velocity-norm route.",
    "main_body.tex:202-215: LSI definition, the phi=sqrt(rho/pi) bridge, KL/FI vocabulary, and the coefficient 1/(2*C_LSI)."
  ]
  sourceStepMap := [
    "lem:gronwall: the middle target is the final display rewrite, after multiplying by exp(-int_0^t1 a), from exp(-int_0^t1 a)*exp(int_0^t a) to exp(-int_t^t1 a).",
    "lem:dv_variation: keep the equality as a cited formula and expose only common-space, measurable-test, and finite-log-mgf interfaces for later SALD instantiations.",
    "def:PI: keep the definition contract-only and route the mean-zero Sobolev, bounded-functional, Riesz, weak-PDE, and velocity-bound steps to sald.pi.velocity_norm_backend.",
    "eq:LSI-KL-FI: preserve the paper substitution phi=sqrt(rho/pi), density normalization, entropy rewrite, FI chain rule, and final coefficient audit."
  ]
  leanStepMap := [
    "lem:gronwall -> SALD.saldGronwallExponentRewriteContract, SALD.gronwallExponentRewriteObligation, and the parent SALD.saldGronwallEndpointCalculusContract.",
    "lem:dv_variation -> SALD.dvContract, SALD.saldDvFiniteLogMgfContract, probability.dv_variational_formula, and sald.dv_variation.finite_log_mgf_interface.",
    "def:PI -> SALD.saldPIContract, SALD.piDefinitionContract, SALD.saldPiVelocityNormDependencyContract, and sald.pi.velocity_norm_backend.",
    "eq:LSI-KL-FI -> SALD.saldLsiKlFiBridgeContract, SALD.saldLsiKlFiDensityTestContract, SALD.lsiKlFiVocabularyContract, sald.lsi_kl_fi.density_test_interface, and probability.lsi_to_kl_fi."
  ]
  citedResultMap := [
    "DV remains the only externally cited result in this focus window; it is still Boucheron Cor. 4.15 / possible SLT entropy_duality pattern only, not a local import.",
    "Gronwall exponent rewriting is local real interval-integral and Real.exp algebra; the scalar Real.exp product substep is compiled locally, and no SLT result applies.",
    "PI and LSI/KL/FI use local measure, Sobolev, and density-test obligations; no SLT theorem is marked formalized."
  ]
  obligationMap := [
    "sald.gronwall.exponent_rewrite: interval-integral additivity on 0<=t<=t1, compiled scalar exponent algebra, compiled outer-integral congruence, and remaining theorem-specific adjacent interval-integrability.",
    "sald.dv_variation.finite_log_mgf_interface: common measurable space, measurable Z, finite log E_mu[exp Z], and theorem-specific alpha-complexity witnesses.",
    "sald.pi.velocity_norm_backend: weighted mean-zero Sobolev Hilbert backend, bounded T_mu, Riesz representation, weak PDE interpretation, and boundary regularity.",
    "sald.lsi_kl_fi.density_test_interface: Radon-Nikodym density, smooth/admissible sqrt test, entropy identity, FI chain rule, and coefficient audit."
  ]
  lowerPacket := [
    "Target SALD.saldGronwallExponentRewriteContract / sald.gronwall.exponent_rewrite only.",
    "Preserve appendix.tex:63-69 exactly: no sign assumption on a or b, no change to the additive b_t integral, and no change to the final Gronwall bound.",
    "If the interval-integral backend is not ready, keep the scalar exponent lemma as the only formalized substep and refine the remaining obligation rather than proving lem:gronwall or changing theorem statements.",
    "Leave DV source-cited, PI contract-only, and LSI/KL/FI as obligations."
  ]
  reviewerChecklist := [
    "SALD_original.jsonl indexes the four focus labels and excludes sald_version_2.tex.",
    "SALD.saldFirstProofDag dependencies for the four labels include the cycle-17 middle rebaseline.",
    "Conversion window, proof-obligation ledger, and SLT audit name this middle packet and its Gronwall exponent-rewrite lower target.",
    "No analytic backend is promoted to formalized and the mandatory check passes."
  ]
  status := ProofStatus.obligation

/-- Cycle-21 upper packet for the first appendix/vocabulary source-index layer.

This returns to the original first-DAG labels after the cycle-20 discrete
general VA-SALD scalar coefficient work.  It is an upper-role selection packet:
the source theorem statements stay fixed, the source-index and conversion
window must remain synchronized, and lower work should refine one existing
first-layer obligation rather than reopening a theorem proof.
-/