ASTIS mathematical exposition

Record the name and provenance of a measure

AutoSamplingTheory.MeasureContract · structure · Teaching coverage

Statement

This record stores descriptions of a named measure, its state space, optional density and smoothness labels, and its source. It contains no actual Measure value and no evidence that a density or regularity property exists.

\[\operatorname{fields}(\texttt{MeasureContract})=\{\texttt{name},\texttt{stateSpace},\texttt{densityName},\texttt{smoothness},\texttt{source}\}.\]

All objects and hypotheses

name has type String: required label of the measure or law.
stateSpace has type String: required description of its state space.
densityName has type String: optional density label, default empty string.
smoothness has type String: optional regularity description, default empty string.
source has type SourceAnchor: required provenance record.
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 MeasureContract 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 · MeasureContract

This declaration introduces a record type. Its 5 fields are strings and a source anchor, 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 MeasureContract where
  name : String
  stateSpace : String
  densityName : String := ""
  smoothness : String := ""
  source : SourceAnchor
deriving Repr, DecidableEq

/-- Forward KL divergence contract `KL(rho || pi)`. -/

Exact module and namespace context

Lean construction · MeasureContract

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 MeasureContract where
  name : String
  stateSpace : String
  densityName : String := ""
  smoothness : String := ""
  source : SourceAnchor
deriving Repr, DecidableEq

/-- Forward KL divergence contract `KL(rho || pi)`. -/

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.
Measure and regularity labels remain text; a record can describe an unproved object.

Source and reuse

ASTIS parents called

AutoSamplingTheory.SourceAnchor

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.

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