AutoSamplingTheory.SALD.cycle177GeneralMovingTargetDiscreteEmGeneratorLaplacianEventFieldFrozenScalarBrownianItoSecondTaylorCoeffMiddleObligation

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 cycle177GeneralMovingTargetDiscreteEmGeneratorLaplacianEventFieldFrozenScalarBrownianItoSecondTaylorCoeffMiddleObligation :
    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.cycle177_em_generator_laplacian_event_field_frozen_scalar_brownian_ito_second_taylor_coeff_middle

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 177 middle dynamic-leaf worker packet. Classification: narrows-source-cited-boundary. Exact boundary narrowed: hSecondTaylorCoeffDef is no longer primitive once the source correspondence supplies hScalarLineSecondCoeffDef : testRegular -> forall phi x i, quadraticCoeff phi x i = iteratedDeriv 2 (fun q : Real => selectedTest phi (x + q • (stdOrthonormalBasis Real E i))) 0, together with the already explicit selected-test ambient C2 regularity hSource : testRegular -> forall phi, ContDiffOn Real 2 (selectedTest phi) Set.univ. SALD.selectedWeakTestSecondTaylorCoeffDefOfScalarLineSecondCoeffDef compiles the local Mathlib bridge by applying SALD.gaussianRealSelectedTestLineSecondDerivEqDirectionalFDeriv at q = 0 and identifying the repeated Fin 2 direction with ![e_i, e_i]. Source decision: hSourceHasHessian and hSourceHessianBound are still not derivable from appendix.tex:984-995, appendix.tex:1026-1072, appendix.tex:1170-1176, appendix.tex:1379-1387, main_body.tex:273-305, or iteration_complexity.tex:309-321, so they remain source-contract gaps and are not used in this bridge. Remaining source boundary after this packet is hScalarLineSecondCoeffDef for the scalar Brownian second Taylor coefficient and hNormalizedVarianceDef for the normalized Brownian variance; hSecondCoeff, Taylor moment decomposition, normalized-remainder DCT data, and coordinate-sum stay explicit.

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.formalized — 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.selectedWeakTestSecondTaylorCoeffDefOfScalarLineSecondCoeffDef
2. SALD.gaussianRealSelectedTestLineSecondDerivEqDirectionalFDeriv
3. SALD.selectedWeakTestQuadraticVariationNormalizationOfSecondTaylorCoeffAndNormalizedVarianceDef
4. SALD.selectedWeakTestQuadraticCoeffDefOfSecondTaylorCoeffDef
5. hSecondTaylorCoeffDef
6. hScalarLineSecondCoeffDef
7. hSource
8. hNormalizedVarianceDef
9. hSourceHasHessian
10. hSourceHessianBound
11. hSecondCoeff
12. hFrozenScalarBrownianItoTaylorMomentDecomposition
13. hFrozenScalarBrownianItoNormalizedTaylorRemainderVanishes
14. hFrozenScalarBrownianItoEventFieldCoordinateSum
15. eq:SALD_general_EM
16. eq:general_moving_target_SALD_frozen_interp
17. eq:increment_basic_bound_revised
18. appendix.tex:958-970
19. appendix.tex:984-995
20. appendix.tex:1026-1072
21. appendix.tex:1170-1176
22. appendix.tex:1379-1387
23. main_body.tex:273-305
24. iteration_complexity.tex:309-321 score Hessian bound rejected for sourceTest
25. paper-wide original-source search excluding sald_version_2.tex
26. 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.

No local SLT file was consulted or imported. The compiled bridge uses only the existing local affine-line second-derivative chain rule and a Fin 2 direction-vector identification. It does not derive or use hSourceHasHessian/hSourceHessianBound, does not define sourceHessian from the desired conclusion, does not move sigma_eta^2/2 inside the event field, and does not mark the stochastic scalar coefficient source fact formalized.

