Samplinglib mathematical lesson

Record the intended labels of a guided tilt

AutoSamplingTheory.GuidedTiltContract · structure · Teaching coverage

Read this first

Mathematical statement

This record stores names for a base path, guide, guided path and terminal target together with a source and default contractOnly status. The intended exponentially tilted relationship is descriptive, not an enforced measure equality.

\[\operatorname{fields}(\texttt{GuidedTiltContract})=\{\texttt{basePath},\texttt{guideName},\texttt{guidedPath},\texttt{terminalTarget},\texttt{source},\texttt{status}\}.\]

Lean statement · GuidedTiltContract

This declaration introduces a record type. Its 6 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 GuidedTiltContract where
  basePath : String
  guideName : String
  guidedPath : String
  terminalTarget : 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

basePath has type String: base-path label.
guideName has type String: guide label.
guidedPath has type String: tilted-path label.
terminalTarget has type String: terminal target label.
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 GuidedTiltContract 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 · GuidedTiltContract

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 GuidedTiltContract where
  basePath : String
  guideName : String
  guidedPath : String
  terminalTarget : 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.
It proves neither finite normalizer nor target correctness and does not construct the tilted law.

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.