Checked example🔗

/-! # Reflexivity

Reflexivity proved through propositional extensionality. -/
theorem reflexive (n : Nat) : n = n := Eq.mp (propext (Iff.rfl : (n = n) ↔ (n = n))) rfl

reflexive (theorem) [Prop] type=∀ (n : Nat), n = n axioms=["propext"] -> choice-free

  /-! # Reflexivity
  
- Reflexivity proved through propositional extensionality. -/
- theorem reflexive (n : Nat) : n = n := Eq.mp (propext (Iff.rfl : (n = n) ↔ (n = n))) rfl
+ The same universally quantified reflexivity with an empty axiom set. -/
+ theorem reflexive (n : Nat) : n = n := rfl

/-! # Reflexivity

The same universally quantified reflexivity with an empty axiom set. -/
theorem reflexive (n : Nat) : n = n := rfl

The correction proves the same universally quantified reflexivity with an empty axiom set, under the unchanged Kernel-only claim, instead of routing through propext.

Checked by a fresh single-file audit of <example>/Fixture.lean (axiomGate --file, claim kernel-only, execution checked): violating run rejected, corrected run completed.

How to fix it🔗

1. Find the axiom that raises the label in the diagnostic's axiom list, then find the lemma or tactic that introduces it (for example simp lemmas using propext, or classical reasoning using Classical.choice).

2. Prove the statement constructively or with a narrower lemma so the exact set fits the claim.

3. If the stronger foundation is intended, change the surface's claim and rationale explicitly; this changes the published claim and needs review.

4. lake lint groups a declaration Lean generated under the one it came from if it is a constructor; projection; recursor such as casesOn; equation lemma; reserved name such as f.induct; matcher; fixpoint helper; structural helper; auxiliary declaration such as f._proof_1; constructor lemma; type construction; field default; recursion helper f._unsafe_rec. Other declarations keep their own location. Fix the one reported or a definition it uses that adds the axiom.

Why it matters🔗

A profile claim tells readers which logical principles every result on the surface may use. One declaration above the bound makes the claim false for the whole surface.

What triggers it🔗

Each declaration receives the least label containing its exact axiom set. If that label exceeds the surface maximum, the declaration is rejected with applicability label-exceeds-claim.

The exact axiom set is computed in the kernel that replayed the declaration (RG2005), as for RG1002: the axioms reached through the types and values of the constants it uses and the constructors of each inductive type. It is not the table of axioms that each module records when compiled, which #print axioms reads for an imported declaration.

The three logical labels are Kernel-only (no axioms), Choice-Free (a subset of propext and Quot.sound) and Standard-Logical (additionally Classical.choice). A surface's claim in foundation_manifest.json is the upper bound; each declaration is labeled from its own exact axiom set.

Required proof shape🔗

The replacement proves the same proposition. Classical, erased proofs are permitted when the surface claims Standard-Logical; executable behavior is a separate account (RG1007, RG3001, RG3002).

What a passing result establishes🔗

Every declaration's exact axiom set is within the selected surface maximum.

It does not establish:

• Which label a declaration should have: the claim is a project decision, reviewed with its rationale.

It leaves these review obligations open: R-QUALIFY.

Configuration and exceptions🔗

The surface maximum is the claim of its entry in foundation_manifest.json; axiomGate --file F --claim PROFILE audits one file under an explicit profile. In the editor, regula.localFoundation selects local feedback only.

Limitations and unsupported cases🔗

The label is computed from the exact transitive set; a proof that merely could avoid an axiom still carries it until rewritten.

The table Lean records for a module can omit axioms that a declaration reaches: the pinned Lean 4.34.1 records no axiom for Float, whose constructor's type reaches propext and Quot.sound. #print axioms can then show a smaller set, and a lower label, than the checker, and the audit reports the omission (RG2005). The editor, which has no replayed kernel, reads that table.

Sources🔗

Normative clauses

standard §7.5 Proof Completeness and Foundation Strength

Checklist rows

FOUND-03, FOUND-04, BUILD-02, THEOREM-01, THEOREM-10, BUILD-01

Detector, policy and proof sources

lean/RegulaPolicy/Domain.lean, lean/RegulaPolicy/Foundation.lean, lean/RegulaCore/Policy.lean, lean/RegulaPolicy/KernelAxioms.lean, website/RegulaStandard/MathematicalFoundations.lean

Proved linkage

The shared declaration decision RegulaPolicy.declarationFailure (its first failed requirement, declarationFailure_ordered) is mapped to a rule by the injective Regula.ruleForFailure. Project, file and documentation audits run it through Regula.Checker.Policy.checked_memberRule (ruleForMember_eq); the editor runs Regula.Linter.checked_editorDecision. For the same member and request, the editor passes exactly when the project decision selects no rule or only RG1008, which the editor does not render (Regula.Checker.Policy.editor_decision_none_iff), a rule it renders is the project decision's rule (editor_decision_rule), and a pending result withholds a project rule whose failure needs generated-role evidence (editor_decision_pending). The editor's request domain is the project's without teaching (editor_request_sound, editor_request_complete). The observed declaration fields and generated-role evidence are hypotheses of these theorems.