Overview🔗

This section establishes proof patterns for mathematical statements and contracts about executable Lean definitions. These patterns implement the theorem-backed-claims principle from Section 1.

3.1 What Must Be Proven🔗

Requirement: Every material property claimed as established about a mathematical model or executable Lean definition MUST have machine-checked evidence from its type, proof-bearing construction, or a supporting theorem. State assumptions and open targets separately (§3.10).

Claim-Specific Proof Obligations: Apply the following obligations where required; they do not demand a separate theorem for every category.

1. Admission and Invariant Preservation: Establish the unary invariant at admission and every write/update by proof-bearing results or justified raw representation contracts of §1.1. Conditional preservation alone does not establish admission.

2. Totality: State the function’s domain and encode any promised restriction in its API. Distinguish a total logical definition from termination of its execution (§3.2.1).

3. Termination: Recursion presented as terminating requires structural or well-founded justification or another checked termination argument. Classify other recursion mechanisms explicitly (§3.6).

4. Composition Properties: Prove the claimed relations over transitions, reachable states, histories, or resource use. Include initialization, preservation, and composition where needed to derive the claim. A state invariant alone does not establish how an output relates to an input or history.

5. Impossibility Results: Use the type or a theorem to establish that the states a claim excludes cannot occur.

Example - An Intrinsic Invariant and Its Consequences:

The theorem comp_activeProposals_le_participants follows from the result type: every returned SystemState carries its bound. The functions are total in Lean’s logic. This theorem establishes no relation between inputs and outputs beyond the invariant. It does not provide an execution time bound or connect to an external process (module 1 §1.6).

3.2 Proof Patterns🔗

Pattern: Structure proofs to be both correct and comprehensible, following established patterns for common proof obligations.

Core Patterns:

1. Totality and Termination by Construction: Use structural or well-founded recursion for terminating definitions; distinguish other computation mechanisms explicitly (module 7 §7.6).

2. Property-Based Testing as Refutation Aid: Use optional counterexample search to diagnose false candidates; a passing sampled run is not a proof (§3.2.2).

3. Typeclasses for Lawful Abstractions: Generic interfaces with proven laws, held in the operational class or in a Prop-valued lawful mixin (§3.2.3).

4. Decidability: Distinguish logical decidability from executable decision procedures (§3.2.4).

5. Proof Economy: Separate elaboration, proof-artifact, kernel-replay, and native-execution cost; inspect the resulting dependencies rather than inferring trust from speed (§3.2.5).

fail to show termination for
  loop
with errors
failed to infer structural recursion:
Cannot use parameter n:
  failed to eliminate recursive application
    loop (n + 1)


failed to prove termination, possible solutions:
  - Use `have`-expressions to prove the remaining goals
  - Use `termination_by` to specify a different well-founded relation
  - Use `decreasing_by` to specify your own tactic for discharging this kind of goal
n : Nat
⊢ n + 1 < n

Tactic `decide` proved that the proposition
  0 < 0
is false

Fields missing: `enhance_increases`, `diminish_decreases`, `measure_monotone`

failed to synthesize instance of type class
  Economy.LawfulFlourishable α

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

Tactic `decide` failed for proposition
  Economy.sumWf 10 = 55
because its `Decidable` instance
  instDecidableEqNat (Economy.sumWf 10) 55
did not reduce to `isTrue` or `isFalse`.

After unfolding the instances `instDecidableEqNat` and `Nat.decEq`, reduction got stuck at the `Decidable` instance
  match h : (Economy.sumWf 10).beq 55 with
  | true => isTrue ⋯
  | false => isFalse ⋯

3.3 Elaboration-Time Verification🔗

Requirement: Express the properties an interface enforces in its types and proof obligations, and ensure the resulting terms are kernel-checked. Elaboration constructs those terms and reports unsolved obligations. This checks the program’s reasoning before execution; validating runtime inputs may still require runtime computation.

Strategies:

