Overview🔗

Reuse Lean and Mathlib structures whose laws match the mathematical objects or executable program contracts being specified. State the exact foundation strength as described in §4.5.

4.1 Numeric Representations: Mathematical and Machine Arithmetic🔗

Requirement: Use a numeric representation whose semantics match the claim. For example, ℝ provides exact real arithmetic, while Float, UInt32, and BitVec n have different arithmetic semantics. A claim relating different representations MUST state and prove the correspondence under its required hypotheses.

Rationale: ℝ provides exact real-number semantics. Floating-point arithmetic rounds and includes exceptional values such as NaN and infinities. Unsigned addition and multiplication on n bits wrap modulo 2 ^ n. A theorem about real arithmetic does not establish the behavior of an unrelated machine computation. Checked correspondence connects the two when the claim needs both (module 2 §2.4).

Implementation Guidelines:

• Import Mathlib.Basic.Real.Basic when the model uses real numbers.

• Use ℝ when the claim treats time, probability, or another quantity as real-valued. Use the corresponding refined type when bounds are required.

• Use core's Rat when the claim is exact rational arithmetic: its order is decidable and its operations execute. It is not a model of the reals; a statement that needs completeness, limits or analysis requires ℝ.

• Use floating-point and fixed-width machine types when the claim is about that arithmetic, and name the semantics the claim relies on: rounding and exceptional values for Float; wrapping and bit width for machine words and BitVec; serialization when values cross a byte boundary.

• Specify an executable representation directly when its behavior is the subject of the claim. Transfer an abstract model’s result through checked correspondence to the actual implementation (module 1 §1.3).

• Discrete models, such as ℕ-based clocks and Fin n phases, also conform when they fit the claim. Supply the laws of every claimed mathematical interface.

Example - Exact Rational Quantities with a Lawful Order:

The shared Time type wraps non-negative rational numbers: exact arithmetic with a decidable order, not the real numbers. In Audit.DocClaims, DecayingValue.valueAt is the linear curve initial * (1 + decayRate * (t - startTime)), using the underlying rational values of the times. The theorem below establishes a nonincreasing curve for a negative rate. It does not establish strict decrease because initial may be zero. Its quantifiers include all ordered pairs of times, including times before startTime. That field shifts the formula rather than restricting its domain. The curve is linear, not exponential: a claim about initial * exp (decayRate * (t - startTime)) over ℝ needs Mathlib's real analysis, and the Mathlib integration package proves the same antitonicity statement for that real-valued curve.

An LE instance supplies a relation used by ≤. It provides no proofs of reflexivity, transitivity, antisymmetry, or totality, and does not provide min or max. Even when its relation has those properties, the stronger interface requires their evidence. The bare relation below therefore does not synthesize core's Std.IsLinearOrder:

failed to synthesize
  Std.IsLinearOrder T

Hint: Additional diagnostic information may be available using the `set_option diagnostics true` command.

If the prose claims that time has a linear order, supply the corresponding lawful instance (core's Std.IsLinearOrder, or Mathlib's LinearOrder in a Mathlib project) as the shared Glossary.Time does in Audit.DocPrelude.

Example - Machine Arithmetic as the Specification Object:

When the claim is about the machine arithmetic itself, the specification uses the machine type and carries its exact semantics:

The specification uses Float because the claim concerns binary64 values. Its return type excludes NaN and infinities. admitReading_eq_ok additionally establishes acceptance and preservation of every input satisfying those conditions. These properties do not establish sensor accuracy or a permitted measurement range.

On the pinned toolchain, Float wraps a logical Float.Model. isNaN and isInf have definitions over that model. Compiled calls use native implementations through @[extern]. The proof does not verify those external implementations. A real-valued interpretation of accepted readings requires the stated correspondence (module 2 §2.4).

4.2 Algebraic Structures🔗

Requirement: Reuse the matching Lean or Mathlib algebraic structure when it expresses the intended interface. Introduce a custom structure only when existing interfaces do not fit, and explain the distinction. Its claimed laws still require proofs.

Rationale: The reuse principle of module 1 §1.4, applied to algebra: a standard structure carries its theorem library and integrates with the rest of Mathlib.

Key Structures from Mathlib:

• Groups: AddGroup, AddCommGroup, Group, CommGroup.

• Rings: Semiring, Ring, CommRing.

