AutoSamplingTheory.SALD.cycle21FirstAppendixMiddleAuditContract

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 cycle21FirstAppendixMiddleAuditContract :
    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 final exponent rewrite.
2. appendix.tex:73-79: Donsker--Varadhan formula cited as Boucheron Cor. 4.15, with same-space probabilities and finite log-mgf tests.
3. appendix.tex:86-151: PI definition, weighted mean-zero Sobolev space, bounded functional, Riesz step, and velocity-norm applications.
4. main_body.tex:202-215: LSI definition, rho << pi density route with phi=sqrt(rho/pi), KL/FI comparison, and KL/FI vocabulary.

sourceStepMap : List String (explicit)

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

Ordered data items

1. lem:gronwall: lines 47-52 state the differential inequality and endpoint bound; lines 58-61 differentiate exp(int_0^t a)*K; line 63 integrates; lines 65-69 multiply by exp(-int_0^t1 a) and rewrite the integral factor to exp(-int_t^t1 a).
2. lem:dv_variation: lines 73-79 give the cited variational equality KL(nu||mu)=sup_Z(E_nu Z-log E_mu exp Z), with the finite log-mgf side condition as the only local instantiation interface.
3. def:PI: lines 86-94 define PI by Var_mu(phi) <= C_PI^{-1} int ||nabla phi||^2 dmu; lines 96-151 use that definition for weighted Sobolev norm equivalence, weak PDE/Riesz representation, and A_0 velocity bounds.
4. eq:LSI-KL-FI: lines 202-215 define LSI, substitute phi=sqrt(rho/pi), record KL <= FI/(2*C_LSI), and define the KL/FI integrals under rho << pi.

leanStepMap : List String (explicit)

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

Ordered data items

1. lem:gronwall -> SALD.saldGronwallCandidateContract, SALD.saldGronwallEndpointCalculusContract, SALD.saldGronwallExponentRewriteContract, sald.gronwall.integrating_factor, sald.gronwall.endpoint_calculus, and sald.gronwall.exponent_rewrite.
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.saldKLContract, SALD.saldFIContract, SALD.saldLSIContract, 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 is source-cited from Boucheron Cor. 4.15; an SLT entropy_duality pattern is only a future port candidate and is not imported.
2. Gronwall is local real/interval-integral calculus; existing scalar exponent helpers are formalized substeps only, not a proof of the lemma.
3. PI velocity bounds and LSI-to-KL/FI remain local measure/Sobolev/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 remains blocked on endpoint-safe calculus/FTC choices, adjacent interval-integrability in theorem contexts, and congruence inside the b_t integral.
2. sald.dv_variation.finite_log_mgf_interface remains blocked on common measurable space, measurable Z, finite log E_mu[exp Z], and alpha-complexity witnesses for squared fields.
3. sald.pi.velocity_norm_backend remains blocked on weighted mean-zero Sobolev Hilbert structure, bounded T_mu, Riesz representation, weak PDE interpretation, and boundary regularity.
4. sald.lsi_kl_fi.density_test_interface remains blocked on Radon-Nikodym density conventions, admissibility/approximation for sqrt(rho/pi), entropy rewrite, 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 exactly SALD.saldGronwallExponentRewriteContract / sald.gronwall.exponent_rewrite as the first lower slice.
2. Permitted work: refine endpoint-safe derivative/FTC assumptions, adjacent interval-integrability, or the remaining integral-congruence obligation for appendix.tex:63-69.
3. Keep the already formalized scalar helpers as substeps only; do not mark lem:gronwall formalized unless the full local theorem builds.
4. Leave DV source-cited, PI contract-only, LSI/KL/FI obligation, and all forward-KL or VA-SALD theorem statements unchanged.

reviewerChecklist : List String (explicit)

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

Ordered data items

