AutoSamplingTheory.SALD.cycle13FirstAppendixMiddleAuditContract

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 cycle13FirstAppendixMiddleAuditContract :
    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.
2. appendix.tex:73-79: DV variational formula cited from Boucheron Cor. 4.15.
3. appendix.tex:86-151: PI definition plus velocity-norm Sobolev/Riesz proof route.
4. main_body.tex:202-215: LSI definition, phi=sqrt(rho/pi), 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: start from dK/dt <= -a_t*K_t+b_t, differentiate exp(int_0^t a)*K, integrate from 0 to t1, then rewrite exp(-int_0^t1 a)*exp(int_0^t a) as exp(-int_t^t1 a); the source assumes continuous a,b and differentiable K on [0,t1].
2. lem:dv_variation: use the cited equality KL(nu||mu)=sup_Z(E_nu Z-log E_mu exp Z) over finite-log-mgf tests; later SALD uses only instantiations with squared velocity or residual fields.
3. def:PI: record Var_mu(phi) <= C_PI^{-1}*int ||nabla phi||^2 dmu, then map the appendix Sobolev/Riesz velocity-norm proof to a separate backend obligation instead of folding it into the definition.
4. eq:LSI-KL-FI: apply LSI to phi=sqrt(rho/pi), identify entropy with KL and the gradient term with one quarter of FI, preserving the coefficient 1/(2*C_LSI).

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.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 the only external cited result in the focus window; it remains source-cited from Boucheron Cor. 4.15 and is not imported from SLT or Mathlib.
2. Gronwall is a local real-calculus obligation; possible Mathlib interval-integral and derivative lemmas are backend candidates only.
3. PI and LSI/KL/FI vocabulary require local measure/Sobolev/density-test backends; no SLT theorem is marked as formalized.

obligationMap : List String (explicit)

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

Ordered data items

1. Gronwall blocked on endpoint-safe differentiability or absolute-continuity formulation, interval-integral FTC, order integration, endpoint evaluation, and the separated exponent rewrite sald.gronwall.exponent_rewrite.
2. DV blocked on common probability space, measurable test variables, finite log-mgf witnesses, and alpha-complexity monotonicity for theorem-specific squared-norm tests.
3. PI velocity bound blocked on weighted mean-zero Sobolev Hilbert structure, bounded functional T_mu, Riesz representation, weak PDE regularity, and boundary handling.
4. LSI/KL/FI blocked on Radon-Nikodym density vocabulary, admissibility or 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. Preferred lower target: SALD.saldGronwallEndpointCalculusContract and its lower sub-obligation SALD.saldGronwallExponentRewriteContract / sald.gronwall.exponent_rewrite, because the source proof is self-contained real calculus and does not require the probability backend.
2. Alternative lower targets: SALD.saldDvFiniteLogMgfContract, SALD.saldPiVelocityNormDependencyContract, or SALD.saldLsiKlFiDensityTestContract.
3. Refine one interface only; if a full backend proof is not ready, add a narrower ProofObligation instead of changing theorem statements.
4. Preserve the SourceAnchor from SALD_original.jsonl and leave sald_version_2.tex excluded.

reviewerChecklist : List String (explicit)

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

Ordered data items

1. The middle map cites the same four source-index labels and line windows as the upper packet.
2. Each source proof step is classified as Lean contract, cited result, or named obligation.
3. No first-layer status is upgraded to formalized and no later SALD theorem target is edited.
4. Conversion window, proof-obligation ledger, SLT audit, and saldFirstProofDag mention the middle map.

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 cycle13FirstAppendixMiddleAuditContract :
    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.",
    "appendix.tex:73-79: DV variational formula cited from Boucheron Cor. 4.15.",
    "appendix.tex:86-151: PI definition plus velocity-norm Sobolev/Riesz proof route.",
    "main_body.tex:202-215: LSI definition, phi=sqrt(rho/pi), and KL/FI vocabulary."
  ]
  sourceStepMap := [
    "lem:gronwall: start from dK/dt <= -a_t*K_t+b_t, differentiate exp(int_0^t a)*K, integrate from 0 to t1, then rewrite exp(-int_0^t1 a)*exp(int_0^t a) as exp(-int_t^t1 a); the source assumes continuous a,b and differentiable K on [0,t1].",
    "lem:dv_variation: use the cited equality KL(nu||mu)=sup_Z(E_nu Z-log E_mu exp Z) over finite-log-mgf tests; later SALD uses only instantiations with squared velocity or residual fields.",
    "def:PI: record Var_mu(phi) <= C_PI^{-1}*int ||nabla phi||^2 dmu, then map the appendix Sobolev/Riesz velocity-norm proof to a separate backend obligation instead of folding it into the definition.",
    "eq:LSI-KL-FI: apply LSI to phi=sqrt(rho/pi), identify entropy with KL and the gradient term with one quarter of FI, preserving the coefficient 1/(2*C_LSI)."
  ]
  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.lsi_kl_fi.density_test_interface, and probability.lsi_to_kl_fi."
  ]
  citedResultMap := [
    "DV is the only external cited result in the focus window; it remains source-cited from Boucheron Cor. 4.15 and is not imported from SLT or Mathlib.",
    "Gronwall is a local real-calculus obligation; possible Mathlib interval-integral and derivative lemmas are backend candidates only.",
    "PI and LSI/KL/FI vocabulary require local measure/Sobolev/density-test backends; no SLT theorem is marked as formalized."
  ]
  obligationMap := [
    "Gronwall blocked on endpoint-safe differentiability or absolute-continuity formulation, interval-integral FTC, order integration, endpoint evaluation, and the separated exponent rewrite sald.gronwall.exponent_rewrite.",
    "DV blocked on common probability space, measurable test variables, finite log-mgf witnesses, and alpha-complexity monotonicity for theorem-specific squared-norm tests.",
    "PI velocity bound blocked on weighted mean-zero Sobolev Hilbert structure, bounded functional T_mu, Riesz representation, weak PDE regularity, and boundary handling.",
    "LSI/KL/FI blocked on Radon-Nikodym density vocabulary, admissibility or approximation for sqrt(rho/pi), entropy rewrite, FI chain rule, and coefficient audit."
  ]
  lowerPacket := [
    "Preferred lower target: SALD.saldGronwallEndpointCalculusContract and its lower sub-obligation SALD.saldGronwallExponentRewriteContract / sald.gronwall.exponent_rewrite, because the source proof is self-contained real calculus and does not require the probability backend.",
    "Alternative lower targets: SALD.saldDvFiniteLogMgfContract, SALD.saldPiVelocityNormDependencyContract, or SALD.saldLsiKlFiDensityTestContract.",
    "Refine one interface only; if a full backend proof is not ready, add a narrower ProofObligation instead of changing theorem statements.",
    "Preserve the SourceAnchor from SALD_original.jsonl and leave sald_version_2.tex excluded."
  ]
  reviewerChecklist := [
    "The middle map cites the same four source-index labels and line windows as the upper packet.",
    "Each source proof step is classified as Lean contract, cited result, or named obligation.",
    "No first-layer status is upgraded to formalized and no later SALD theorem target is edited.",
    "Conversion window, proof-obligation ledger, SLT audit, and saldFirstProofDag mention the middle map."
  ]
  status := ProofStatus.obligation

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

This returns to the source-index focus after the cycle-16 unified transport
bridge work.  It is workflow data only: the four source labels remain fixed,
the existing first-layer contracts remain the Lean targets, and every analytic
backend keeps its honest non-formalized status.
-/