SCOPE-01

Every normative requirement concerns Lean, dependent types, proofs, elaboration, modules, or a Lean-code claim.

Set scope

Read every normative MUST/MUST NOT; fail any generic lifecycle, release, deployment, organizational, certification, or other non-Lean mandate.

SCOPE-02

Prose states no result stronger than the exact Lean declaration it cites.

0: claim boundary, 1 §1.6

For every material claim, record the elaborated type, all quantifiers and hypotheses, and compare them with the prose conclusion.

SCOPE-03

A theorem about a model is not presented as a theorem about an unrelated implementation, runtime, or external system.

1 §1.3, 1 §1.6

Identify the exact model and implementation definitions. For distinct objects, require a checked relation sufficient to transfer the claimed property; reuse definitional equality or existing evidence where it suffices. State the external execution assumptions separately; otherwise narrow or remove the claim.

SCOPE-04

Universal rules are technical Lean rules, not arbitrary style or application-domain policy. The style, naming, and documentation-form baseline is the Lean community's, adopted by requiring its linters, not restated as rules.

1 §1.4, 6, 6 §6.7

For each universal rule, identify the precise type, proof, elaboration, resolution, module, or computation consequence. Confirm that the style, naming, and documentation-form requirements are the community's own linters (§6.7) and its guides, not conventions restated as rules of this standard.

SCOPE-05

The object and kind of every material claim are clear: abstract mathematical, executable Lean definition, refinement/correspondence, or external/effectful boundary. Combined claims keep these scopes distinct. An unresolved execution path or a partial surface presented as whole-application coverage blocks the affected claim.

1 §1.3, 3 §3.6, 7 §7.6

Enumerate the claimed surfaces and material claims. Reconcile the executable roots and boundary accounts under COMP-03, including additional registered roots under BUILD-03 where applicable.

TYPE-01

Each unary admitted-value invariant is enforced intrinsically by default; a justified raw representation has verified admission and every write boundary closing the same invariant. Reachability and relational claims are stated separately.

1 §1.1, 2 §2.2

Inspect the elaborated type and invalid constructor/update terms; for raw representations, inspect the rationale, every admission/write theorem, and how consumers obtain the required proof. Do not apply an intrinsic-value claim to arbitrary raw states.

TYPE-02

Every semantic distinction claimed to be enforced by Lean is represented in the interface types or constructors, with its exact scope stated.

2 §2.1, 2 §2.3

Inspect the typed decoding boundary and downstream API. An enumeration restricts the vocabulary but its constructors share one type. Where distinct types, indices, or refinements are claimed to prevent cross-use, check that use is rejected for the intended reason; parsing or validation at admission is permitted.

TYPE-03

Totalized operations and restricted domains are described accurately; a restriction appears in the API only when claimed.

2 §2.3, 3 §3.2.1

Check boundary cases by reduction/theorem and verify the exact hypothesis or subtype required at call sites.

TYPE-04

Abstract models express assumptions as parameters, hypotheses, or proof-bearing fields rather than project logical axioms.

2 §2.4

Inspect binders and ConstantInfo; distinguish assumed propositions from definitions with checked bodies.

TYPE-05

Claimed orders, algebras, and other mathematical interfaces provide their laws and reuse matching Lean/Mathlib structures.

1 §1.4, 4 §4.1–§4.2

Inspect the selected structures, law-bearing instances, or explicit proof assumptions, including laws supplied by stronger instances. Compare the resulting operations and relations with the intended concept and matching Core/Mathlib definitions.

TYPE-06

Every claimed abstraction boundary is the boundary Lean actually enforces.

1 §1.3, 6 §6.5

State the client import context. Verify the intended API use succeeds and that each claimed exclusion fails from a separate importing module. Distinguish name resolution, unfolding, construction, and observation; inspect exported constructors, recursors, projections, coercions, operations, and equations. A failed probe establishes only that attempted exclusion.

THEOREM-01

Every material behavior claim presented as established has kernel-checked evidence in a type, proof-bearing construction, or theorem with the exact intended quantifiers, assumptions, and conclusion.

1 §1.2, 3 §3.1

Enumerate prose claims and match each to an elaborated declaration type; unmatched or weakened claims fail. For executable components, inspect explicit proof requirements and their linkage to actual definitions; gate PASS alone does not establish specification adequacy or completeness.

THEOREM-02

Every claimed typeclass law follows from proof-requiring fields of the operational class or a required Prop-valued lawful mixin, directly or by checked derivation under the advertised hypotheses. Every law-bearing instance discharges its required primitive fields, and required instances are available directly or from stronger assumptions.

