Samplinglib mathematical lesson

Record a log-Sobolev inequality as an obligation

AutoSamplingTheory.LSIContract · structure · Teaching coverage

Read this first

Mathematical statement

This record stores a measure label, a constant label, an inequality written as text, its source, and a status defaulting to obligation. No log-Sobolev inequality is asserted as a proposition by this structure.

\[\operatorname{fields}(\texttt{LSIContract})=\{\texttt{measureName},\texttt{constantName},\texttt{statement},\texttt{source},\texttt{status}\}.\]

Lean statement · LSIContract

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 LSIContract where
  measureName : String
  constantName : String
  statement : String
  source : SourceAnchor
  status : ProofStatus := ProofStatus.obligation
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

measureName has type String: measure label.
constantName has type String: inequality-constant label.
statement has type String: written inequality.
source has type SourceAnchor: provenance.
status has type ProofStatus: default obligation.
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 LSIContract 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 · LSIContract

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 LSIContract where
  measureName : String
  constantName : String
  statement : String
  source : SourceAnchor
  status : ProofStatus := ProofStatus.obligation
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.
No constant convention, positivity, admissible test class or validity of LSI is enforced by string fields.

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.