• Orders: PartialOrder, LinearOrder, Lattice.

• On the pinned Mathlib, the following ordered-algebra interfaces combine operational classes with proof-valued mixins: AddCommGroup, PartialOrder (or LinearOrder), and IsOrderedAddMonoid for ordered additive commutative groups; Field, LinearOrder, and IsStrictOrderedRing for linearly ordered fields. The former bundled names OrderedAddCommGroup and LinearOrderedField are absent on this pin. This describes those interfaces, not a ban on bundled hierarchies.

Key Structures from Lean's Core Library:

• Order laws over the operational class LE: Std.IsPreorder, Std.IsPartialOrder and Std.IsLinearOrder, with the Prop-valued mixins Std.LawfulOrderLT, Std.LawfulOrderMin and Std.LawfulOrderMax relating <, min and max to ≤.

• Laws of a binary operation: Std.Associative, Std.Commutative and Std.LawfulIdentity.

• Std.LinearOrderPackage.ofLE builds the lawful linear-order structure of a type from its ≤, a decision procedure and the three laws Std.Total, Trans and Std.Antisymm.

Example - Canonical Orders Without Rebuilding Them:

The rank function chooses the intended ordering. The injectivity proof shows that distinct constructors receive distinct ranks. In a Mathlib project, LinearOrder.lift' transports the order and its laws along the same injective rank in one step; Glossary.Tick in the Mathlib integration package is built that way. Lean provides no deriving handler for the lawful structure:

No deriving handlers have been implemented for class `Std.IsLinearOrder`

4.3 Temporal Models🔗

Principle: Model time with the structure the claim needs — and provide the lawful structure the prose claims.

Discrete and continuous models are both conforming, as long as the order (or other) interface is complete and lawful:

The timestamp order on Event is a preorder. Two different events can share a timestamp and be ordered both ways without being equal. A partial order on Event based only on timestamps would additionally need antisymmetry, which these fields do not establish.

mem_eventsInWindow states both directions of membership: an event is retained exactly when it belongs to the input list and satisfies the window predicate. The function is executable when its supplied decision procedure is executable. The shared Time order compares rationals and is decidable, so eventsWithin is an executable caller. A real-valued time has no executable comparison: over Mathlib's ℝ the same function has only noncomputable callers, and a discrete clock or another decidable input domain serves a runtime requirement.

CausalOrder requires an irreflexive, transitive relation on the declared events. Its fields do not connect that relation to timestamps or establish any external causal interpretation. State and prove such a connection separately when claimed.

For protocol models, a discrete clock can count steps. Here ticks and phase numbers must not be interchanged. Glossary.Tick is a nominal structure with a public val : Nat field. Its Std.IsLinearOrder instance reuses the natural order and its laws through that injective projection, built by core's Std.LinearOrderPackage.ofLE. Construction and projection are explicit conversions, not an abstraction boundary.

A phase number cannot be used directly as a tick:

Application type mismatch: The argument
  phase
has type
  Nat
but is expected to have type
  Glossary.Tick
in the application
  atTick phase

If a model intentionally needs only another name for natural numbers, abbrev Tick := Nat inherits their order instances and laws but creates no semantic type distinction. An ordinary def is also definitionally equal to its body but is not unfolded by typeclass synthesis at the same transparency. Even the relation ≤ must be supplied explicitly or obtained by another deliberate transparency choice:

failed to synthesize instance of type class
  LE Tick

Hint: Type class instance resolution failures can be inspected with the `set_option trace.Meta.synthInstance true` command.

4.4 Spatial Properties🔗

Requirement: Reuse the matching Mathlib interface for the claimed geometry: for example, a metric for its distance laws or a topology for continuity. Incidence, affine, and combinatorial claims may use other structures. Require the laws the claim needs. Being geometric does not by itself require a metric or topology.

Rationale: A claim about distance or continuity needs the corresponding laws. Mathlib provides those verified interfaces, while other geometric claims may require different structures. Selecting the matching interface preserves the exact claim boundary from §1.4.

