Checked example🔗

import Regula.MaterialClaim
/-! # Reflexivity

Reflexivity for every natural number; `reflexive` supplies its evidence. -/
/-- Every natural number equals itself, without additional hypotheses. -/
@[regula_material] theorem reflexive (n : Nat) : n = n := rfl

material-intent: add a nonempty `# Intent` section stating the requirement this claim must meet

  import Regula.MaterialClaim
  /-! # Reflexivity
  
  Reflexivity for every natural number; `reflexive` supplies its evidence. -/
- /-- Every natural number equals itself, without additional hypotheses. -/
+ /-- Every natural number equals itself, without additional hypotheses.
+ 
+ # Intent
+ ## Requirement
+ 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
## Requirement
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 a nonempty # Intent section, structured with a ## Requirement subsection, to the registered theorem's existing docstring; the explanation, 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 # Intent with the requirement in your own words, derived from the source mathematics or program specification, not from the Lean statement.

2. Prefer a level-one heading; a top-level Verso docstring header must be #.

Why it matters🔗

The explanation states what the formal statement says; the intent states what it is required to say. Comparing the two, and both with the declaration, exposes statements that are faithfully explained but wrong (standard §5.2).

What triggers it🔗

An Intent section is an ATX heading line whose text is exactly Intent (one to six #, no closing sequence), followed before the next heading of equal or higher level by at least one non-heading line with text. Text under deeper subsection headings counts. A registered docstring without such a section is rejected with applicability material-intent.

A declaration with no docstring at all is RG5002 only; the two rules partition the failures.

Required proof shape🔗

The Intent section states the requirement the declaration must meet; review compares the two.

What a passing result establishes🔗

Every registered public material declaration's docstring has a nonempty labelled Intent section, decided by the proved classifier RegulaPolicy.materialDocumentationFailure.

It does not establish:

• That the intent states what the requirement owner needs, or that the declaration meets it (R-INTENT, R-DOC). There is no intent detector, length threshold or similarity check.

• Code fences in the docstring are not tracked: a # Intent line inside a fenced block counts as an Intent heading.

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

Configuration and exceptions🔗

The rule checks only declarations registered with @[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🔗

Setext headings and closing sequences such as # Intent # are not recognized as Intent headings.

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.2 Faithful Explanation of Formal Claims

Checklist rows

DOC-02

Detector, policy and proof sources

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

Proved linkage

RegulaPolicy.materialDocumentationFailure_eq_missingIntent_iff and RegulaPolicy.Intent.hasIntentSection_iff.