1. SALD_original.jsonl indexes lem:gronwall, lem:dv_variation, def:PI, and eq:LSI-KL-FI from the original source and excludes sald_version_2.tex.
2. SALD.saldFirstProofDag dependencies for the four focus labels include SALD.cycle21FirstAppendixMiddleAuditContract.
3. The conversion window, proof-obligation ledger, SLT audit, and dialogue board identify cycle 21 middle as source-to-Lean synchronization, not analytic proof closure.
4. python3 tools/astis.py source-index ASTIS-SALD-001 and python3 tools/astis.py check pass.

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 cycle21FirstAppendixMiddleAuditContract :
    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 final exponent rewrite.",
    "appendix.tex:73-79: Donsker--Varadhan formula cited as Boucheron Cor. 4.15, with same-space probabilities and finite log-mgf tests.",
    "appendix.tex:86-151: PI definition, weighted mean-zero Sobolev space, bounded functional, Riesz step, and velocity-norm applications.",
    "main_body.tex:202-215: LSI definition, rho << pi density route with phi=sqrt(rho/pi), KL/FI comparison, and KL/FI vocabulary."
  ]
  sourceStepMap := [
    "lem:gronwall: lines 47-52 state the differential inequality and endpoint bound; lines 58-61 differentiate exp(int_0^t a)*K; line 63 integrates; lines 65-69 multiply by exp(-int_0^t1 a) and rewrite the integral factor to exp(-int_t^t1 a).",
    "lem:dv_variation: lines 73-79 give the cited variational equality KL(nu||mu)=sup_Z(E_nu Z-log E_mu exp Z), with the finite log-mgf side condition as the only local instantiation interface.",
    "def:PI: lines 86-94 define PI by Var_mu(phi) <= C_PI^{-1} int ||nabla phi||^2 dmu; lines 96-151 use that definition for weighted Sobolev norm equivalence, weak PDE/Riesz representation, and A_0 velocity bounds.",
    "eq:LSI-KL-FI: lines 202-215 define LSI, substitute phi=sqrt(rho/pi), record KL <= FI/(2*C_LSI), and define the KL/FI integrals under rho << pi."
  ]
  leanStepMap := [
    "lem:gronwall -> SALD.saldGronwallCandidateContract, SALD.saldGronwallEndpointCalculusContract, SALD.saldGronwallExponentRewriteContract, sald.gronwall.integrating_factor, sald.gronwall.endpoint_calculus, and sald.gronwall.exponent_rewrite.",
    "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.saldKLContract, SALD.saldFIContract, SALD.saldLSIContract, SALD.saldLsiKlFiBridgeContract, SALD.saldLsiKlFiDensityTestContract, SALD.lsiKlFiVocabularyContract, sald.lsi_kl_fi.density_test_interface, and probability.lsi_to_kl_fi."
  ]
  citedResultMap := [
    "DV is source-cited from Boucheron Cor. 4.15; an SLT entropy_duality pattern is only a future port candidate and is not imported.",
    "Gronwall is local real/interval-integral calculus; existing scalar exponent helpers are formalized substeps only, not a proof of the lemma.",
    "PI velocity bounds and LSI-to-KL/FI remain local measure/Sobolev/density-test obligations; no SLT theorem is marked formalized."
  ]
  obligationMap := [
    "sald.gronwall.exponent_rewrite remains blocked on endpoint-safe calculus/FTC choices, adjacent interval-integrability in theorem contexts, and congruence inside the b_t integral.",
    "sald.dv_variation.finite_log_mgf_interface remains blocked on common measurable space, measurable Z, finite log E_mu[exp Z], and alpha-complexity witnesses for squared fields.",
    "sald.pi.velocity_norm_backend remains blocked on weighted mean-zero Sobolev Hilbert structure, bounded T_mu, Riesz representation, weak PDE interpretation, and boundary regularity.",
    "sald.lsi_kl_fi.density_test_interface remains blocked on Radon-Nikodym density conventions, admissibility/approximation for sqrt(rho/pi), entropy rewrite, FI chain rule, and coefficient audit."
  ]
  lowerPacket := [
    "Target exactly SALD.saldGronwallExponentRewriteContract / sald.gronwall.exponent_rewrite as the first lower slice.",
    "Permitted work: refine endpoint-safe derivative/FTC assumptions, adjacent interval-integrability, or the remaining integral-congruence obligation for appendix.tex:63-69.",
    "Keep the already formalized scalar helpers as substeps only; do not mark lem:gronwall formalized unless the full local theorem builds.",
    "Leave DV source-cited, PI contract-only, LSI/KL/FI obligation, and all forward-KL or VA-SALD theorem statements unchanged."
  ]
  reviewerChecklist := [
    "SALD_original.jsonl indexes lem:gronwall, lem:dv_variation, def:PI, and eq:LSI-KL-FI from the original source and excludes sald_version_2.tex.",
    "SALD.saldFirstProofDag dependencies for the four focus labels include SALD.cycle21FirstAppendixMiddleAuditContract.",
    "The conversion window, proof-obligation ledger, SLT audit, and dialogue board identify cycle 21 middle as source-to-Lean synchronization, not analytic proof closure.",
    "python3 tools/astis.py source-index ASTIS-SALD-001 and python3 tools/astis.py check pass."
  ]
  status := ProofStatus.obligation

/-- Cycle-25 upper packet for the first appendix/vocabulary layer.

This returns to the source-index focus after the cycle-24 continuous general
VA-SALD Gronwall coefficient work.  It chooses the PI velocity-norm dependency
as the next lower slice while keeping the four first-layer source labels and
all analytic statuses fixed.
-/