ASTIS mathematical exposition

Record a Fisher-information expression and its status

AutoSamplingTheory.FIContract · structure · Teaching coverage

Statement

This record stores labels for the two measures, a Fisher-information expression, source provenance and a status defaulting to contractOnly. It contains no gradient, density or integrability witness.

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

All objects and hypotheses

rho has type String: first measure label.
pi has type String: reference-measure label.
expression has type String: written Fisher-information 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 FIContract 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 statement · FIContract

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 FIContract where
  rho : String
  pi : String
  expression : String
  source : SourceAnchor
  status : ProofStatus := ProofStatus.contractOnly
deriving Repr, DecidableEq

/-- Log-Sobolev inequality contract. -/

Exact module and namespace context

Lean construction · FIContract

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.

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

/-- Log-Sobolev inequality contract. -/

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.
Writing a Fisher-information expression does not establish differentiability, Sobolev regularity or finiteness.

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.