100%

Section 08: Rule-File Sync + Dual-Discharged Proof Re-Validation

Goal: Update the in-tree rule files to reflect implementation reality AND keep the machine-checked proof corpus (compiler_repo/aims-proof/) in lockstep with the burden-revised calculus. Spec (Annex E §AIMS) is intentionally NOT touched here — /sync-aims-spec runs at §10 PASS per conditional-approval governance.

Context: Per proposal §Spec & Grammar Impact + §Approved canon.md §7.1 Invariant 5 Reframing + §Approved missions.md §AIMS Conflict-Resolution Rule Reframing. The proposal includes verbatim text for the rewrites; this section applies them. aims-proofing-suite §18 (Dual-Prover Lean Formalization) has LANDED — every .proof rule-theorem now has a substantive kernel-checked Lean mirror under compiler_repo/aims-proof/lean/AimsProof/ and the dual-discharge gate (scripts/dual-discharge.sh) is a CI hard gate (.github/workflows/aims-proofs.yml). §08.6 consumes that gate; it does NOT re-establish the Lean corpus.

Reference implementations: Existing rule-file structure in .claude/rules/. The proof corpus + Lean mirror + dual-discharge gate at compiler_repo/aims-proof/ (per aims-proofing-suite §18).

Depends on: Section 07 — full coverage migration verified complete (§07 closes VERIFICATION-ONLY per 00-overview.md; rules describe shipped reality). The realization-time predicate stack COEXISTS with the burden path until §09.2’s runtime-green split retires it; §08 rule files document the burden path as the canonical RC-emission surface while noting the §09-transitional coexistence (predicate-stack retirement is §09’s deliverable, not §08’s).

Intelligence Reconnaissance

Queries:

  • scripts/intel-query.sh --human file-symbols ".claude/rules/aims-rules.md" --repo ori
  • scripts/intel-query.sh --human callers BurdenSpec --repo ori — every consumer cited in updated rules
  • scripts/intel-query.sh --human callers eliminate_burden_ops --repo ori — CH-4 shipped-binding consumer set (Handshake.proof anchor)

Queried: 2026-05-08 (rule-symbol consumers); 2026-06-02 (proof-corpus reconciliation — Lean mirror + dual-discharge gate confirmed landed via aims-proofing-suite §18).

Results summary (≤500 chars) [ori]:

  • Existing AIMS infrastructure consumed; section work extends or migrates within the unified model per missions.md §AIMS invariant 5 (no parallel paths, no shadow trackers).
  • Proof corpus: 10 substantive Lean modules under lean/AimsProof/; proof-lean-map.json is the per-.proof↔Lean SSOT; dual-discharge.sh is a CI hard gate.

08.1 arc.md update

  • RECONCILE the existing block, do not author a duplicate: an in-flight guardrail subsection ### Canonical RC-Emission Path — burden architecture (migration in flight) already landed in .claude/rules/arc.md (post-§04B). EDIT THAT SAME SUBSECTION in place into the terminal shipped-surface description — NEVER add a second burden-canonical block. Reconciliation rules:
    • Promote the burden Phase 5/6/7 + BurdenSpec avenue (d) + LEAK:aims-ad-hoc-emission cross-ref to terminal shipped-surface language (these are shipped reality post-§04B Prototype Gate).
    • KEEP an explicit §09-transitional caveat: plans/aims-burden-tracking/section-09 (predicate-stack retirement) is NOT yet started, so the predicate-stack path and the burden path COEXIST today (ORI_DISABLE_BURDEN_OPS=1 runs the pre-§04A baseline). Retain the coexistence note + the BANNED: extending the predicate-stack path (PIN-1..6, class_payload_of, ssa_alias_classes-driven emission) guardrail until §09 retires the predicate stack.
    • Drop ONLY the “in-flight SSOT pointer; do NOT duplicate the reframe ahead of §08” framing — §08 IS the reframe landing, so that forward-pointer is now satisfied. The terminal canon.md §7.1 / missions.md §AIMS reframe (§08.3/§08.4) is the SSOT this subsection now cross-references rather than defers to.
  • Update .claude/rules/arc.md shipped-surface section: cite BurdenRegistry + BurdenSpec + BurdenInc/BurdenDec; describe Phase 5 trivial emission + Phase 6 elimination role + Phase 7 mechanical lowering.
  • Strip references to retired predicate-stack predicates (PIN-1..6).
  • Update the arc.md §Proof Checking / §Debugging “Realization-semantics grounding” map so the burden-op surface points at its governing proven rules: burden-op elimination → proofs/11-coexistence/CH-*.proof + lean/AimsProof/Coexistence.lean; burden RC-balance → proofs/08-realization/RL-comp.proof (RL3_elision_net_preserving) + lean/AimsProof/Realization.lean. NEVER cite the non-existent cross-validation/coexistence-handshake.lean (retired by aims-proofing-suite §18); the real mirror is lean/AimsProof/Coexistence.lean.
  • No prose violations per .claude/rules/skill-vocabulary.md §3.