1. Dependent Return Types: Functions return proofs along with values.

2. Propositions as Types: Encode requirements in type signatures.

3. Indexed Bounds: Use types such as Fin n to require evidence of a bound; n and the index may be runtime inputs.

4. Witness Types: Return evidence of properties, not just boolean checks.

Example - Proof-Requiring Interfaces (these definitions use computable operations):

In findPositive and compare, the search or comparison still executes when the inputs arrive at runtime; the proof fields are erased. findPositive’s return type establishes soundness of a successful result but does not promise success whenever the list contains a positive value. Likewise, ValidTransition describes allowed edges; it does not require callers to use the latest state.

3.4 Foundation Strength: Axioms Are Reported, Never Assumed🔗

Requirement: A conforming proof surface contains no project logical axiom declarations and no sorry, admit, or transitive dependence on sorryAx. Domain assumptions are explicit parameters, hypotheses, or proof-bearing fields. Lean 4 has no constant command. Implemented opaque declarations are classified separately (§3.6).

What a theorem does transitively use of Lean's standard logical axioms is not hidden: it is reported, exactly, per declaration. The report is a dependency statement, not a quality ranking (module 4 §4.5).

• Foundation profiles — kernel-only, choice-free, standard-logical — are defined precisely in module 4 §4.5. The shipped gate (module 7 §7.5) computes each declaration's exact transitive axiom set and its profile mechanically, including through Mathlib dependencies.

• Compiler-trusting proof mechanisms generate axioms outside the permitted standard logical set. They are classified separately and rejected from conforming positive surfaces. They are never folded into a foundation label (module 7 §7.5).

3.5 Theorems Worth Proving🔗

Principle: Prove the theorems the development’s claims need. Explain each theorem’s mathematical purpose or intended use in its docstring. An unresolved obligation must remain explicitly open or conditional; it must not appear as a completed theorem with sorry or admit. Whether proof terms are erased during compilation is a separate question.

Documentation pattern: State why the result matters, its assumptions, and the exact conclusion. For example, runChecked_compose_success in §3.7 explains how a successful prefix supplies the state its suffix requires. Its theorem names the actual runner and the hypotheses under which the composition succeeds.

It is acceptable to defer a theorem when no current claim needs it. Its statement may remain as an explicitly open Prop definition or a hypothesis in a conditional result (§3.10); it must not be presented as proved.

3.6 Contracts for Executable and Effectful Mechanisms🔗

Requirement: Every material behavior claimed for an owned executable component has explicit contracts checked against its actual Lean definitions. Each contract states exactly the guarantee its mechanism provides on the pinned toolchain. Executable partiality, logical opacity, and unsoundness are different properties and MUST NOT be conflated. This includes optimizations: an optimized implementation MUST meet the same contract, so an optimization preserves the intended result, input domain, error behavior, and relevant ordering of effects; a faster implementation of a different specification is not an optimization of the original contract.

What each mechanism guarantees on the pinned toolchain:

• Total definitions, including recursion accepted by structural or well-founded termination checking: kernel-checked definitions, total in Lean's logic, open to equational reasoning. Termination-as-checked is not a complexity bound and not a runtime guarantee (§3.2.1).

• Noncomputable definitions: code generation is omitted for these declarations; the modifier adds no logical axiom by itself. A noncomputable reference alone supplies no executable witness. An executable implementation or compiled caller may be related to that reference by checked correspondence, while replacement and external execution retain their stated trust boundaries (§3.2.4).

• Pure monadic code (StateM, ReaderT, Except, ...): ordinary total functions; proofs reason by ordinary reduction (example below).

• IO and runtime execution: an IO α value is a program description run by Lean's runtime. Lean theorems cover the pure core and relations between programs; a theorem about a program or effect model does not by itself establish what happens in the outside world. A conforming executable claim names the split (example below).

