AutoSamplingTheory.SALD.cycle174GeneralMovingTargetDiscreteEmGeneratorLaplacianEventFieldFrozenScalarBrownianItoQuadraticVariationLower1Obligation

Data definition / provenance and workflow record

Meaning and type

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

def cycle174GeneralMovingTargetDiscreteEmGeneratorLaplacianEventFieldFrozenScalarBrownianItoQuadraticVariationLower1Obligation :
    ProofObligation

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.

id : String (explicit)

Stable obligation identifier.

sald.general_moving_target_discrete.cycle174_em_generator_laplacian_event_field_frozen_scalar_brownian_ito_quadratic_variation_lower1

statement : String (explicit)

Desired mathematical or workflow content as String; it is not a proposition in Prop and the def does not prove it.

Cycle 174 lower_1 dynamic-leaf proof-scout packet. Classification: narrows-source-cited-boundary. Exact missing theorem boundary narrowed: hFrozenScalarBrownianItoQuadraticVariationNormalization under SALD.generalMovingTargetDiscreteEmGeneratorLaplacianEventFieldFrozenScalarBrownianItoOneDimTaylorOfGaussianMomentRemainder should be proved only from the two source-backed fields hQuadraticCoeffDef and hVarianceOne. Source route: appendix.tex:984-995 gives the frozen interpolation Brownian increment sigma_eta*(W_s-W_{s_k}); after the paper's drift separation and normalized scalar-coordinate change, the scalar Brownian coordinate is centered with variance one, while appendix.tex:1379-1387 keeps the global sigma_eta^2/2 diffusion coefficient outside the Brownian event field. Therefore the local quadratic coefficient must already be the diagonal Hessian generator SALD.emFrozenScalarBrownianItoOneDimTaylorGenerator (selectedTest phi) x ((stdOrthonormalBasis Real E) i), and the normalized variance field must coerce to 1. Lower_2-ready theorem shape: from hQuadraticCoeffDef : testRegular -> forall phi x i, quadraticCoeff phi x i = SALD.emFrozenScalarBrownianItoOneDimTaylorGenerator (selectedTest phi) x ((stdOrthonormalBasis Real E) i) and hVarianceOne : testRegular -> forall phi x i, (variance phi x i : Real) = 1, prove forall phi x i, quadraticCoeff phi x i * (variance phi x i : Real) = SALD.emFrozenScalarBrownianItoOneDimTaylorGenerator (selectedTest phi) x ((stdOrthonormalBasis Real E) i) by rewriting both source-backed fields and simplifying multiplication by one. If either hQuadraticCoeffDef or hVarianceOne is not source-backed, record exactly that pair as the smaller source-cited gap; do not introduce a wrapper from unexpanded testRegular, do not move sigma_eta^2/2 inside the event field, and do not return to source-Hessian wrapper churn.

source : AutoSamplingTheory.SourceAnchor (explicit)

SourceAnchor supporting the intended requirement.

AutoSamplingTheory.SALD.saldGeneralMovingTargetDiscreteWeakFpSource — audited data reference, not expanded and not a compiled dependency edge

status : AutoSamplingTheory.ProofStatus (explicit)

Stored ProofStatus, default obligation; even an explicitly stored formalized does not independently certify a Lean theorem.

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

dependsOn : List String (explicit)

List of declared dependency names as strings; may mix theorem names, obligations, source labels, or descriptions. Not the compiled dependency DAG.

Ordered data items

1. SALD.cycle174GeneralMovingTargetDiscreteEmGeneratorLaplacianEventFieldFrozenScalarBrownianItoQuadraticVariationMiddleObligation
2. SALD.generalMovingTargetDiscreteEmGeneratorLaplacianEventFieldFrozenScalarBrownianItoOneDimTaylorOfGaussianMomentRemainder
3. SALD.emFrozenScalarBrownianItoOneDimTaylorGenerator
4. SALD.gaussianRealZeroOneDimTaylorMomentContribution
5. hFrozenScalarBrownianItoQuadraticVariationNormalization
6. hQuadraticCoeffDef
7. hVarianceOne
8. hFrozenScalarBrownianItoTaylorMomentDecomposition
9. hFrozenScalarBrownianItoNormalizedTaylorRemainderVanishes
10. hFrozenScalarBrownianItoEventFieldCoordinateSum
11. eq:general_moving_target_SALD_frozen_interp
12. appendix.tex:984-995
13. appendix.tex:1379-1387
14. sald.general_moving_target_discrete.em_interpolation_fp

note : String (explicit)

Recorded evidence/caveats; may distinguish a compiled scalar helper from still-open source analysis.