3 §3.2.3

Inspect the actual primitive law fields, derived theorems, and selected instances. Every primitive obligation must be discharged; every derived guarantee must follow with exactly its advertised hypotheses. Required mixin evidence must be available at the use site; operations alone do not supply it.

THEOREM-03

Admission and every update establish the claimed invariant by proof-bearing results or the justified raw-boundary contracts; transition/history/resource-use claims have exact proofs, including initialization, preservation, and composition where the claim requires them.

3 §3.1

Inspect admission, all writes, consumers, and exact relational theorem statements. Conditional preservation is not admission, functional behavior, reachability, liveness, or latest-state use.

THEOREM-04

Important claims are non-vacuous at the exact strength claimed; non-vacuity is relative to the claim.

0: non-vacuity, 3 §3.10

Require inhabitance, joint satisfiability, or reachability proofs according to the actual prose; stronger evidence may discharge a weaker requirement when the implication and any additional hypotheses are established. Do not reject a deliberately conditional, contradiction, or minimal-counterexample theorem for lacking an antecedent inhabitant when only the implication is claimed; when the development establishes that the antecedent is false, require the prose to acknowledge vacuity where it affects interpretation; the implication establishes neither an antecedent witness nor its conclusion unconditionally.

THEOREM-05

Logical totality, termination, complexity, and native execution are distinguished; each claimed property has evidence about the exact definitions and semantics it concerns.

3 §3.2.1

Inspect recursive definitions and termination evidence. Match additional claims to the exact types, constructions, or theorems establishing them; logical totality alone does not establish complexity or native execution behavior.

THEOREM-06

Sampled tests and unchecked evaluation do not replace proofs of universal or existential Lean claims. Counterexample search is an optional aid to refutation.

0: role of testing, 3 §3.2.2, 7 §7.8

Reject proof claims supported only by samples, unchecked enumeration, #eval, or native output. Kernel-checked exhaustive finite proofs and checked existential witnesses are proof evidence. Checker qualification under §7.8 is diagnostic evidence about the tool, not proof of the audited mathematics.

THEOREM-07

Material functional contracts state the component’s exact input/output meaning, rejection and normalization behavior, intended updates and frames, state/error composition, and promised fold relation where applicable. Admission completeness is proved when promised.

3 §3.7

Inspect the actual executable definitions and the relations their contracts require. Check intermediate preconditions and the claimed success, error, and effect semantics. Reuse types, construction, library results, or another checked argument; initialization and preservation are required when the chosen argument needs them. Rule out degenerate implementations that violate the promised relation. Separate finite totality and partial correctness from external liveness.

THEOREM-08

Stateful safety transfer has checked correspondence over the exact state and transition semantics. The forward-simulation method in §3.9 supplies initialization, finite abstract matching, preservation, and relation-to-concrete implication; another method must prove the same claimed transfer. Observations and liveness are separate claims.

3 §3.9

Inspect the transfer theorem’s exact hypotheses, conclusion, and executable linkage. For the forward-simulation method, check every related pair/concrete successor quantifier, the existential abstract match, stuttering semantics, and universal finite-path induction. Check initial-state reachability at the claimed strength and observation granularity. Require separate hypotheses/proofs for any progress, fairness, productivity, or liveness claim; safety alone supplies none.

THEOREM-09

A research statement is adequate to its source mathematics, the presented result's status is exactly one of proved unconditionally, proved under explicit binder hypotheses, or open, and an open target is a Prop definition or binder rather than a hole, project axiom, or claimed proof.

3 §3.10, 5 §5.2

Read each material statement back from the elaborated term: quantifier order and dependence, implicit parameters and universes, consequential definitions, notation, coercions, selected instances, totalized operations, and existence/construction/uniqueness/complexity distinctions. Reject strengthened prose or omitted domain assumptions. Keep reduction hypotheses explicit. Exclude intentionally incomplete sketches and adapters from positive surfaces and closed declarations’ dependency closures; a platform-accepted result needs evidence for the actual elaboration environment and foundation.

THEOREM-10

Every cost claim names its domain — elaboration/search, proof artifact, kernel replay, or native execution — and no speed, tactic name, native result, theorem count, sample, or audit digest is presented as evidence of correctness or foundation strength; a well-founded definition's own axiom set is reported exactly.

3 §3.2.5

For each cost statement, identify its domain and inspect the argument or bounded observation supporting that exact claim. Recursive-step counts alone do not establish wall-clock complexity. Inspect elaborated recursion, produced terms, and exact axiom dependencies as relevant; cost or native output does not replace proof evidence.

