Checked example🔗

import Regula.Report
/-! # Reflexivity

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

unexpected-project-module: checker probe module Regula.Report was imported into positive library Example by Example

- import Regula.Report
  /-! # Reflexivity
  
  Reflexivity for every natural number. -/
  theorem reflexive (n : Nat) : n = n := rfl

/-! # Reflexivity

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

The correction removes an unused forbidden reporter import; the reflexivity statement and its assumptions are unchanged.

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

How to fix it🔗

1. Delete imports of excluded modules (for example checker or fixture modules) from claimed code.

2. Use a glob with the intended meaning, such as .andSubmodules `Lib in lakefile.lean or ["Lib", "Lib.+"] in lakefile.toml, so every intended module is in the library.

3. Classify any new root library or executable in the manifest (RG2002).

Why it matters🔗

A conformance claim covers an exact set of modules. A module imported into a claimed library but outside every surface would contribute declarations nobody classified, and an umbrella import alone does not define that set.

What triggers it🔗

Module inventory comes from Lake's elaborated configuration and Lean's recorded module indices, not from file lists or name prefixes. The checker resolves each imported root-package module's origin and rejects unexpected project modules, imports of excluded modules into claimed ones, and unknown ownership (unexpected-project-module and related subreasons).

A root-package module outside every manifested library that a claimed module imports stops that environment's inspection, since kernel admission cannot classify it: the finding names the module and the modules that import it. The single-file audit (axiomGate --file) reports such an import the same way, naming the audited file by its path where it is an importer.

The impact depends on the subreason. A forbidden import or a module outside every manifested library (unexpected-project-module) is a violation (lake lint exit 1 unless the same run also has an incomplete finding). A configured module that was omitted or not freshly built, or a declaration attributed outside the claimed surface, is incomplete evidence (INCOMPLETE, lake lint exit 3).

Required proof shape🔗

The removed import must not have supplied evidence the claim still relies on.

What a passing result establishes🔗

For a project audit, the claimed modules are exactly Lake's configured modules for the claimed targets, and every owned constant is attributed to one of them.

For a single-file audit, every module the file loads from the root package's build output is a module of one of the package's Lake libraries or an executable's root.

It does not establish:

• That the chosen library boundaries are the ones the project intends to claim; that is reviewed with the manifest rationale.

It leaves these review obligations open: R-QUALIFY.

Configuration and exceptions🔗

An exclusion in the manifest never permits a claimed module to import the excluded one.

Limitations and unsupported cases🔗

The editor is explicitly partial and does not report this rule. A single-file audit reports only a module outside every Lake library that the file imports, not the whole project's inventory coverage.

Sources🔗

Normative clauses

standard §7.2 Define Surfaces Through Lake Semantics

Checklist rows

DECL-02, DECL-03, SCOPE-05, DECL-01, DECL-04, BUILD-01, BUILD-03, BUILD-04

Detector, policy and proof sources

lean/Regula/Checker/Lake.lean, lean/Regula/Probe.lean, lean/Regula/Checker/AxiomGate.lean, lean/RegulaPolicy/Plan.lean

Proved linkage

Acceptance side only: an accepted run satisfies RegulaPolicy.ScopeOK, over the surface assignments of Regula.Checker.Acceptance.checked_surfaceAssignments, and RegulaPolicy.census_covers_claimed_targets shows that every module of a claimed Lake target is a positive module of the accepted census. The inventory checks are operational.