• partial: executable recursion without a kernel termination proof. The logical-facing declaration is opaque (#print shows opaque f; the kernel does not unfold calls) and the mechanism introduces no new logical axiom; dependencies of its type and implementation still require inspection. Opacity is not unsoundness, and an opaque constant proves nothing about its own executions. partial is excluded from conforming proof surfaces (module 7 §7.6).

• partial_fixpoint (present on the pinned toolchain): a termination clause that, for supported result domains and with checked monotonicity in recursive calls, accepts a potentially non-terminating recursive equation as a safe def, generating one-step unfolding theorems (f.eq_def) from a choice-dependent fixpoint construction. The definition is logically sound within the standard axioms, but kernel reduction does not follow the recursive equation; proofs use the generated equations. Its execution may not terminate. This mechanism is outside the current conforming recursion surface: its generated partial helper does not meet the structural or well-founded authentication required by module 7 §7.4. This restriction is a standard/checker policy, not a claim of logical unsoundness.

• unsafe: excluded from safe kernel declarations — the kernel rejects a safe declaration that references it — and intended for compiled execution; excluded from conforming proof surfaces (module 7 §7.6).

• @[implemented_by]: kernel reasoning uses the reference definition while compiled execution runs the replacement. The correspondence is checked only when a Lean theorem states it (f = g, or pointwise, e.g. ∀ xs, f xs = g xs); otherwise the replacement is a trusted boundary.

• @[csimp]: prefer this proof-backed optimization when the pinned compiler's supported constant-equality form fits. An unconditional equality @reference = @replacement lets compilation replace occurrences without changing kernel reduction. The equality relates the Lean constants; it does not verify an extern, unsafe implementation, or further replacement reached from the target. Imported and chained transformations belong in the separate execution account (§7.6), including choices subsequently overwritten or scoped away. The attribute acts only in the compiler: kernel reduction, decide cost, and the logical definition the theorems are about are unchanged (§3.2.5).

• @[extern] / FFI: executed behavior comes from external code the Lean declaration does not establish — always a trusted boundary. Primitives resolved from the pinned toolchain's own Init, Std and Lean modules (for example Float arithmetic) are the toolchain's trusted base, as are the replacements and unsafe or partial implementations those modules declare; they are reported as what they are, neither confused with project boundaries nor presented as kernel-checked correspondence.

Continuing services and streams: A continuing service is not required to terminate, and its safety contract does not ask it to. Conforming forms include invariant preservation over arbitrary finite execution prefixes and partial correctness (every produced result satisfies the postcondition). Both are statable over total definitions, as the example below shows. Termination, productivity, progress, and liveness are distinct claims. When claimed, each carries its own stated hypotheses (scheduling or fairness assumptions as explicit parameters) and is never read out of a safety theorem.

Metaprograms: A metaprogram has two distinct objects: the terms it produces, which the kernel checks independently of how they were generated, and the producer's own behavior (which declarations it emits, which goals it closes), which kernel checking of the products does not establish. A sound resulting proof does not prove the producer correct. Claims about the producer are executable Lean definition claims with their own contracts.

Models of effects: proofs about models of effects — a modeled file system, a modeled network — are theorems about the model, distinct from guarantees about the external world. Assumptions are explicit parameters, hypotheses, or proof-bearing interfaces (§3.4), never project logical axioms.

Checker alignment: Foundation labels report transitive logical axiom dependencies (module 4 §4.5). The declaration gate separately computes an execution-coverage account for each owned executable root using the conservative closure defined in module 7. That account distinguishes retained execution edges, candidate transformations, and checked, trusted, or unresolved boundaries. A logical profile pass is not an execution guarantee: an unresolved boundary blocks the affected execution claim, and a trusted boundary must not be presented as unconditionally checked.

Example — Proof-Backed Compiler Optimization:

This theorem proves function equality for every Nat, using funext and Nat.add_comm. It does not establish a speed improvement. Both definitions use trusted native natural-number arithmetic when compiled.

Example - Pure Monadic Code Reasons by Ordinary Reduction:

Example - Safety Over Arbitrary Finite Prefixes (a continuing service):

The authoritative definitions and universal proofs are in audit/Audit/Server.lean. Glossary.Server carries served ≤ cap; init constructs an idle value for every capacity, and validate admits exactly valid raw counts. Its public constructor requires the same proof, so it enforces validity without claiming construction is exclusive to validate.

run_bounded combines the output proof field with run_cap, proved by induction over run. It covers every n : Nat and admitted s : Server, including values constructed directly with a proof. step_served establishes the exact increment/refusal behavior; the bound alone would also allow an idle implementation. These theorems do not establish liveness, productivity, external service behavior, or a rule requiring callers to use the latest state. Reusing a saved immutable value is well-typed. Any stronger usage guarantee must be proved over the actual transition or trace semantics. Each finite run is total; it is not a whole-process termination claim.

Direct invalid construction and an invalid update both fail at their proof obligation:

Tactic `decide` proved that the proposition
  1 ≤ 0
is false

Tactic `decide` proved that the proposition
  1 ≤ (Glossary.Server.init 0).cap
is false

Raw counts also cannot be passed directly to the admitted-state API:

Application type mismatch: The argument
  raw
has type
  Nat × Nat
but is expected to have type
  Glossary.Server
in the application
  Glossary.Server.step raw

3.7 A Compositional Method for Complete Program Contracts🔗

A type invariant describes valid results; a functional contract also relates them to the input. For each owned component, state the intended relation before selecting proof tools. The obligations below apply to material claims about that component, not to unrelated mathematical definitions or every implementation helper.

Every required relation MUST be proved about the actual definitions used by the application (or transferred through exact checked correspondence). Reuse proof-bearing construction and library lemmas; do not create a parallel implementation and assume equivalence. A finite fold is total in Lean's logic; arbitrary finite-prefix safety for a continuing service does not assert process termination, progress, fairness, or liveness.

Why the invariant is insufficient. This always-rejecting implementation satisfies its refined return type but violates positive-input completeness:

The last two statements use the decision kinds of §3.8. A soundness theorem alone, ∀ n, (rejectAll n).isSome = true → 0 < n, holds of rejectAll vacuously; the sound kind also requires an input the function accepts, and rejectAll has none.

The intended admission in lean/AuditApp/Limiter.lean instead has admit_exact. For every natural capacity, a positive input returns the idle state at exactly that capacity, and zero returns none. It performs no normalization. admit_sound alone would not exclude always rejecting or substituting a different positive capacity. At the CLI boundary, requestedCapacity_exact gives the separate policy: apply Lean's String.toNat? to the first argument, default to 2 on missing/unparsable input, and ignore trailing arguments; admission then rejects parsed zero. The parser's meaning is that pinned library definition, not a theorem about terminal input or an unspecified external encoding.

Worked state/error program. The limiter carries inUse ≤ capacity. Its grant_some and grant_none prove exact increment/frame and refusal behavior; step_capacity supplies the capacity frame for release and reset as well. run_capacity and run_replicate_grant retain the total fold's frame and exact successful-burst result. run keeps going after a refused grant. The strict runChecked instead sequences checkedStep with ordinary monadic bind and stops at the first refusal.

Its stack is ExceptT Unit (StateM Limiter) Unit, which runs as Limiter → (Except Unit Unit × Limiter). State is returned on either outcome. A refused operation preserves its input state; earlier successful updates remain, and the suffix is not run (checkedStep_exact, runChecked_cons, runChecked_error). This is retention, not rollback to the script's initial state. Conversely, StateT Limiter (Except Unit) has result shape Except Unit (α × Limiter) and exposes no state on error; that type alone would not specify an application's recovery policy or undo external effects.

Fits ops l states that every grant has space at the state reached by its preceding operations, using the total step. runChecked_success is an equivalence: success occurs exactly for a fitting script, and its returned state equals run ops l. The successful prefix invariant is Fits prefix initial ∧ current = run prefix initial. runChecked_append threads that current state to the suffix on success, or retains the prefix error/state; runChecked_error identifies the successful prefix immediately before the first full grant. runChecked_capacity frames capacity in both cases, so the returned state's intrinsic bound is also relative to the original capacity.

executeChecked_exact composes admission with this runner. Main passes required_contracts to executeChecked, so required admission, update, input policy, success/refusal, and composition propositions are proof obligations about the same core it calls (§7.5). The shell describes success/refusal output using the returned result and state. The proofs do not establish terminal effects, native arithmetic correctness, complexity, empirical benefit, or external liveness. The default demonstration reaches a refusal; AuditApp.demo_checked_error derives its stopped state from the universal contract.

Choose the smallest proof interface. The Lean 4.34.0 library provides Std.Do.Triple (precondition entails weakest precondition), Std.Do.Triple.bind for composition, WPMonad instances for StateT/ExceptT, and Std.Tactic.Do's mvcgen. Use these when they simplify verification conditions; no tactic is mandatory. This example reuses the standard transformers and proves exact outcome equations by reduction and list induction, avoiding an additional predicate-transformer encoding of the same equations. For a larger monadic program, Triple.bind connects the first result's postcondition to the continuation's precondition while retaining explicit exceptional postconditions.

Local let mut, a for loop, or an efficient array representation does not itself imply external effects or unsafe execution. Inspect the elaborated total function and prove its relation; efficient representations remain permitted with their boundary/correspondence proofs. For example, local rebinding below denotes a pure function for every Nat:

3.8 Delivering Executable Witnesses with Required Evidence🔗

When an API promises to produce a witness or make a decision at runtime, it MUST supply an executable definition and the required relation about that same definition. A theorem ∃ y, R x y establishes existence in Lean's logic; it does not by itself deliver executable data. Existential mathematical theorems remain legitimate. Likewise, a Decidable argument used for execution must have a computable producer (§3.2.4).

The public Regula.Contract import provides ExecutableContract f R : Prop, whose evidence field requires exactly R f. Its run requires that evidence and reduces to f (ExecutableContract.run_eq); compilation erases the proof. An application can use this interface or a richer one such as AuditApp.RequiredContracts.

Contract adequacy remains semantic. Replacing a required relation with fun _ => True loses that requirement. By contrast, a dependent function type may already enforce the entire intended relation: every f : (n : Nat) → {m : Nat // m = n + 1} supplies the stated successor property. Such evidence by construction is sufficient for that claim. Require additional input, success/refusal, frame, or composition relations only where the intended behavior needs them (§3.7).

An executable may have a classical correctness proof under Standard-Logical. Proof erasure does not turn its runtime data into a noncomputable construction:

The classical proof here deliberately illustrates the distinction; the direct proof ⟨fun _ => rfl⟩ is simpler. The shipped standalone adopter uses that direct proof and selects Kernel-only. Its ordinary lake build also inspects registered executable roots, the selected transitive foundation profile, and execution boundaries (§7.11).

Omitting evidence while keeping the requirement fails at the proof-bearing field:

Fields missing: `evidence`

Existence evidence cannot fill a promised data result:

Type mismatch
  exists_eq_add_one n
has type
  ∃ m, m = n + 1
of sort `Prop` but is expected to have type
  { m // m = n + 1 }
of sort `Type`

Using choice to extract the data makes it a noncomputable specification instead:

failed to compile definition, consider marking it as 'noncomputable' because it depends on 'Classical.choose', which is 'noncomputable'

Marking that definition noncomputable permits the logical definition; it does not deliver the executable promise. The build linter rejects a registered noncomputable root even under Standard-Logical. Conversely, classical evidence alone does not reject a computable root. Neither a successful build nor a Choice-Free label proves kernel normalization, witness extraction from arbitrary existence theorems, compiler correctness, or native/FFI behavior.