[FINDING] Post-remediation residual sweep: A2-demotion doc stragglers, wider 10/10 KAT-count drift, and three micro gate/doc items

[Nicola-Ceornea]

Surface: docs / fv · Severity: low · Evidence: source greps (no PoC needed — enumerated drift) · Target: 666e372 + remediation working tree

Banked during the 2026-08-20 red-team remediation wave (findings #658–#681); each item is real but was outside every fix wave's file ownership:

1. A2-demotion doc stragglers. ~12 historical/living docs still say "A2 axiom" / "11-axiom" where it was true when written (docs/AXIOMS.md, TRUST_ASSUMPTIONS.md, PROOF_MAP.md, ASSURANCE_CASE.md, THREE_CLAIMS_PROOF.md, DISCHARGE_PLAN.md, EUF_CMA_INCONSISTENCY.md, FAITHFULNESS_AUDIT_2026-06-14.md, BLOCKERS.md, OPEN_PROOF_OBLIGATIONS.md, MISSING_FOR_FULL_BYTECODE_PROOF.md, contracts/verification/README.md). The two census-like living docs (AXIOMS.md, TRUST_ASSUMPTIONS.md) are the worthiest updates; the historical findings docs can stay as dated records.
2. Wider "10/10" KAT-count drift across ~11 files: contracts/verification/docs/{A3_1_VERIFIER_GAP,A3_1_CLOSURE_PATH,ASSURANCE_CASE,DISCHARGE_PLAN,EUF_CMA_INCONSISTENCY,MISSING_FOR_FULL_BYTECODE_PROOF,TRUST_ASSUMPTIONS}.md, lean/SphincsCVerify/{Spec/Signature,Bridge/Refinement}.lean, lean/Main.lean:111 (corpus is 12 vectors since 2026-07-06).
3. Bridge/Refinement.lean:28-30 comment says A4 "stays as a True TCB marker" — contradicted by the ledger (A4 content-bearing since 2026-06-14).
4. contracts/verity/Makefile:27 verify-stats still uses the naive multi-file grep -c 'sorry$' pattern (cosmetic stats emitter, not the gate — the gate was fixed with a ratchet in [FINDING] contracts/verity zero-sorry gate fail-open on multiline grep (12 live sorries PASS); census wrong (3 axioms, not 2); uncensused CREATE2 axiom #673).
5. check_c10_transcription.py check (D) (gate_keys_lean) still scans unstripped text — a commented-out gate line would still parse; in practice covered because the histogram loses the .ifnz, but the model gap remains.
6. CI wiring for contracts/verity sorry-ratchet: make -C contracts/verity ci depends on lake build (~20 min) — split the grep-only census into its own target before wiring ([FINDING] contracts/verity zero-sorry gate fail-open on multiline grep (12 live sorries PASS); census wrong (3 axioms, not 2); uncensused CREATE2 axiom #673 follow-up).

Also still open from the red-team wave by design: #679 (lean4checker exact-HEAD replay — manual 40–60 min gate, not yet run), #680 (EIP-712 decode fuzz target — new harness code), #456 (branch protection — off-tree owner action), #670/#671/#681 (EasyCrypt surface — owner actively working it), #97 (tx-merkle waiver holds).