FOUND-01

No owned declaration is a project logical axiom (Lean 4 has no constant command; opaque is classified under COMP-01); domain assumptions are binders or proof-bearing fields.

3 §3.4, 7 §7.5

Inspect every owned ConstantInfo, including unused, private, internal-looking, and generated declarations. Review that each domain assumption, as a binder or proof-bearing field, presents the intended hypothesis.

FOUND-02

No owned declaration depends transitively on sorryAx; no sorry or admit survives under alternate syntax, attributes, definitions, or instances.

1 §1.1, 7 §7.5

Compute transitive axiom sets for every owned declaration, including proof-valued definitions and instances. Qualification: adversarial hole mutations cover all advertised declaration forms.

FOUND-03

Every owned declaration has its exact transitive axiom set reported. An admissible set receives the least permissive logical label containing it; the selected surface profile is an upper bound. Forbidden and compiler-trusting sets are rejected from conforming positive surfaces.

4 §4.5, 7 §7.5

Compare the computed set with {}, {propext, Quot.sound}, and that set plus Classical.choice; unknown axioms fail. The actual proof's dependencies do not establish minimal axioms among all possible proofs of its proposition.

FOUND-04

No Choice-Free surface depends directly or transitively on Classical.choice; a selected Standard-Logical surface may.

4 §4.5

Inspect the transitive sets for the selected surface profile. Qualification: direct and transitive choice mutations fail the Choice-Free claim; a positive Standard-Logical control passes with its exact label.

FOUND-05

Native/compiler-generated proof axioms are classified separately and rejected from the conforming positive proof surface; final-environment metadata alone cannot spoof the classification.

7 §7.5–§7.6

Inspect generated proof axioms and dependent declarations; the compiler-trusting classification requires a name the nativeEqTrue scheme generates under a declaration of the axiom's module, the tactic's exact asserted statement with a successful independent native replay, and fresh-transcript provenance: the one command introducing that declaration adds the axiom, and no axiom declaration occurs in that command's recorded syntax or macro expansions. Qualification: a real native proof is compiler-trusting; a native-named axiom declared directly, through a macro, or through a macro whose declaration fails after adding the axiom stays a project axiom; a custom frontend forging the final semantic shape of a natively true proof is classified compiler-trusting, never logical.

DECL-01

Every exact module in each claimed Lake library and every claimed standalone executable root is discovered and elaborated from source in fresh root-package build state, warning-free, under the declared exact elaboration environment with the community linters of §6.7 enabled, with completed owned logical declaration and dependency admission under §7.3.

7 §7.1–§7.3, 6 §6.2, 6 §6.7

Read the elaborated Lake library module arrays and executable roots. Import every claimed module and reconcile exact attribution and additional root-owned imports. Record toolchain and dependency source state, the identity the result is bound to; reject emitted warnings and stale root-package artifacts. Dependency artifacts may be reused under §7.3. The modules facet can include local imports beyond the configured array; it is a cross-check, not an interchangeable inventory. Check the Lake options of every claimed library and executable (RG2006): autoImplicit and relaxedAutoImplicit off (§7.1), linter.missingDocs on (§6.7), no linter turned off for a whole target beyond the §6.7 exclusions (§6.2), and, when the surface imports Mathlib, weak.linter.mathlibStandardSet with exactly those exclusions, or with the header linter on and its license line configured (§6.7), with no -D among the extra lean arguments setting any of these options otherwise. Review what the audit cannot see: every source set_option command, in particular that no claimed module sets autoImplicit or relaxedAutoImplicit back on or disables a Lean default warning; and every source-local linter disable, each disabled community linter being declaration-scoped with a stated reason (§6.2).

DECL-02

Every constant in every owned module is inventoried; proof-valued definitions and instances are not omitted.

7 §7.4

Compare environment constant counts and exact names; classify isProp from the elaborated type and validate the trusted-runner report. Qualification includes an audited module registering a colliding observer-command token.

DECL-03

Ownership uses Lean/Lake semantics. Generated-role exceptions require independent evidence: regeneration by Lean's own recursion compiler for recursive helpers (§7.4), and native replay with fresh-frontend command provenance for native-proof axioms (§7.5); names or forgeable final metadata alone cannot authorize them.

7 §7.2, 7 §7.4

Inspect ownership and every claimed exception. Qualification: exact-prefix lookalikes, private and auxiliary-looking names, native-name spoofs, custom-command addDecl, and nested-run_tac generated-role forgeries receive their intended classification or rejection.

DECL-04

