Checked example🔗

/-! # Reflexivity

Reflexivity for every natural number. -/
axiom reflexive (n : Nat) : n = n

reflexive (axiom) [AXIOM, Prop] type=∀ (n : Nat), n = n axioms=["reflexive"] -> unknown-axiom

  /-! # Reflexivity
  
  Reflexivity for every natural number. -/
- axiom reflexive (n : Nat) : n = n
+ theorem reflexive (n : Nat) : n = n := rfl

/-! # Reflexivity

Reflexivity for every natural number. -/
theorem reflexive (n : Nat) : n = n := rfl

The correction proves the same ∀ n : Nat, n = n by rfl instead of assuming it, under the unchanged Kernel-only claim.

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. If the statement is provable, prove it: replace axiom name : P by theorem name : P := proof.

2. If it is a genuine assumption of a model, make it a parameter: theorem result (h : P) : Q, or a field of a structure that bundles the model and its laws.

3. If it states an open research target, define it as a Prop (def Target : Prop := P) and state results conditionally on it; do not assert it.

Why it matters🔗

An axiom extends Lean's logic for everything that imports it. An assumption that is false, or inconsistent with other axioms, makes every downstream theorem vacuous, and the kernel cannot tell. A hypothesis keeps the assumption visible in each theorem's type, so every use must supply it.

Lean 4 has no constant command; an opaque definition with a body is kernel-checked and is classified separately, not as an axiom.

What triggers it🔗

The checker inspects every constant attributed to an owned module in the completed Lean environment. A ConstantInfo.axiomInfo there is rejected with applicability project-axiom.

The rule applies whether or not any other declaration uses the axiom, and to private, protected, internal-looking and generated names alike. A name or namespace never exempts it.

Required proof shape🔗

A conditional result must carry the assumption in its type, for example ∀ (h : P), Q, so the exact theorem statement shows what it depends on. Its transitive axiom set must then fit the surface's foundation profile.

What a passing result establishes🔗

No owned constant of the checked modules is a logical axiom (the complete inventory itself is RG2004).

The rule is evaluated from Lean's elaborated environment after checked admission, not from source text.

It does not establish:

• That the hypotheses replacing an axiom are satisfiable or appropriate: that is the claim's intent and non-vacuity review.

• Anything about axioms of imported, unowned dependencies; those are reported through the transitive axiom sets of RG1003 and RG1005.

It leaves these review obligations open: R-INTENT, R-NONVACUITY.

Configuration and exceptions🔗

Authenticated native-proof axioms generated by native_decide, decide +native, bv_decide, bv_decide? or bv_check are not project axioms: they are classified as compiler-trusting and rejected by RG1004 instead.

Limitations and unsupported cases🔗

The editor linter reports this rule for completed declarations of the current file (editorSnapshot); a clean editor buffer is not a project result.

A metaprogram that adds declarations still produces owned constants; they are inspected like authored ones.

Sources🔗

Normative clauses

standard §7.5 Proof Completeness and Foundation Strength

Checklist rows

FOUND-01, TYPE-04, THEOREM-09, THEOREM-01, DECL-03, BUILD-01

Detector, policy and proof sources

lean/RegulaCore/Policy.lean, lean/RegulaPolicy/Decision.lean, lean/Regula/Findings.lean, website/RegulaStandard/LogicProofPatterns.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 (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.