Companion reviewer-teeth already landed outside this section’s touches: set: impl-hygiene.md §Finding Categories carries LEAK:aims-ad-hoc-emission (Critical). If the §08.3/§08.4 reframe renames Invariant 5 avenues, reconcile that subcategory’s cross-reference; otherwise leave it.

Subsection close-out (08.1) per protocol.

08.2 aims-rules.md update

  • COORDINATION (per decisions/04 Clarification + plans/completed/aims-proofing-suite/section-12-*.md / section-17-*.md): aims-rules.md is ALSO edited by plans/completed/aims-proofing-suite/section-12-*.md (target-only-annotation clearing + proven-rule propagation). Both plans touch aims-rules.md §3/§4 + IC-3; the second mover rebases onto the first’s aims-rules.md state. This section MUST NOT re-introduce or contradict the IC-3 may_escape stored field — plans/locality-representation-unification/ removes it (field → derived method) and plans/completed/aims-proofing-suite/section-12 / section-17 propagate the derived-may_escape form as the IC-3 SSOT. Leave aims-rules.md §1.5 Locality (5-variant post-locality) and aims-rules.md §5 IC-3 may_escape to locality + plans/completed/aims-proofing-suite/section-12; this section owns ONLY the BurdenInc/BurdenDec + Phase-5/6/7 + VF-1.1 edits below.
  • §3 Forward Transfer Matrix: list BurdenInc/BurdenDec in TF-N/A as side-effect-only ops (no dst, no forward AimsState image), mirroring the RcInc/RcDec TF-N-A row that proof-lean-map.json records as doc_encoded (“side-effect-only, no dst; no forward image”). Precision (proof-corpus-grounded): this edit documents burden ops in the matrix; it MUST NOT assert a new BurdenInc.proof/BurdenDec.proof transfer theorem. Burden-op ELIMINATION soundness is the proven §11 coexistence family — CH-1 (AimsProof.Coexistence::CH1_lattice_bridge + CH1_burden_emitted_is_bridge: burden_emitted IS burden_owned, a pure function of the converged lattice state) and CH-2 (CH2_single_elimination: the burden-derived elimination decision EQUALS the lattice-only DP-2/DP-3 decision). The lowered (Phase 7: BurdenInc→RcInc / BurdenDec→RcDec) form’s RC-balance is the proven RL-comp net-preservation (proofs/08-realization/RL-comp.proof → RL3_elision_net_preserving).
  • §4 Decision Predicates: DP-2/DP-3 mention burden-op-site application (cite the proven proofs/05-decisions/DP-2.proof/DP-3.proof + their AimsProof.Decision mirrors; this is the SAME proven predicate the check-section-05-compiler-conformance.sh cross-walk already maps to burden_elim.rs).
  • §7 Pipeline Ordering: Phase 5 trivial / Phase 6 eliminate / Phase 7 mechanical. Anchor the burden pre-pass slot to the proven CH-5 (AimsProof.Coexistence::CH5_analyze_before_realize: the burden pre-pass is sequenced after analyze_function, before realize_rc_reuse, preserving PL-2).
  • §8 Realization Rules: cite mechanical lowering; cross-reference RL-comp net-preservation as the invariant the lowered form preserves.
  • §9 Verification Layers: add VF-1.1 burden-balance check; state explicitly it is an executable CONFORMANCE pass enforcing the proven RC net-preservation (RL3_elision_net_preserving) on emitted burden-op IR, NOT a new calculus theorem (per missions.md §AIMS invariant 5 — extend, never parallel).
  • §VF-7 rewrite-soundness: add a forward-reference note in aims-rules.md §9 VF-7 stating that the burden-path active-rewrite verification posture (the three-tier VF-7 discipline applied to the Phase 5→6→7 burden lowering) is authored by plans/aims-burden-tracking/section-10 verification, which is the authority for the VF-7 posture; this §08 edit only inserts the pointer. Do NOT restate or re-derive the VF-7 tier text here — §10 owns it. If this edit changes the VF-7 rule STATEMENT (obligation / carrier types / operators) rather than adding a pointer, it is a burden-reformulated rule per §08.6 and MUST gate proof-map parity: update proofs/09-verification/VF-7.proof + its lean/AimsProof/Verification.lean mirror (VF7_three_tier_conjunction) + the proof-lean-map.json VF-7 row in lockstep and re-run dual-discharge.sh to exit 0. A pointer-only note (no statement change) does NOT touch the proof corpus.

