Record a forward-KL expression and its status
AutoSamplingTheory.KLContract · structure · Teaching coverage
Statement
This record stores labels for rho and pi, a written forward-KL expression, source provenance and a status defaulting to contractOnly. It does not define KL as an analytic functional or prove the expression correct.
All objects and hypotheses
- rho has type String: first measure label.
- pi has type String: reference-measure label.
- expression has type String: written KL expression.
- 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 KLContract 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 · KLContract
This declaration introduces a record type. Its 5 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 KLContract where
rho : String
pi : String
expression : String
source : SourceAnchor
status : ProofStatus := ProofStatus.contractOnly
deriving Repr, DecidableEq
/-- Fisher information contract `FI(rho || pi)`. -/Lean construction · KLContract
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 KLContract where
rho : String
pi : String
expression : String
source : SourceAnchor
status : ProofStatus := ProofStatus.contractOnly
deriving Repr, DecidableEq
/-- Fisher information contract `FI(rho || pi)`. -/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.
- The order rho, pi records forward KL notation but supplies no absolute continuity, finite entropy or nonnegativity proof.
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.