Missing/malformed manifests, unknown metadata, omitted declarations, and unexpected project modules fail closed.

7 §7.2–§7.4

Validate the manifest and report schemas and reconcile targets, modules, and declarations. Qualification: mutate each advertised configuration/coverage failure independently and require its intended diagnostic, including observer-command collisions.

COMP-01

noncomputable, opaque, logical Decidable, executable decision procedures, kernel reduction, and native evaluation are distinguished accurately.

3 §3.2.4, 7 §7.6

Inspect metadata and axiom sets; check representative reduction/evaluation behavior on the pinned toolchain.

COMP-02

Partial and unsafe declarations are excluded from positive proof surfaces, except for the range-less partial code-generation helper of a safe recursive def whose base Lean's own recursion compiler regenerates from it, up to compilation erasure (§7.4).

7 §7.4–§7.6

Inspect ConstantInfo.isUnsafe/isPartial and every helper exception. Qualification: safe recursion, explicit termination_by, namespaced, default-tactic, custom-proof, lexicographic and proof-carrying well-founded recursion, attributed, abbrev, where, specialized and mutual recursion, recursion through the module's own notation beside module IO code, derived DecidableEq, BEq, Hashable and Repr functions on a recursive inductive that is neither nested nor mutual, a definition elaborated under a source-local replacement of the specialize attribute pass, well-founded recursion through the toolchain's attach and forIn' rewrites, a module whose macros override the tactics and the term the regeneration would otherwise dispatch, definitions whose nested proofs Lean shares with an earlier declaration or numbers differently from the regeneration, and public definitions of a module file that are not exposed; authored helper-name spoofs, custom-command, run_tac, by_elab, custom tactic- and term-elaborator forgeries of the complete helper metadata, forgeries by a module-local elaborator dispatched unrecorded inside derived code, by an earlier self-removing installer and by a module command elaborator installing a forging deriving handler, a forged helper that calls the audited module's own constant under the name root the regeneration uses in place of its base's callee, a forged helper that computes with another function than its base where the nested proof is shared with an earlier declaration (its faithful copy is admitted), a base whose decreasing proof rests on a project axiom, a project wf_preprocess rule that removes the helper's recursive call from its base, partial definitions (reported under their own names, derived BEq on a nested inductive included), unsafe definitions, and unsafe opaque declarations receive the intended rejection.

COMP-03

Every boundary in the §7.6 conservative execution closure has its exact kind and correspondence state reported; retained compiler edges are distinguished from candidates and historical choices. In "execution": "checked" mode, every boundary in that closure outside the toolchain's origin-checked trusted base is checked. Unresolved paths block the affected execution claim in every mode.

7 §7.6

Reconcile all executable roots and their closures, retained IR, supported histories, boundaries, and exact admitted correspondence proofs over the full dependent domain and universes. Qualification covers legitimate and insufficient equalities, imported/chained/both-order replacements, local and overwritten histories, inlined targets, extern/unsafe/partial paths, and cycles or unsupported histories. A definitional comparison the kernel could not complete is unresolved, never trusted; only a completed negative comparison without another admitted proof leaves a replacement trusted. Observing a diagnostic target in emitted code qualifies discovery, not compiler or external-code correctness. Review that the reconciled executable roots are the intended ones.

COMP-04

Transfer from a Lean reference definition to a replacement requires sufficient checked correspondence. Keep remaining trust assumptions for native and external execution explicit.

7 §7.6

Compare each theorem’s exact statement and dependencies with the claimed computation and admitted relation. A relation between Lean definitions does not itself verify external machine code or discharge reached extern/native boundaries.

BUILD-01

The documented enabled ordinary lake build, and lake lint with the lint driver, reject every emitted warning, policy violation, and unresolved claimed execution path. Source-local warning/linter options cannot authorize policy exceptions.

7 §7.11

Run the enabled ordinary build or lake lint for the claimed adopter configuration. Qualification drives the actual default policy target, including disabled and re-enabled controls, intended diagnostics, and fresh restoration, and drives lake lint in both lakefile formats through every exit class; any other adapter needs corresponding qualification.

BUILD-02

Declared profiles are transitively enforced, with classical erased proofs permitted under Standard-Logical and executable promises checked separately.

3 §3.8, 4 §4.5

Inspect current profile and execution results separately. Qualification: all three positive profiles, direct/imported choice and configuration-change failures, a classical-contract positive, and noncomputable witness rejection.

BUILD-03

Required executable evidence inhabits the exact predicate of the actual named implementation, and registered private/imported roots retain execution coverage.

7 §7.11

