ASTIS mathematical exposition

Record a Poincaré inequality as an obligation

AutoSamplingTheory.PIContract · structure · Teaching coverage

Statement

This record stores labels and text for a Poincaré inequality with provenance and a default obligation status. It is metadata rather than a proof of the inequality.

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

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 PIContract 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 · PIContract

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 PIContract where
  measureName : String
  constantName : String
  statement : String
  source : SourceAnchor
  status : ProofStatus := ProofStatus.obligation
deriving Repr, DecidableEq

/-- Transport velocity field satisfying a continuity equation. -/

Exact module and namespace context

Lean construction · PIContract

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 PIContract where
  measureName : String
  constantName : String
  statement : String
  source : SourceAnchor
  status : ProofStatus := ProofStatus.obligation
deriving Repr, DecidableEq

/-- Transport velocity field satisfying a continuity equation. -/

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 structure does not assert a spectral gap, compare Poincaré and LSI constants, or impose a function domain.

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.