Example - Incidence Constraints on Network Edges (an incidence claim: which cells lie in which coverage zones. It needs no distance, so it uses no metric; a claim about range measures distance through Mathlib's MetricSpace ℝ, checked as MathlibModels.InRange in the Mathlib integration package):

This subtype constrains which edges may be present. It does not require every pair that shares a zone to be an edge. The empty edge relation always satisfies it. It also requires neither symmetry nor absence of self-loops. A claim of a complete zone graph or a simple undirected graph needs the corresponding definition and laws. Here NetworkTopology names a type of constrained edge relations, not a topological-space instance or a verified communication network. ShareZone states incidence only: it is not transitive when zones overlap, and it says nothing about how far apart two cells are. ShareZone.of_subset is the one law this example proves about it. A claim about distance or range needs a metric and its laws, reused from the matching interface, not defined beside the example.

4.5 Foundation Strength: Kernel-Only, Choice-Free, Standard-Logical🔗

Every Lean declaration has an exact transitive axiom set: the axioms reached through the types and values of the constants it uses, including those from Mathlib. #print axioms follows these dependencies, but for an imported declaration it reads the axiom table that the declaration's module recorded when it was compiled, and on the pinned toolchain such a table can omit axioms reached through the constructors of an inductive type. A gate therefore computes the set from the kernel-checked declarations (§7.4). This standard fixes exactly three logical foundation labels plus one non-logical classification:

Rules:

• A choice-dependent declaration is never labeled Choice-Free. The shipped gate mechanically checks a surface's claimed profile against these exact sets (module 7 §7.5).

• Standard-Logical is a permitted foundation profile. Erased mathematical proofs may use Classical.choice within that profile without making the associated program noncomputable. Select the foundation appropriate to the claim and report dependencies honestly. A smaller axiom set is useful when the interface requires it or when a simpler proof achieves it. It is not a general software-assurance ranking.

• Selecting Choice-Free limits the permitted dependencies. It is not a synonym for correctness or executable construction. Replacing a choice-dependent construction may require explicit witnesses, different operations, or weaker interfaces. Inspect the actual dependencies before deciding whether the change supports the claim.

• Importing Mathlib is not disqualifying. The transitive axiom set decides. A pure arithmetic theorem proved inside a Mathlib-importing module can still be kernel-only.

A project logical axiom, sorryAx, or an unrecognized axiom fails the conforming proof claim. Compiler-trusting mechanisms are classified separately and excluded from conforming positive proof surfaces. A generated-looking name alone does not establish a compiler origin. §7.5 defines the required classification.

Selected actual labels from this repository. An allowed maximum profile admits every subset of its permitted axioms including the empty set. An actual label is the smallest of these three profiles containing the declaration's computed set: empty is Kernel-only; a nonempty subset of {propext, Quot.sound} is Choice-Free; a permitted set containing Classical.choice is Standard-Logical. Never infer that set from a tactic name. For a theorem, its actual label does not establish that the same proposition has no proof with fewer axioms.

These assertions import the actual declarations from Basic and DocClaims; the §3.2.2 example makes the same assertion for reverse_append_eq where it is written. #guard_msgs compares each #print axioms result with its displayed expected output, so a changed set fails fence elaboration. This checks these selected dependency claims; the gate reports the complete declaration inventory with lake exe axiomGate --json-out tmp/axiom-report.json.

The label is computed per declaration, not inferred from an imported module or a type name. Core's order lemmas for Rat traverse choice-dependent definitions, as do many order and analysis operations over Mathlib's ℝ. Other declarations in the same module may remain kernel-only or Choice-Free. The exact transitive set decides. Constructive alternatives can change the interface and proof obligations. They are interface decisions, not automatic conformance upgrades.

Selecting a maximum is an enforceable requirement. The opt-in build linter (§7.11) reads the surface's "claim" from foundation_manifest.json on every enabled ordinary build. Selecting "choice-free" rejects both direct and imported/transitive Classical.choice, even when the modules have cached build artifacts. Switching a surface with a covered declaration that depends on Classical.choice from "standard-logical" to "choice-free" therefore fails without any source edit. The standalone qualification includes this intended label-exceeds-claim failure, a fresh restoration, and positive controls for all three profiles. Enabled ordinary-build evidence is incremental elaboration and current policy inspection, not fresh-source conformance evidence.

This foundation condition is separate from executable construction. A Standard-Logical correctness proof may use choice while its function computes normally (§3.8). Choice-Free alone does not guarantee kernel normalization, executable witness extraction, or native execution assurance. Each requires its own precisely stated claim and evidence.