Inspect registered predicates, proof-bearing construction, and actual callers. Reconcile additional private/imported roots and review specification adequacy. Qualification mutates missing, unrelated, or weakened evidence and unsupported registrations, and exercises private/extern, replacement, imported csimp, and unsafe boundaries.

BUILD-04

Cached modules and changed configuration cannot reuse a stale policy verdict; exact claimed Lake coverage and supported-context limits are explicit.

7 §7.11

Inspect target/job dependencies and the current manifest and report. Qualification covers unimported glob modules, unclassified targets, imported source and cached profile/execution changes, repeated cached failures, and fresh restoration. Incremental evidence does not establish fresh-source conformance.

DOC-01

Public declarations supporting material normative claims have docstrings stating their formal purpose, relevant assumptions, result, and invariant boundary; every other public definition has a docstring; every claimed module documents its material declarations and assumptions.

5 §5.1–§5.3, 6 §6.7

Compare the documented claims with elaborated types, definitions, and supporting contracts; a function type alone need not specify its input/output relationship. Check actual module docstrings in owned modules; RG5001 checks that each is present and is the first command after the imports (§5.3). RG2006 checks that every claimed target enables linter.missingDocs (DECL-01), so that RG2003 rejects every public definition it reports without a docstring.

DOC-02

English explanations of normative Lean statements faithfully convey their quantifiers, hypotheses, conclusions, relevant definitions, and limitations, and identify the authoritative Lean declaration. Each public declaration supporting a material normative claim carries a nonempty labelled Intent section in its docstring.

5 §5.2

Read the explanation with its referenced definitions; check quantifier order and dependence, domains, hypotheses, conclusion, and limits affecting interpretation. Distinguish results proved without additional hypotheses, results proved under explicit hypotheses, and open targets, retaining stated domains and foundations. Locate the supporting declaration (including through an attached docstring), and compare its elaborated meaning and its explanation with the written intent statement, the requirement-side record of the intended mathematics or program specification. Section presence is mechanical; adequacy of the intent and agreement with it are semantic review.

DOC-03

Every Lean fence in the normative documentation tree (here every lean block of the standard's Verso source, website/RegulaStandard) is structurally classified; malformed markers/fences fail closed.

Set convention, 7 §7.7

Recursively scan the complete normative tree. Qualification mutates every malformed marker/fence state specified in §7.7.

DOC-04

Every positive Lean fence elaborates exactly as printed, warning-free, then passes owned logical admission and declaration/axiom classification.

7 §7.7

Elaborate raw source first; inspect the elaborated temporary module without injecting imports into the claimed source. The shipped fence checker uses Standard-Logical; narrower foundation or execution claims require separate evidence.

DOC-05

Every negative fence fails for its non-empty expected diagnostic, and trusted-compiler teaching fences are classified but never counted as conforming.

7 §7.7

Require a completed diagnostic-worker result and the whole pattern within one effective-error message, preserving multiline text and rejecting cross-message or informational matches. Inspect trusted declarations and their generated axioms.

MUT-01

A checker that classifies foundation profiles has positive controls for all three profiles through its actual detection implementation, with public-path qualification as required by §7.8.

7 §7.8

For new or affected foundation-classification behavior, exercise the relevant positive profiles through the actual detection path; retain applicable evidence for other profiles.

MUT-02

A checker implementation has an independent intended-reason mutation for every violation class it advertises.

7 §7.8

Select intended-reason controls for affected advertised capabilities under §7.8. A complete-campaign claim additionally requires its complete applicable manifest. Reject masked or wrong-reason failures.

MUT-03

A checker qualification harness cannot overwrite positive sources or leave stale Lean artifacts, and its restored control passes fresh.

7 §7.3, 7 §7.8

In a qualification run, use unique disposable paths/build state; verify red mutation and fresh restored green.

MUT-04

Checker qualification establishes a fresh warning-free configured-module baseline and keeps mutation artifacts from satisfying restored controls.

7 §7.3, 7 §7.8

In a qualification run, use empty or isolated root-package output and reject every emitted warning. Share the unchanged baseline where valid; mutations may use isolated incremental rebuilds, with fresh restored controls under §7.8.

MUT-05

When separate serialized-graph checking is claimed, the exact claimed module graph is rechecked in a compatible fresh checker state.

7 §7.9

Require successful results for every selected root. Reconcile the union of claimed modules in their import closures with the exact Lake inventory. Qualification covers root selection and additional-module coverage. Distinguish the driver’s incremental artifact build from its fresh checker state; it does not establish fresh-source elaboration.