Critical Violations to Check First🔗

This triage list summarizes the compliance and quality audit. It does not introduce new requirements or reduce the compliance level. Record an established violation as FAIL and missing required evidence as INCOMPLETE. Either result blocks the affected conformance claim. When a violation and missing evidence coexist, report FAIL and identify both. The absence of the issues below does not establish compliance but only shows these specific failures were not found.

1. Forbidden assumptions or an incorrect foundation claim. Project logical axioms, proof holes, unknown or compiler-trusting proof axioms, and dependencies outside the selected foundation profile are not permitted on the positive surface. Inspect every owned declaration’s exact transitive axiom set and reported actual label or separate classification, distinguishing it from the selected surface maximum. Check FOUND-01 through FOUND-05 in Axioms and Foundation Strength.

2. Incomplete coverage or invalid elaboration evidence. Verify complete ownership and classification, the exact environment, and fresh warning-free root-package elaboration and completed owned logical admission (§7.3). An audit that accepts an omitted owned module or declaration, a name-only exemption, stale output as fresh, or an emitted warning violates these requirements. Missing evidence without an established violation leaves the affected claim INCOMPLETE. Check DECL-01 through DECL-04 in Declaration and Module Coverage.

3. Unsupported or misrepresented behavior claims. A claim is unsupported if it exceeds its elaborated declaration, transfers a model result to a separate implementation without sufficient checked correspondence, or presents an open target or conditional result as if proved unconditionally. Required behavior is unsupported if it is missing from the contract or disconnected from the application's actual definitions. Check SCOPE-02, SCOPE-03, THEOREM-01, THEOREM-07, and THEOREM-09 in Scope and Claim Boundaries and Theorems, Proofs, and Non-Vacuity.

4. An invariant, law, domain restriction, or abstraction boundary is weaker than advertised. Inspect the type-enforced distinctions, each admission and write boundary, law-bearing evidence, and the actual client context. Laws may be established by the operational class or by a required lawful mixin, including instances that rely on stronger assumptions. Do not claim stronger functional, reachability, or history properties based on invariant preservation without supporting evidence. Check TYPE-01 through TYPE-06 in Dependent Types and Lawful APIs and THEOREM-02 through THEOREM-04 in Theorems, Proofs, and Non-Vacuity.

5. Lean mechanisms or execution boundaries are misrepresented. Logical decidability, executable computation, noncomputability, opacity, partiality, unsafety, native proof, runtime replacement, and FFI each have distinct consequences. Unresolved execution paths block the affected claim. In checked mode, do not permit trusted boundaries outside the toolchain's trusted base in the claimed closure. Speed, native output, or a tactic name does not establish correctness or foundation strength. Check COMP-01 through COMP-04 in Lean Computation and Evaluation and THEOREM-05, THEOREM-06, and THEOREM-10 in Theorems, Proofs, and Non-Vacuity.

6. Documentation or checker qualification lacks the required evidence. Normative Lean fences require their prescribed elaboration and classification evidence; negative patterns must match one effective-error message from a completed source rejection (§7.7). A checker’s advertised detection behavior requires applicable positive controls and independent intended-reason mutations. Valid qualification for unchanged supported inputs remains usable but does not replace evidence for the current surface. Check DOC-03 through DOC-05 in Documentation as a Lean Teaching Surface and applicable MUT-01 through MUT-04 in Checker Implementation Qualification.

7. An optional build-enforcement or serialized-graph claim is unsupported. An enabled enforcing-build claim requires evidence for its actual invocation, configuration, and coverage. A serialized-graph claim requires successful checking of the exact claimed graph in a compatible fresh checker state. Incremental build evidence does not establish fresh-source elaboration. Check BUILD-01 through BUILD-04 in Opt-in Enforcing Build Integration and MUT-05 in module 8.

After triage, complete every applicable row in module 8. Record the actual scope, failures, and missing evidence as specified by its result rule.