Subsection close-out (08.2) per protocol.

08.3 canon.md §7.1 Invariant 5 reframing

  • Replace canon.md §7.1 Invariant 5 with the proposal’s verbatim text: “Ownership is itself a typed pre-pass input (registered on the type as BurdenSpec, queried at Phase 5 lowering), not a property the lattice derives. New capabilities shall extend a lattice dimension, extend a contract field, OR extend BurdenSpec — never spawn a parallel emission path.”
  • Cite that the burden-registry-as-typed-pre-pass invariant is the machine-checked CH-4 acyclic read-only property (AimsProof.Coexistence::CH4_state_map_immutable: eliminate_burden_ops L m = L — BR reads the frozen lattice state map, L does not depend on BR).

Subsection close-out (08.3) per protocol.

08.4 missions.md §AIMS conflict-resolution rule reframing

  • Replace missions.md §AIMS Conflict-Resolution Rule with the proposal’s verbatim text: “When a new capability could be added as either a side pipeline or a lattice/contract/burden extension, the typed-data extension wins. The lattice operates as an optimizer over the burden-emitted baseline; ownership decisions live in BurdenSpec, not in flow analysis. New analyses shall NOT spawn parallel RC emission paths, shadow uniqueness trackers, or independent escape enums that bypass the lattice or the burden registry.”

Subsection close-out (08.4) per protocol.

08.5 registry.md update (BurdenRegistry sibling)

  • Add BurdenRegistry to the sibling-registry list in .claude/rules/registry.md: pure-const builtin (ori_registry::burden::BURDEN_TABLE) + user heap-backed (ori_types::TypeRegistry::burden).

  • Confirm pure-const compliance per registry.md §Invariants.

  • TPR checkpoint — /tpr-review covering 08.1-08.5. (3 rounds, converged clean: round 1 4 findings cured, round 2 1 cured, round 3 0 actionable; scratch tpr-review-92eh2w2l.)

Subsection close-out (08.5) per protocol.

08.6 Dual-discharged proof re-validation (burden-reformulated rules)

