Checked example🔗

/-! # Reflexivity

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

reflexive (theorem) [Prop] type=∀ (n : Nat), n = n axioms=["sorryAx"] -> hole

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

/-! # Reflexivity

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

The correction fills the same reflexivity proof with rfl. The checked violation records Lean's original sorry warning as well; the corrected file passes the ordinary warning-rejecting gate.

Checked by a single-file policy inspection of <example>/Fixture.lean that keeps Lean's original compiler warning: violating run rejected, corrected run completed.

How to fix it🔗

1. Replace the sorry or admit with a complete proof.

2. If the hole comes from an imported declaration, fix or replace that dependency; imported holes are not exempt.

3. For an open target, write def Target : Prop := … and prove Target → Result, which states exactly what is established.

Why it matters🔗

sorryAx proves every proposition. A declaration that depends on it has no evidence, even if Lean elaborated the file, and every theorem that uses it inherits the gap.

What triggers it🔗

The checker computes the exact transitive axiom set of every owned declaration with Lean's collectAxioms. If sorryAx belongs to it, the declaration is rejected with applicability hole.

Theorems, proof-valued definitions and instances, and data definitions are all inspected; alternate syntax (admit, a tactic sorry) is caught because the kernel term contains sorryAx.

Lean itself warns declaration uses 'sorry' by default, and an elaboration error recovered as sorry is an error. In lake lint, axiomGate and the build-lint policy target that warning or error stops the audit at the warning-free build check before policy inspection, so an owned sorry in a claimed module is reported as RG2003 and the result is INCOMPLETE (lake lint exit 3); a single-file axiomGate --file F --claim P audit reports it as a RG2003 violation. This rule's own finding appears in the editor, in a file audit without --claim (which does not reject warnings), and in project and claimed-file audits when no warning was emitted (for example a hole inherited from an imported declaration, or set_option warn.sorry false, which does not waive the rule).

Required proof shape🔗

The completed declaration keeps the same statement. Weakening the proposition until it is easy to prove changes the requirement and is a semantic review failure, even though this rule then passes.

What a passing result establishes🔗

No owned declaration of the checked scope has sorryAx in its exact transitive axiom set.

It does not establish:

• That the completed proof proves the intended statement; the proposition itself is reviewed against its intent.

• Lean's own warning for sorry is a separate compiler diagnostic (RG2003); this rule does not depend on it, and disabling that warning does not waive this rule.

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

Limitations and unsupported cases🔗

In the editor the rule is reported for completed declarations of the current snapshot. A cancelled collection reports nothing for that declaration; a failed one is reported as RG2005 (incomplete), never as an invented RG1002.

The checked example comes from a diagnostic single-file inspection that keeps Lean's sorry warning as related evidence and continues to policy inspection; the ordinary project commands stop earlier with RG2003, as described above.

Sources🔗

Normative clauses

standard §7.5 Proof Completeness and Foundation Strength

Checklist rows

FOUND-02, THEOREM-06, TYPE-04, THEOREM-01, THEOREM-09, BUILD-01

Detector, policy and proof sources

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