AutoSamplingTheory.SALD.cycle25FirstAppendixMiddleAuditContract

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 cycle25FirstAppendixMiddleAuditContract :
    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 and integrating-factor proof; unchanged status guard for this cycle.
2. appendix.tex:73-79: Donsker--Varadhan formula cited as Boucheron Cor. 4.15; unchanged source-cited dependency.
3. appendix.tex:86-151: PI definition plus the weighted Sobolev/Riesz velocity-norm route, with the lower sub-slice starting at appendix.tex:96-129.
4. main_body.tex:202-215: LSI definition, phi=sqrt(rho/pi), KL/FI vocabulary, and coefficient 1/(2*C_LSI); unchanged obligation.

sourceStepMap : List String (explicit)

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

Ordered data items

1. lem:gronwall: keep dK/dt <= -a_t*K_t+b_t and the endpoint exponent display as existing Gronwall obligations; no Gronwall proof search is selected in cycle 25.
2. lem:dv_variation: keep the cited variational equality over finite-log-mgf random variables; local theorem instantiations still owe common-space, measurability, and finite-log-mgf witnesses.
3. def:PI: lines 86-94 define PI; lines 96-103 define dot H^1(mu) and its gradient inner product; lines 104-112 use PI to identify the gradient norm as equivalent to the weighted H^1 norm on the mean-zero space; lines 114-129 introduce the weak PDE and the first Cauchy-Schwarz bound for T_mu before the Riesz step.
4. def:PI follow-on: lines 130-138 are the immediate PI operator-norm and Riesz continuation after the selected first sub-slice; lower should expose the interface but not prove the Riesz backend unless it builds locally.
5. eq:LSI-KL-FI: keep the source route phi=sqrt(rho/pi), entropy rewrite, FI chain rule, and coefficient audit in the existing density-test obligation.

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, and existing sald.gronwall.* obligations.
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, SALD.piVelocityNormBackendObligation, and sald.pi.velocity_norm_backend.
4. cycle 25 PI lower target -> SALD.cycle25FirstAppendixMiddleAuditContract and SALD.cycle25FirstAppendixPiVelocityNormMiddleObligation, refining only the appendix.tex:96-129 source-to-Lean interface.
5. eq:LSI-KL-FI -> SALD.saldKLContract, SALD.saldFIContract, SALD.saldLSIContract, SALD.saldLsiKlFiDensityTestContract, 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 external cited result in the first-layer window; no SLT theorem is imported or promoted.
2. The PI velocity-norm route is local analysis: weighted Sobolev Hilbert structure, PI norm equivalence, bounded functional, Riesz representation, weak PDE, and boundary/regularity interfaces.
3. Gronwall and LSI/KL/FI remain local Mathlib/measure obligations outside this lower slice.

obligationMap : List String (explicit)

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

Ordered data items

1. sald.pi.velocity_norm_backend first sub-slice: formalize or specify dot H^1(mu), the mean-zero condition E_mu[psi]=0, the gradient inner product, the PI-to-H1 norm equivalence, and boundedness of T_mu before Riesz.
2. sald.pi.velocity_norm_backend follow-on: line 119 has a phi/psi notation mismatch in the source, and lines 130-138 require the operator-norm, Riesz representation, weak-PDE interpretation, and boundary/regularity backend.
3. sald.gronwall.exponent_rewrite, sald.dv_variation.finite_log_mgf_interface, and sald.lsi_kl_fi.density_test_interface remain unchanged obligations/source-cited dependencies.
4. No theorem-level forward-KL, discrete, guided, general VA-SALD, or unified theorem statement is changed by this map.

lowerPacket : List String (explicit)

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

Ordered data items

