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 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 - Continuous Quantities with a Lawful Order:

The shared Time type wraps non-negative real numbers. In Audit.DocClaims, DecayingValue.valueAt is initial * exp (decayRate * (t - startTime)), using the underlying real 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.

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 LinearOrder:

failed to synthesize
  LinearOrder 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 LinearOrder instance 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.

Example - Canonical Orders Without Rebuilding Them:

The rank function chooses the intended ordering. The injection proof shows that distinct constructors receive distinct ranks. The imports above do not provide a deriving LinearOrder handler:

No deriving handlers have been implemented for class `LinearOrder`

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 PartialOrder 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. Arbitrary real-time comparison in the shared Time order is noncomputable, so that order does not supply an executable caller. A discrete clock or a different decidable input domain can serve a runtime requirement.

CausalOrder requires an irreflexive, transitive relation on the declared event set. 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 LinearOrder reuses the natural order and its laws through that injective projection using Mathlib's LinearOrder.lift'. 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
  ℕ
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 LinearOrder 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. The instance must be supplied explicitly or obtained by another deliberate transparency choice:

failed to synthesize
  LinearOrder Tick

Hint: Additional diagnostic information may be available using the `set_option diagnostics 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 - Geometric Constraints on Network Edges:

This subtype constrains which edges may be present. It does not require every in-range pair to be an edge. The empty edge set always satisfies it. It also requires neither symmetry nor absence of self-loops. A claim of a complete range graph or a simple undirected graph needs the corresponding definition and laws. Here NetworkTopology names a type of constrained edge sets, not a topological-space instance or a verified communication network.

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

Every Lean declaration has an exact transitive axiom set. #print axioms reports this set by following its logical dependencies, including those from Mathlib. 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. Some order and analysis operations over ℝ traverse choice-dependent definitions. 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.