def cycle177GeneralMovingTargetDiscreteEmGeneratorLaplacianEventFieldFrozenScalarBrownianItoSecondTaylorCoeffMiddleObligation :
    ProofObligation where
  id := "sald.general_moving_target_discrete.cycle177_em_generator_laplacian_event_field_frozen_scalar_brownian_ito_second_taylor_coeff_middle"
  statement := "Cycle 177 middle dynamic-leaf worker packet. Classification: narrows-source-cited-boundary. Exact boundary narrowed: hSecondTaylorCoeffDef is no longer primitive once the source correspondence supplies hScalarLineSecondCoeffDef : testRegular -> forall phi x i, quadraticCoeff phi x i = iteratedDeriv 2 (fun q : Real => selectedTest phi (x + q • (stdOrthonormalBasis Real E i))) 0, together with the already explicit selected-test ambient C2 regularity hSource : testRegular -> forall phi, ContDiffOn Real 2 (selectedTest phi) Set.univ. SALD.selectedWeakTestSecondTaylorCoeffDefOfScalarLineSecondCoeffDef compiles the local Mathlib bridge by applying SALD.gaussianRealSelectedTestLineSecondDerivEqDirectionalFDeriv at q = 0 and identifying the repeated Fin 2 direction with ![e_i, e_i]. Source decision: hSourceHasHessian and hSourceHessianBound are still not derivable from appendix.tex:984-995, appendix.tex:1026-1072, appendix.tex:1170-1176, appendix.tex:1379-1387, main_body.tex:273-305, or iteration_complexity.tex:309-321, so they remain source-contract gaps and are not used in this bridge. Remaining source boundary after this packet is hScalarLineSecondCoeffDef for the scalar Brownian second Taylor coefficient and hNormalizedVarianceDef for the normalized Brownian variance; hSecondCoeff, Taylor moment decomposition, normalized-remainder DCT data, and coordinate-sum stay explicit."
  source := saldGeneralMovingTargetDiscreteWeakFpSource
  status := ProofStatus.formalized
  dependsOn := [
    "SALD.selectedWeakTestSecondTaylorCoeffDefOfScalarLineSecondCoeffDef",
    "SALD.gaussianRealSelectedTestLineSecondDerivEqDirectionalFDeriv",
    "SALD.selectedWeakTestQuadraticVariationNormalizationOfSecondTaylorCoeffAndNormalizedVarianceDef",
    "SALD.selectedWeakTestQuadraticCoeffDefOfSecondTaylorCoeffDef",
    "hSecondTaylorCoeffDef",
    "hScalarLineSecondCoeffDef",
    "hSource",
    "hNormalizedVarianceDef",
    "hSourceHasHessian",
    "hSourceHessianBound",
    "hSecondCoeff",
    "hFrozenScalarBrownianItoTaylorMomentDecomposition",
    "hFrozenScalarBrownianItoNormalizedTaylorRemainderVanishes",
    "hFrozenScalarBrownianItoEventFieldCoordinateSum",
    "eq:SALD_general_EM",
    "eq:general_moving_target_SALD_frozen_interp",
    "eq:increment_basic_bound_revised",
    "appendix.tex:958-970",
    "appendix.tex:984-995",
    "appendix.tex:1026-1072",
    "appendix.tex:1170-1176",
    "appendix.tex:1379-1387",
    "main_body.tex:273-305",
    "iteration_complexity.tex:309-321 score Hessian bound rejected for sourceTest",
    "paper-wide original-source search excluding sald_version_2.tex",
    "sald.general_moving_target_discrete.em_interpolation_fp"
  ]
  note := "No local SLT file was consulted or imported. The compiled bridge uses only the existing local affine-line second-derivative chain rule and a Fin 2 direction-vector identification. It does not derive or use hSourceHasHessian/hSourceHessianBound, does not define sourceHessian from the desired conclusion, does not move sigma_eta^2/2 inside the event field, and does not mark the stochastic scalar coefficient source fact formalized."

/-- Cycle-177 proof-DAG pane for the scalar-line coefficient narrowing. -/