Checked example🔗

import Regula.MaterialClaim
/-! # Reflexivity

Reflexivity for every natural number; `reflexive` supplies its evidence. -/
@[regula_material] theorem reflexive (n : Nat) : n = n := rfl

material-documentation: document the claim, assumptions and evidence at this declaration

  import Regula.MaterialClaim
  /-! # Reflexivity
  
  Reflexivity for every natural number; `reflexive` supplies its evidence. -/
+ /-- Every natural number equals itself, without additional hypotheses.
+ 
+ # Intent
+ Equality on natural numbers must be reflexive for every value, with no side condition.-/
  @[regula_material] theorem reflexive (n : Nat) : n = n := rfl

import Regula.MaterialClaim
/-! # Reflexivity

Reflexivity for every natural number; `reflexive` supplies its evidence. -/
/-- Every natural number equals itself, without additional hypotheses.

# Intent
Equality on natural numbers must be reflexive for every value, with no side condition.-/
@[regula_material] theorem reflexive (n : Nat) : n = n := rfl

The correction adds the registered theorem's docstring, including its # Intent section; registration, proposition and proof are unchanged.

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

How to fix it🔗

1. Add /-- … -/ immediately before the declaration, stating purpose, domain and hypotheses, result and boundary (standard §5.1).

2. Include a # Intent section with the requirement the claim must meet (standard §5.2); a missing Intent section is RG5003.

Why it matters🔗

A material claim must be readable without reconstructing it from the proof: the docstring states what the declaration establishes and under which assumptions, and binds the written intent to that exact declaration.

What triggers it🔗

The checker selects public declarations carrying the persistent @[regula_material] registration and asks Lean for their docstrings (findDocString?, which includes inherited documentation). A registered declaration without one is rejected with applicability material-documentation.

Unregistered declarations are not selected; there is no name heuristic.

Required proof shape🔗

The docstring describes the elaborated statement faithfully.

What a passing result establishes🔗

Every registered public material declaration has a docstring.

It does not establish:

• That every material declaration is registered, or that the docstring is faithful and adequate (R-DOC); registration completeness is semantic review.

• Docstrings of unregistered declarations. Standard §6.7 requires claimed libraries to enable linter.missingDocs, whose reports RG2003 rejects; RG2006, not this rule, checks that option.

It leaves these review obligations open: R-DOC.

Configuration and exceptions🔗

Registration is @[regula_material] from Regula.MaterialClaim. Removing a registration from a material declaration changes the reviewed claim, not only this rule's result.

Limitations and unsupported cases🔗

Lean's broader linter.missingDocs reports public declarations without a docstring only where it is enabled; this rule covers registered material evidence whatever the options.

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.1 Inline Documentation Requirements

Checklist rows

DOC-01

Detector, policy and proof sources

lean/Regula/MaterialClaim.lean, lean/RegulaPolicy/Intent.lean, lean/Regula/Linter/Documentation.lean

Proved linkage

RegulaPolicy.materialDocumentationFailure_eq_none_iff, materialDocumentationFailure_eq_missingDocstring_iff and Regula.ruleForMaterialDocumentation_injective.