Samplinglib mathematical lesson

Record a proposed continuity-equation velocity

AutoSamplingTheory.TransportVelocityContract · structure · Teaching coverage

Read this first

Mathematical statement

This record stores a named measure path, a named velocity field, a continuity equation written as text, provenance and a default contractOnly status. It contains no analytic path or velocity value.

\[\operatorname{fields}(\texttt{TransportVelocityContract})=\{\texttt{pathName},\texttt{velocityName},\texttt{continuityEquation},\texttt{source},\texttt{status}\}.\]

Lean statement · TransportVelocityContract

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 TransportVelocityContract where
  pathName : String
  velocityName : String
  continuityEquation : 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

pathName has type String: measure-path label.
velocityName has type String: velocity-field label.
continuityEquation has type String: written continuity equation.
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 TransportVelocityContract 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 · TransportVelocityContract

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 TransportVelocityContract where
  pathName : String
  velocityName : String
  continuityEquation : 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.
A stored continuity equation does not prove weak differentiability, divergence regularity, boundary behavior or a transport identity.

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.