Samplinglib mathematical lesson

Record a forward-KL expression and its status

AutoSamplingTheory.KLContract · structure · Teaching coverage

Read this first

Mathematical 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.

\[\operatorname{fields}(\texttt{KLContract})=\{\texttt{rho},\texttt{pi},\texttt{expression},\texttt{source},\texttt{status}\}.\]

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.

Download module (.lean)

structure KLContract where
  rho : String
  pi : String
  expression : String
  source : SourceAnchor
  status : ProofStatus := ProofStatus.contractOnly
deriving Repr, DecidableEq

Exact module and namespace context

Proof roadmap

1Specify 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.
2Provide 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.

Full assumptions and notation

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.

\[\text{descriptive fields}+\text{provenance}\longmapsto\text{one record}.\]

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.

\[\operatorname{DecidableEq}(\text{records})\ne\text{decision procedure for the recorded mathematics}.\]

Corresponding Lean step

field defaults; deriving Repr, DecidableEq

Lean verification

The exact proof begins folded immediately after the mathematical argument; the statement is folded beside the claim above.

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.

Download module (.lean)

structure KLContract where
  rho : String
  pi : String
  expression : String
  source : SourceAnchor
  status : ProofStatus := ProofStatus.contractOnly
deriving Repr, DecidableEq

Exact module and namespace context

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.

Sources, dependencies, and reuse

Source and reuse

Samplinglib parents called

Mathlib API called (external library)

No direct Mathlib call recorded; see the Samplinglib 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.

Samplinglib prose is not a quotation or a source-equivalence certificate. Definitions and aliases are explained as constructions, not counted as new mathematical proofs.