Checked example🔗

/-! # Dependency

Dependency reflexivity declaration. -/
namespace Dependency
axiom reflexive (n : Nat) : n = n
end Dependency

import Dependency
/-! # Inherited reflexivity

Reflexivity inherited from the dependency. -/
theorem reflexive (n : Nat) : n = n := Dependency.reflexive n

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

  /-! # Dependency
  
- Dependency reflexivity declaration. -/
- namespace Dependency
- axiom reflexive (n : Nat) : n = n
+ Dependency reflexivity evidence. -/
+ namespace Dependency
+ theorem reflexive (n : Nat) : n = n := rfl
  end Dependency

/-! # Dependency

Dependency reflexivity evidence. -/
namespace Dependency
theorem reflexive (n : Nat) : n = n := rfl
end Dependency

The examples are the imported dependency. The dependency proves the same reflexivity statement instead of declaring it as an axiom, and the file that imports it is unchanged.

Checked by a fresh whole-project audit of <example> (axiomGate): violating run rejected, corrected run completed.

How to fix it🔗

1. Inspect the declaration's axiom list in the diagnostic or with #print axioms, and follow it to the declaration that introduces the axiom.

2. Replace the axiom in the dependency with a proof, or make it a hypothesis of the results that need it.

3. If the dependency cannot change, do not claim the affected declarations on a conforming surface.

Why it matters🔗

A foundation label summarizes exactly which assumptions a result rests on. An unclassified axiom has no label, so no profile claim about the declaration can be true.

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.

What triggers it🔗

Each axiom in the transitive set is classified. One that is not a standard logical axiom, sorryAx (RG1002) or a compiler-trusting axiom (RG1004) is unknown, and the declaration is rejected with applicability unknown-axiom.

Imported axioms are not exempt: an owned theorem that uses a dependency's axiom is rejected even though the axiom is declared elsewhere.

Required proof shape🔗

After the fix, the exact transitive axiom set is a subset of propext, Quot.sound and Classical.choice and fits the surface claim (RG1005).

What a passing result establishes🔗

Every axiom in the transitive set of each owned declaration is either a standard logical axiom or rejected by a more specific rule.

It does not establish:

• Anything about the unowned dependency beyond its axioms; imported declarations are a declared trust boundary, identified by the exact dependency state (RG2001).

It leaves these review obligations open: R-QUALIFY.

Limitations and unsupported cases🔗

Classification uses exact constant names and authenticated compiler evidence, not name patterns; a lookalike name gets no special treatment.

Sources🔗

Normative clauses

standard §7.5 Proof Completeness and Foundation Strength

Checklist rows

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

Detector, policy and proof sources

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