Local Mathlib/Lean consultation was limited to the already compiled Gaussian moment/Taylor chain in AutoSamplingTheory/SALD.lean, especially SALD.generalMovingTargetDiscreteEmGeneratorLaplacianEventFieldFrozenScalarBrownianItoOneDimTaylorOfGaussianMomentRemainder and SALD.gaussianRealZeroOneDimTaylorMomentContribution. No local SLT file was consulted or imported because this packet is coefficient/variance source bookkeeping, not a probability-library theorem.

def cycle174GeneralMovingTargetDiscreteEmGeneratorLaplacianEventFieldFrozenScalarBrownianItoQuadraticVariationLower1Obligation :
    ProofObligation where
  id := "sald.general_moving_target_discrete.cycle174_em_generator_laplacian_event_field_frozen_scalar_brownian_ito_quadratic_variation_lower1"
  statement := "Cycle 174 lower_1 dynamic-leaf proof-scout packet. Classification: narrows-source-cited-boundary. Exact missing theorem boundary narrowed: hFrozenScalarBrownianItoQuadraticVariationNormalization under SALD.generalMovingTargetDiscreteEmGeneratorLaplacianEventFieldFrozenScalarBrownianItoOneDimTaylorOfGaussianMomentRemainder should be proved only from the two source-backed fields hQuadraticCoeffDef and hVarianceOne. Source route: appendix.tex:984-995 gives the frozen interpolation Brownian increment sigma_eta*(W_s-W_{s_k}); after the paper's drift separation and normalized scalar-coordinate change, the scalar Brownian coordinate is centered with variance one, while appendix.tex:1379-1387 keeps the global sigma_eta^2/2 diffusion coefficient outside the Brownian event field. Therefore the local quadratic coefficient must already be the diagonal Hessian generator SALD.emFrozenScalarBrownianItoOneDimTaylorGenerator (selectedTest phi) x ((stdOrthonormalBasis Real E) i), and the normalized variance field must coerce to 1. Lower_2-ready theorem shape: from hQuadraticCoeffDef : testRegular -> forall phi x i, quadraticCoeff phi x i = SALD.emFrozenScalarBrownianItoOneDimTaylorGenerator (selectedTest phi) x ((stdOrthonormalBasis Real E) i) and hVarianceOne : testRegular -> forall phi x i, (variance phi x i : Real) = 1, prove forall phi x i, quadraticCoeff phi x i * (variance phi x i : Real) = SALD.emFrozenScalarBrownianItoOneDimTaylorGenerator (selectedTest phi) x ((stdOrthonormalBasis Real E) i) by rewriting both source-backed fields and simplifying multiplication by one. If either hQuadraticCoeffDef or hVarianceOne is not source-backed, record exactly that pair as the smaller source-cited gap; do not introduce a wrapper from unexpanded testRegular, do not move sigma_eta^2/2 inside the event field, and do not return to source-Hessian wrapper churn."
  source := saldGeneralMovingTargetDiscreteWeakFpSource
  status := ProofStatus.obligation
  dependsOn := [
    "SALD.cycle174GeneralMovingTargetDiscreteEmGeneratorLaplacianEventFieldFrozenScalarBrownianItoQuadraticVariationMiddleObligation",
    "SALD.generalMovingTargetDiscreteEmGeneratorLaplacianEventFieldFrozenScalarBrownianItoOneDimTaylorOfGaussianMomentRemainder",
    "SALD.emFrozenScalarBrownianItoOneDimTaylorGenerator",
    "SALD.gaussianRealZeroOneDimTaylorMomentContribution",
    "hFrozenScalarBrownianItoQuadraticVariationNormalization",
    "hQuadraticCoeffDef",
    "hVarianceOne",
    "hFrozenScalarBrownianItoTaylorMomentDecomposition",
    "hFrozenScalarBrownianItoNormalizedTaylorRemainderVanishes",
    "hFrozenScalarBrownianItoEventFieldCoordinateSum",
    "eq:general_moving_target_SALD_frozen_interp",
    "appendix.tex:984-995",
    "appendix.tex:1379-1387",
    "sald.general_moving_target_discrete.em_interpolation_fp"
  ]
  note := "Local Mathlib/Lean consultation was limited to the already compiled Gaussian moment/Taylor chain in AutoSamplingTheory/SALD.lean, especially SALD.generalMovingTargetDiscreteEmGeneratorLaplacianEventFieldFrozenScalarBrownianItoOneDimTaylorOfGaussianMomentRemainder and SALD.gaussianRealZeroOneDimTaylorMomentContribution. No local SLT file was consulted or imported because this packet is coefficient/variance source bookkeeping, not a probability-library theorem."

/-- Cycle-174 lower_2 compiled bridge from the source-backed coefficient and
variance fields to the Brownian quadratic-variation normalization. -/