File(s): compiler_repo/aims-proof/proofs/**/*.proof + compiler_repo/aims-proof/lean/AimsProof/*.lean + compiler_repo/aims-proof/scripts/proof-lean-map.json (all PUBLIC — per CLAUDE.md §Public Repo Hygiene + aims-proofing-suite §18.1 boundary-hygiene: NO wrapper refs / plans/ paths / BUG-XX-NNN placeholders / ori_lang_ai in any .proof/.lean/map edit; cite Annex E §AIMS, never .claude/rules/aims-rules.md).

The burden model reformulates a bounded set of AIMS rules. For EACH reformulated rule, the proof corpus is the third coherent surface (alongside aims-rules.md and Annex E §AIMS per 00-overview.md §Cross-plan coordination — aims-proofing-suite) and MUST be re-validated through the SAME dual-discharge gate aims-proofing-suite §18 ships.

The Lean corpus is COMPLETE and CI-gated — this section consumes the gate, it does not rebuild it.

  • Re-validate exactly the burden-reformulated rule set — the closed enumeration below (every row whose calculus the burden model touches; a rule absent from this list is NOT re-validated here — scope is the reformulated set sourced from the 00-overview.md STRONG-LINK coherence bullet, NOT a blanket re-run):
    • DP-2 / DP-3 burden-op-site application — compiler_repo/aims-proof/proofs/05-decisions/DP-2.proof + DP-3.proof; Lean mirror compiler_repo/aims-proof/lean/AimsProof/Decision.lean. The elimination consumer (eliminate_burden_ops) applies the SAME proven DP-2/DP-3 verdict at burden-op sites. NO statement change — existing DP-2 DP2_is_rc_dec_unnecessary_table + DP-3 DP3_is_rc_inc_elidable_table cover the burden-site application (the verdict is unchanged; burden-op sites are where it is applied, proven via CH-2 single-elimination). NO edit.
    • §7 Phase-5→6→7 ordering composed with the burden pre-pass — compiler_repo/aims-proof/proofs/07-pipeline/PL-1.proof..PL-11.proof + PL-comp.proof; Lean mirror compiler_repo/aims-proof/lean/AimsProof/Pipeline.lean. CH-5 (AimsProof.Coexistence::CH5_analyze_before_realize) anchors the burden pre-pass slot (after analyze_function, before realize_rc_reuse, preserving PL-2). NO statement change — existing PL-* + CH-5 hold. NO edit.
    • §11 coexistence family CH-1..CH-5 + CH-comp — compiler_repo/aims-proof/proofs/11-coexistence/CH-1.proof, CH-2.proof, CH-3.proof, CH-4.proof, CH-5.proof, CH-comp.proof, Handshake.proof; Lean mirror compiler_repo/aims-proof/lean/AimsProof/Coexistence.lean (theorems CH1_lattice_bridge + CH1_burden_emitted_is_bridge, CH2_single_elimination, CH4_state_map_immutable, CH5_analyze_before_realize). NO statement change — existing, proven; confirmed burden_emitted = burden_owned + elimination = CH-1/CH-2. NO edit.
    • VF-1.1 / §AIMS.9.1.1 burden-balance check — consumes RL-comp net-preservation: compiler_repo/aims-proof/proofs/08-realization/RL-comp.proof → RL3_elision_net_preserving (Lean mirror Realization.lean) + compiler_repo/aims-proof/proofs/09-verification/VF-1.proof → AimsProof.Verification::VF1_catches_structural (Lean mirror Verification.lean). The burden-balance pass is an executable CONFORMANCE check enforcing the proven RC net-preservation, NOT a new calculus theorem. NO statement change — existing RL3_elision_net_preserving + VF1_catches_structural hold. NO edit.
    • TF-N/A BurdenInc / BurdenDec side-effect-only encoding — updated compiler_repo/aims-proof/proofs/04-transfers/TF-N-A.proof to list BurdenInc/BurdenDec alongside RcInc/RcDec as side-effect-only ops (no dst, no forward AimsState image); updated compiler_repo/aims-proof/lean/AimsProof/Transfer.lean module-header no-forward-image note to enumerate RcInc/RcDec/BurdenInc/BurdenDec; updated compiler_repo/aims-proof/scripts/proof-lean-map.json TF-N-A row lean_encoding to “RcInc/RcDec + BurdenInc/BurdenDec side-effect-only, no dst; no forward image” (kind doc_encoded, lean_theorem: null, parity_tokens: []). This is a doc_encoded matrix-row edit, NOT a new BurdenInc/BurdenDec transfer theorem — burden-op elimination soundness remains the CH-1/CH-2 coexistence family and the lowered-form RC-balance remains RL3_elision_net_preserving. Wrapper refs stripped from TF-N-A.proof; cites Annex E §AIMS. Mirrors the §08.2 §3 aims-rules.md matrix edit on the proof-corpus side.
  • For each reformulated rule, update the .proof AND its Lean mirror in lean/AimsProof/<Module>.lean in LOCKSTEP. Only the TF-N/A doc_encoded row was edited (.proof + Transfer.lean doc-comment + map lean_encoding); no theorem statement changed, so no proof-lean-map.json parity_tokens/lean_theorem moved and no dual_discharge_divergence was introduced.
  • Run the REAL gate: compiler_repo/aims-proof/scripts/dual-discharge.sh exits 0 — dual_discharge_agree — 119 theorems agree across Ori-checker + Lean (statement-parity prelude PASS over the FULL corpus, THEN Ori-checker verdict via check-proofs.sh AND Lean verdict via lake build AGREE per theorem). Theorem-agreement count UNCHANGED (the TF-N-A doc_encoded row carries no theorem).
  • compiler_repo/aims-proof/scripts/lean-no-placeholder-lint.sh exits 0 — lean_no_placeholder_clean (zero sorry/admit/: True := by trivial/:= by trivial/standalone axiom in any touched .lean).
  • §08.6 enforces ONLY the aims-rules.md ↔ proof-corpus edge (both .proof and Lean) via dual-discharge; it does NOT close the aims-rules.md ↔ Annex E §AIMS edge. That second edge is §10.5’s deliverable, enforced by /sync-aims-spec --check at §10 PASS. The full bi-directional triangle proofs ↔ aims-rules.md ↔ Annex E §AIMS closes across §08.6 (proof edge) + §10.5 (Annex E edge), NOT inside §08 alone.
  • Emit a §10.5 handoff manifest recording the exact burden-revised surface §08 changed, so §10.5 propagates the SAME calculus to Annex E without re-deriving it. Written to plans/aims-burden-tracking/decisions/08-rule-sync-manifest.md (in this section’s touches: frontmatter). Enumerates: (a) every changed aims-rules.md rule row (§3 TF-N/A BurdenInc/BurdenDec, §4 DP-2/DP-3, §7 Phase-5→6→7, §8 RL-comp cross-ref, §9 VF-1.1); (b) the changed proof-lean-map.json row (TF-N-A doc_encoded — the ONLY one, since no theorem statement changed); (c) the expected Annex E §AIMS clauses §10.5 must update (§4 TF-N/A matrix, §4/§3 DP-2/3, §6 pipeline ordering, §8 RL-comp, §9 VF-1.1). Prose-lint clean.
  • Coordinate with plans/completed/aims-proofing-suite/section-18-*.md: any burden-reformulated rule’s proof exists in BOTH the Ori-checker corpus AND the Lean corpus; the §18.3 dual-discharge gate covers it. aims-proofing-suite §18 (Dual-Prover Lean Formalization) is a legitimate CROSS-PLAN reference — plans/completed/aims-proofing-suite/00-overview.md is declared in THIS plan’s 00-overview.md frontmatter references:[], so the §18 dependency belongs in references:, NOT in this section’s local depends_on: (which carries only intra-plan section IDs — ["07"]). Do NOT scope-creep this re-validation into the §18.3 checker-trust job NOR into the §10.7 emitted-IR conformance job — §08.6 keeps the CALCULUS surfaces coherent; §18.3 proves the CHECKER trustworthy; §10.7 proves emitted burden-op IR obeys the calculus.

Subsection close-out (08.6) per protocol.

08.R Third Party Review Findings

  • None.

08.N Completion Checklist

  • Strip the retired cross-validation/coexistence-handshake.lean reference from .claude/rules/aims-rules.md. The ## HISTORY 2026-05-28 §“Coexistence handshake” bullet ends with Lean 4 cross-validation umbrella at compiler_repo/aims-proof/cross-validation/coexistence-handshake.lean (dual-prover Lean formalization, nightly CI gate). — that path does NOT exist (retired by aims-proofing-suite §18; the proof corpus has no cross-validation/ directory). VERIFIED against the shipped corpus (compiler_repo/aims-proof/scripts/proof-lean-map.json): the CH-1..CH-5 + CH-comp rows all map to lean_module: "AimsProof.Coexistence" → the real Lean mirror is compiler_repo/aims-proof/lean/AimsProof/Coexistence.lean, and the dual-prover gate harness is compiler_repo/aims-proof/scripts/dual-discharge.sh. Rewrite the bullet to point at compiler_repo/aims-proof/lean/AimsProof/Coexistence.lean (the kernel-checked CH mirror) gated by compiler_repo/aims-proof/scripts/dual-discharge.sh (the dual-discharge CI gate). Mirrors the §08.1 arc.md grounding-map edit that already corrects the same stale path. This is a .claude/rules/aims-rules.md edit (in touches:); it carries NO proof-corpus statement change (the corpus already lacks the retired file), so no proof-lean-map.json row changes.
  • All 08.X rule files updated.
  • /sync-aims-spec is NOT invoked here. Annex E §AIMS conditional rewrites propagate at §10 PASS.
  • Dual-discharge clean: compiler_repo/aims-proof/scripts/dual-discharge.sh exits 0 + lean-no-placeholder-lint.sh exits 0 for the burden-reformulated rule set; proof-lean-map.json covers every touched theorem (no missing/wrong/weaker parity row).
  • python3 scripts/prose-lint.py .claude/rules/arc.md .claude/rules/aims-rules.md .claude/rules/canon.md .claude/rules/missions.md .claude/rules/registry.md clean.
  • Plan annotation cleanup.
  • Plan sync per protocol; mission criteria 7 + 12 (00-overview.md) checkboxes flipped.
  • /tpr-review passed (final); /impl-hygiene-review passed. /review-plan ran 2 /tpr-review rounds (verify-done) + §08.5 standalone /tpr-review 3-round converged clean; /impl-hygiene-review run 2026-06-03 zero findings (markdown/proof-doc arc; prose-lint clean, claim-fidelity vs Lean clean, no public-leak)

HISTORY

  • 2026-06-02 — Reworked §08.6 to dual-discharge against the REAL, now-complete Lean corpus + TF-N/A precision fix. aims-proofing-suite §18 (Dual-Prover Lean Formalization) landed since this section was authored: all rule-theorems now have substantive kernel-checked Lean mirrors under compiler_repo/aims-proof/lean/AimsProof/ (10 modules) and dual-discharge.sh + lean-no-placeholder-lint.sh + lake build are CI hard gates (.github/workflows/aims-proofs.yml). §08.6 was reframed from “update or re-prove the corresponding .proof” (single-checker, pre-§18 framing) to the dual-discharged contract: update .proof + lean/AimsProof/<Module>.lean + proof-lean-map.json in lockstep, run dual-discharge.sh (statement-parity prelude + Ori↔Lean verdict agreement) to exit 0. Added the §08.2 precision fix: BurdenInc/BurdenDec are TF-N/A side-effect-only ops with NO forward image (per the doc_encoded RcInc/RcDec TF-N-A row in proof-lean-map.json); their elimination soundness is the proven CH-1/CH-2 coexistence theorems (burden_emitted = burden_owned; burden-decision = lattice DP-2/DP-3 decision), and their lowered RC-balance is RL3_elision_net_preserving — NOT a new BurdenInc/BurdenDec transfer theorem. Corrected the stale cross-validation/coexistence-handshake.lean reference (does not exist; retired by §18) to lean/AimsProof/Coexistence.lean in the §08.1 arc.md grounding-map edit. touches: extended with the proof-corpus + Lean + map paths §08.6 edits.
  • 2026-06-01 — In-flight burden-canonical guardrail pre-landed: post-§04B Prototype Gate PASS, a forward-looking guardrail subsection ### Canonical RC-Emission Path landed in .claude/rules/arc.md (in-flight SSOT pointer) + a LEAK:aims-ad-hoc-emission Critical finding category landed in .claude/rules/impl-hygiene.md, to stop external work reintroducing predicate-stack-style ad-hoc emission during the migration window. §08.1 RECONCILES the arc.md subsection into the terminal shipped-surface rewrite (does NOT re-add). The normative canon.md §7.1 / missions.md §AIMS / aims-rules.md reframe stays gated here per the conditional-authority governance.
  • 2026-05-28 — Coordination with aims-proofing-suite §12.1: plans/completed/aims-proofing-suite/section-12-aims-rules-revision.md §12.1 landed proven-revised calculus propagation into .claude/rules/aims-rules.md HISTORY (provenance table + ArgEscaping carve-out + §10 empirical-adequacy + §11 coexistence footnote). Both plans touch aims-rules.md §3/§4 + IC-3; per §12.1 line 180 the second mover rebases onto the first’s aims-rules.md state. Neither may re-introduce the IC-3 may_escape stored field the §17 manifest tracks for removal — once locality lands and §17 flips to conformance: pass, the IC-3 derived-may_escape form is the SSOT both §12 and burden §08 honor.
  • 2026-06-03 — Autopilot auto-cure: phantom_ids=[§07]; per decisions/10-target-self-drift-cure.md 2026-05-11 autopilot carve-out
  • 2026-06-03 — Stale review_pipeline: marker cleared by /continue-roadmap orchestrator: marker carried stage: ?, next_step: ?, updated: ?. Per /review-plan SKILL.md §Step 1a stale-marker rule (reviewed: false + marker present → STALE by definition), marker invalid; prior diagnosis preserved here for traceability. Cure rooted in scripts/plan_orchestrator/markers.py:clear_stale_marker_if_unreviewed.