Record the intended labels of a guided tilt
AutoSamplingTheory.GuidedTiltContract · structure · Teaching coverage
Statement
This record stores names for a base path, guide, guided path and terminal target together with a source and default contractOnly status. The intended exponentially tilted relationship is descriptive, not an enforced measure equality.
All objects and hypotheses
- basePath has type String: base-path label.
- guideName has type String: guide label.
- guidedPath has type String: tilted-path label.
- terminalTarget has type String: terminal target label.
- source has type SourceAnchor: provenance.
- status has type ProofStatus: default contractOnly.
- No ambient measurable space, measure, analytic hypothesis or proof witness is a parameter of this metadata structure. Default fields may be overridden when constructing a record.
Notation and interpretation
- Analytic values versus metadata
Contracts and obligation/interface constructors store strings and status labels. They are not propositions asserting the written mathematics and supply no Lean proof of it.
\[\texttt{ProofObligation}\ne\text{proof of its statement string}\]
Construction and meaning
1. Specify the record's data slots
The structure declares exactly the listed fields and their data types. A source anchor is itself provenance data from Core, not a proof of the described statement.
Corresponding Lean step
structure GuidedTiltContract where; listed fields
2. Provide defaults and routine data operations
Any listed defaults are filled when omitted. Derived representation and decidable equality let the program display and compare records; they compare data and do not decide analytic truth.
Corresponding Lean step
field defaults; deriving Repr, DecidableEq
Lean statement · GuidedTiltContract
This declaration introduces a record type. Its 6 fields are descriptions, provenance and a status label, not mathematical objects satisfying the written claim.
Braces mark parameters Lean can infer; square brackets request structures such as a measurable space or probability measure. Named hypotheses are mathematical premises, not facts established by this declaration. Section parameters are described in the mathematical hypotheses above; the module link retains their exact source context.
structure GuidedTiltContract where
basePath : String
guideName : String
guidedPath : String
terminalTarget : String
source : SourceAnchor
status : ProofStatus := ProofStatus.contractOnly
deriving Repr, DecidableEq
/-- Source-cited interface for the Donsker--Varadhan entropy duality formula.
This is data, not a proof. It records the exact analytic shape needed by the
SALD paper before theorem-specific finite-log-mgf witnesses instantiate it.
-/Lean construction · GuidedTiltContract
There is no theorem proof here. The body declares the fields and their defaults; derived display and equality support are ordinary operations on that data.
Braces mark parameters Lean can infer; square brackets request structures such as a measurable space or probability measure. Named hypotheses are mathematical premises, not facts established by this declaration. Section parameters are described in the mathematical hypotheses above; the module link retains their exact source context.
structure GuidedTiltContract where
basePath : String
guideName : String
guidedPath : String
terminalTarget : String
source : SourceAnchor
status : ProofStatus := ProofStatus.contractOnly
deriving Repr, DecidableEq
/-- Source-cited interface for the Donsker--Varadhan entropy duality formula.
This is data, not a proof. It records the exact analytic shape needed by the
SALD paper before theorem-specific finite-log-mgf witnesses instantiate it.
-/Scope and omitted-condition boundaries
- Contracts and obligation/interface constructors store strings and status labels. They are not propositions asserting the written mathematics and supply no Lean proof of it.
- It proves neither finite normalizer nor target correctness and does not construct the tilted law.
Source and reuse
ASTIS parents called
Mathlib API called (external library)
No direct Mathlib call recorded; see the ASTIS parents.
Mathematical sources
- Exact existing ASTIS declaration and body — Directly read local source; not a new proof or source-fidelity verdict.
- AutoSamplingTheory.SourceAnchor — Core workflow metadata type, not an analytic theorem.
- AutoSamplingTheory.ProofStatus — Core workflow metadata type, not an analytic theorem.
ASTIS prose is not a quotation or a source-equivalence certificate. Definitions and aliases are explained as constructions, not counted as new mathematical proofs.