Checked example🔗

theorem reflexive (n : Nat) : n = n := rfl

module-documentation: add a module doc comment describing this module

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

/-! # Reflexivity

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

The correction adds module documentation to the unchanged reflexivity evidence.

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

How to fix it🔗

1. Add /-! # Title … -/ as the first command after the imports.

2. In a module file, move the module docstring above @[expose] public section or public section.

3. Delete the second copy of a repeated import; public import A and import all A are different imports.

4. Follow the template in standard §5.3: a # title and summary, main declarations with their results and hypotheses, assumptions and dependencies, design notes. Keep only sections that help.

Why it matters🔗

Module documentation tells a reader which declarations carry the module's claims and under which assumptions, so the claims can be reviewed without reading every proof. The Lean community puts it first, where readers and tools look. A repeated import adds nothing and obscures which dependencies a module declares.

What triggers it🔗

When a claimed module finishes elaborating, the checker asks Lean for its module documentation and parses the module's header and first command from its source with Lean's own parser. The proved decision RegulaPolicy.ModuleHeader.failures then rejects, with applicability module-documentation, a module without module documentation; a module whose first command after the imports is not a module docstring (for example @[expose] public section or a declaration; a set_option … in prefix, the community's form for a Verso module docstring, is read through); and each import that occurs twice with the same public, meta and all modifiers. Empty modules are included.

What a passing result establishes🔗

Every claimed module has module documentation, its first command after the imports is a module docstring, and its header repeats no import.

It does not establish:

• That the documentation identifies all material declarations and assumptions, or describes them faithfully (R-DOC). Presence and position say nothing about content; no section layout is imposed.

• Import minimality: an unused or transitively redundant import that is not repeated is not reported.

It leaves these review obligations open: R-DOC.

Limitations and unsupported cases🔗

The editor reports this rule only when the module has finished elaborating without errors; a module with elaboration errors gets RG2005 (incomplete) instead.

Sources🔗

Normative clauses

standard §5.3 Module Documentation, standard §6.4 Import Discipline

Checklist rows

DOC-01, DECL-01

Detector, policy and proof sources

lean/RegulaPolicy/ModuleHeader.lean, lean/Regula/Linter/Documentation.lean, lean/Regula/Checker/AxiomGate.lean, website/RegulaStandard/DocumentationStandards.lean

Proved linkage

RegulaPolicy.ModuleHeader.failures_eq_nil_iff and mem_repeated_iff, and Regula.Checker.Acceptance.modulePresence_iff and documentationPresence_modes. Parsing the module header is operational.