This page documents Regula 0.4.1. The latest release is Regula 0.11.1: this page in Regula 0.11.1.

RG4002: Positive examples require warning-free elaboration and admission🔗

Category Documentation
Scope documentation fence
Subreason positive-example

A positive Lean fence in the documentation did not elaborate verbatim and warning-free, or it did and then failed admission or the declaration and axiom rules.

What to do. Make the example correct as printed: fix its errors or warnings, and make its declarations satisfy the same rules as project code.

Requirement: An unmarked lean fence in the checked docs elaborates verbatim and warning-free and passes the declaration and axiom rules.
Reported in: Docs examples
Enforcement: Strict, like every rule: see how rules are enforced.

Checked example🔗

Violating input

✗ Rejecteddocs/Example.mdsource examples/rules/RG4002/Violation.md

```lean
/-! # Reflexivity

Reflexivity for every natural number. -/
axiom reflexive (n : Nat) : n = n
```

Findings of the violating run

RG4002 error violation documentation example

Subject Example.md:1 at project Example.md:1

project-axiom: reflexive axioms=[`reflexive]

RG1001 error violation documentation example, claim standard-logical

Declaration reflexive at docs/Example.md:1#lean-snippet, line 4, column 7

project-axiom: reflexive axioms=[`reflexive]

Correction

Change to docs/Example.md

  ```lean
  /-! # Reflexivity
  
  Reflexivity for every natural number. -/
- axiom reflexive (n : Nat) : n = n
+ theorem reflexive (n : Nat) : n = n := rfl
  ```

✓ Passesdocs/Example.mdsource examples/rules/RG4002/Fixed.md

```lean
/-! # Reflexivity

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

The correction proves the same reflexivity claim in the positive fence; the violation reports the RG1001 underlying rejection alongside RG4002.

Checked by a documentation fence audit of <example>/docs: violating run rejected, corrected run completed.

How to fix it🔗

Fix the underlying finding shown with this diagnostic (for example prove the statement instead of declaring an axiom).
If the example is meant to fail, mark it with an exact lean-fail marker instead (RG4003).
Import what the example needs inside the fence; the checker inserts nothing.

Why it matters🔗

Readers copy documented examples and trust them. A positive example that does not elaborate, or that proves its claim with an axiom, teaches a false claim.

What triggers it🔗

Each positive fence is elaborated exactly as printed, with no inserted imports or wrappers, against a fresh build of the claimed libraries. It must be warning-free, pass checked admission, and pass the declaration and axiom rules under Standard-Logical. The fence failure is reported here together with the underlying finding (for example RG1001 for an axiom in the example).

A fence that fails without a source diagnostic (for example a worker that stopped before completing) is reported as INCOMPLETE, not as a violation.

Required proof shape🔗

The fence proves exactly the claim the surrounding prose states. A narrower foundation or an execution claim in the prose needs its own evidence; fence success establishes only Standard-Logical admission.

What a passing result establishes🔗

The positive fence elaborated verbatim, warning-free, passed owned admission and the declaration and axiom rules.

It does not establish:

That the prose describes the fence faithfully (R-DOC, R-INTENT), or any narrower foundation claim.

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

Configuration and exceptions🔗

No marker makes a failing positive example acceptable; changing it to lean-fail changes what the documentation claims.

Run lake exe docFenceAudit.

Limitations and unsupported cases🔗

Examples are checked under the declared toolchain only.

Sources🔗

Normative clauses: standard §7.7 Check Lean Documentation Verbatim
Checklist rows: DOC-04
Detector, policy and proof sources: lean/Regula/Checker/Documentation.lean, lean/Regula/Checker/SourceAudit.lean, lean/Regula/Checker/Admission.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. An accepted run satisfies RegulaPolicy.ExampleExpectationOK, and incomplete_example_refused refuses an incomplete example.