1. Target exactly SALD.saldPiVelocityNormDependencyContract / SALD.piVelocityNormBackendObligation / sald.pi.velocity_norm_backend.
2. Start with appendix.tex:96-129: dot H^1(mu), mean-zero interface, gradient inner product, PI norm equivalence, weak-form notation, and the Cauchy-Schwarz boundedness of T_mu.
3. Record line 119's phi/psi mismatch and the line 130-138 operator-norm/Riesz continuation as explicit source-contract gaps if the lower proof cannot close them.
4. Do not reopen Gronwall, DV, LSI-to-KL/FI, forward-KL, guided, general VA-SALD, unified, or discrete proof search in this lower attempt.

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, lem:velocity-norm-bound, and eq:LSI-KL-FI from the original files while excluding sald_version_2.tex.
2. SALD.saldFirstProofDag dependencies for the four first-layer labels include SALD.cycle25FirstAppendixMiddleAuditContract.
3. def:PI dependencies include SALD.cycle25FirstAppendixPiVelocityNormMiddleObligation and still report PI as contractOnly, with velocity-norm as an obligation.
4. Conversion window, proof-obligation ledger, SLT audit, and dialogue board classify cycle 25 middle as source-to-Lean synchronization, not analytic proof closure.

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 cycle25FirstAppendixMiddleAuditContract :
    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 and integrating-factor proof; unchanged status guard for this cycle.",
    "appendix.tex:73-79: Donsker--Varadhan formula cited as Boucheron Cor. 4.15; unchanged source-cited dependency.",
    "appendix.tex:86-151: PI definition plus the weighted Sobolev/Riesz velocity-norm route, with the lower sub-slice starting at appendix.tex:96-129.",
    "main_body.tex:202-215: LSI definition, phi=sqrt(rho/pi), KL/FI vocabulary, and coefficient 1/(2*C_LSI); unchanged obligation."
  ]
  sourceStepMap := [
    "lem:gronwall: keep dK/dt <= -a_t*K_t+b_t and the endpoint exponent display as existing Gronwall obligations; no Gronwall proof search is selected in cycle 25.",
    "lem:dv_variation: keep the cited variational equality over finite-log-mgf random variables; local theorem instantiations still owe common-space, measurability, and finite-log-mgf witnesses.",
    "def:PI: lines 86-94 define PI; lines 96-103 define dot H^1(mu) and its gradient inner product; lines 104-112 use PI to identify the gradient norm as equivalent to the weighted H^1 norm on the mean-zero space; lines 114-129 introduce the weak PDE and the first Cauchy-Schwarz bound for T_mu before the Riesz step.",
    "def:PI follow-on: lines 130-138 are the immediate PI operator-norm and Riesz continuation after the selected first sub-slice; lower should expose the interface but not prove the Riesz backend unless it builds locally.",
    "eq:LSI-KL-FI: keep the source route phi=sqrt(rho/pi), entropy rewrite, FI chain rule, and coefficient audit in the existing density-test obligation."
  ]
  leanStepMap := [
    "lem:gronwall -> SALD.saldGronwallCandidateContract, SALD.saldGronwallEndpointCalculusContract, SALD.saldGronwallExponentRewriteContract, and existing sald.gronwall.* obligations.",
    "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, SALD.piVelocityNormBackendObligation, and sald.pi.velocity_norm_backend.",
    "cycle 25 PI lower target -> SALD.cycle25FirstAppendixMiddleAuditContract and SALD.cycle25FirstAppendixPiVelocityNormMiddleObligation, refining only the appendix.tex:96-129 source-to-Lean interface.",
    "eq:LSI-KL-FI -> SALD.saldKLContract, SALD.saldFIContract, SALD.saldLSIContract, SALD.saldLsiKlFiDensityTestContract, sald.lsi_kl_fi.density_test_interface, and probability.lsi_to_kl_fi."
  ]
  citedResultMap := [
    "DV remains the only external cited result in the first-layer window; no SLT theorem is imported or promoted.",
    "The PI velocity-norm route is local analysis: weighted Sobolev Hilbert structure, PI norm equivalence, bounded functional, Riesz representation, weak PDE, and boundary/regularity interfaces.",
    "Gronwall and LSI/KL/FI remain local Mathlib/measure obligations outside this lower slice."
  ]
  obligationMap := [
    "sald.pi.velocity_norm_backend first sub-slice: formalize or specify dot H^1(mu), the mean-zero condition E_mu[psi]=0, the gradient inner product, the PI-to-H1 norm equivalence, and boundedness of T_mu before Riesz.",
    "sald.pi.velocity_norm_backend follow-on: line 119 has a phi/psi notation mismatch in the source, and lines 130-138 require the operator-norm, Riesz representation, weak-PDE interpretation, and boundary/regularity backend.",
    "sald.gronwall.exponent_rewrite, sald.dv_variation.finite_log_mgf_interface, and sald.lsi_kl_fi.density_test_interface remain unchanged obligations/source-cited dependencies.",
    "No theorem-level forward-KL, discrete, guided, general VA-SALD, or unified theorem statement is changed by this map."
  ]
  lowerPacket := [
    "Target exactly SALD.saldPiVelocityNormDependencyContract / SALD.piVelocityNormBackendObligation / sald.pi.velocity_norm_backend.",
    "Start with appendix.tex:96-129: dot H^1(mu), mean-zero interface, gradient inner product, PI norm equivalence, weak-form notation, and the Cauchy-Schwarz boundedness of T_mu.",
    "Record line 119's phi/psi mismatch and the line 130-138 operator-norm/Riesz continuation as explicit source-contract gaps if the lower proof cannot close them.",
    "Do not reopen Gronwall, DV, LSI-to-KL/FI, forward-KL, guided, general VA-SALD, unified, or discrete proof search in this lower attempt."
  ]
  reviewerChecklist := [
    "SALD_original.jsonl indexes lem:gronwall, lem:dv_variation, def:PI, lem:velocity-norm-bound, and eq:LSI-KL-FI from the original files while excluding sald_version_2.tex.",
    "SALD.saldFirstProofDag dependencies for the four first-layer labels include SALD.cycle25FirstAppendixMiddleAuditContract.",
    "def:PI dependencies include SALD.cycle25FirstAppendixPiVelocityNormMiddleObligation and still report PI as contractOnly, with velocity-norm as an obligation.",
    "Conversion window, proof-obligation ledger, SLT audit, and dialogue board classify cycle 25 middle as source-to-Lean synchronization, not analytic proof closure."
  ]
  status := ProofStatus.obligation

/-- Cycle-25 middle obligation for the selected PI velocity-norm sub-slice. -/