Checked example🔗

/-! # Identity

Identity on natural numbers. -/
/-- The identity function on natural numbers. -/
unsafe def identity (n : Nat) : Nat := n

identity (def) [unsafe] type=Nat → Nat axioms=[] -> kernel-only

  /-! # Identity
  
  Identity on natural numbers. -/
  /-- The identity function on natural numbers. -/
- unsafe def identity (n : Nat) : Nat := n
+ def identity (n : Nat) : Nat := n

/-! # Identity

Identity on natural numbers. -/
/-- The identity function on natural numbers. -/
def identity (n : Nat) : Nat := n

The correction keeps identity's domain and body and removes the unnecessary unsafe marker.

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. Remove an unnecessary unsafe marker.

2. Replace partial def by a definition with structural recursion or a termination_by measure and decreasing_by proof.

3. If the computation must stay unsafe or partial, move it to a separate, unclaimed dependency package; a claimed module cannot import an excluded module of its own package (RG2004). Where a claimed executable reaches it, it is reported as a trusted unsafe-computation or partial-computation boundary, which fails under checked execution (RG3002).

Why it matters🔗

A positive proof surface must consist of kernel-checked definitions. Unsafe and partial code can be executed, but it cannot serve as logical evidence, and reasoning about it silently depends on its runtime behavior.

What triggers it🔗

Authored unsafe and partial declarations are escape hatches: an unsafe declaration is checked only in Lean's unsafe mode, cannot be used by safe declarations or proofs and is not replayed as logical evidence, and a partial definition has no termination proof. They are rejected with applicability escape-hatch.

The only exception is the range-less partial helper Lean generates for a safe, termination-checked recursive def, admitted when every condition of standard §7.4 holds, including fresh-frontend attribution of the exact source.

Required proof shape🔗

A total replacement keeps the same domain and result type; if it changes behavior, state and prove the relation to the intended function.

What a passing result establishes🔗

No authored unsafe or partial declaration is on the claimed surface; every admitted generated helper satisfied all §7.4 conditions.

It does not establish:

• That unsafe or partial code elsewhere is logically unsound; the rule concerns evidence, not a claim that such code is wrong.

• Termination proofs' adequacy for cost claims.

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

Configuration and exceptions🔗

partial_fixpoint helpers are not covered by the recursive-helper exception.

Limitations and unsupported cases🔗

The helper exception is conservative: elaborators defined in the audited module, run_tac or by_elab in the recursion's proofs make the checker reject a definition Lean accepts.

Editor feedback may be pending until the project command completes the fresh-frontend check.

Sources🔗

Normative clauses

standard §7.4 Inventory Every Owned Declaration

Checklist rows

COMP-02, THEOREM-05, THEOREM-01, DECL-03, BUILD-01

Detector, policy and proof sources

lean/RegulaPolicy/Decision.lean, lean/Regula/Checker/Frontend.lean, lean/RegulaCore/Policy.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. RegulaPolicy.authorizedUnsafeRecHelpers_iff characterizes the authenticated recursion helpers.