100%

FOLD-IN + SUPERSEDE + GRIND-HERE (plan-wide standing directive — see overview Mission §Bug Fold-In + Supersession, ABSOLUTE). Every failing burden/RC-emission floor cell this section touches is worked HERE as part of this plan’s grind; any BUG-XX-NNN covering it (BUG-04-118 / 142 / 156, the #150 same-allocation-identity class, every sibling RC-emission bug) is FOLDED INTO this plan and SUPERSEDED — NEVER deferred to / routed away as separate bug tracking, a “separate architecture-level pass”, or “already tracked elsewhere”. Dead-end / deferred-compound / reclassified classifications (decisions/LEDGER.md §6) shape WHAT the fix is; they NEVER exit the cell from this plan. If the correct fix is an architecture-level pass, building it IS this plan’s work. Calculus-first per arc.md §CP-1; one terminal gate = ./test-all.sh zero failing cells.

RC-REMARKS CO-EVOLUTION (plan-wide standing directive — see overview Mission §8, ABSOLUTE). This grind is the rc-remarks RC-survivor observability system’s first real test: every floor cell / surviving-RC cluster this section works MUST be grounded via the burden-sole rc-remark stream (ori build --emit-rc-remarks + intel-query.sh rc-survivors --by-cause / rc-cause-rank) before hypothesizing a fix, AND when the stream/analyzer/query falls short for a real cell, improving rc-remarks (producer ori_arc/.../rc_remark.rs, analyzer tools/ori-rc-remarks, intel import_rc_remarks.py + query_graph.py rc-* handlers) IS this section’s work for that cell — never deferred as separate observability work. Burden-sole verdict discipline (arc.md §STOP) unchanged.

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

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.

  • 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.

08.2 aims-rules.md update

Subsection close-out (08.2) per protocol.

  • 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.

08.3 canon.md §7.1 Invariant 5 reframing

Subsection close-out (08.3) per protocol.

  • 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).

08.4 missions.md §AIMS conflict-resolution rule reframing

Subsection close-out (08.4) per protocol.

  • 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.”

08.5 registry.md update (BurdenRegistry sibling)

Subsection close-out (08.5) per protocol.

  • 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 AND /impl-hygiene-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.)

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.

Subsection close-out (08.6) per protocol.

  • 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 logical-event-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 DP-2 is_release_event_unnecessary and DP-3 is_additional_credit_elidable to logical ownership events; Burden* names are transitional Phase-6 carriers. NO statement change — historical theorem identifiers DP2_is_rc_dec_unnecessary_table + DP3_is_rc_inc_elidable_table cover the unchanged verdicts 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 logical owner-credit/release 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 pass checks transitional Burden* carrier IR as executable conformance to the logical invariant, 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.

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.

Fresh intel (regenerated)

§08 is closed-form, low-risk work: rewrite four rule files (arc.md, aims-rules.md, canon.md §7.1, missions.md §AIMS, registry.md) to describe the burden path as shipped canonical reality, then re-validate the bounded burden-reformulated proof set through the ALREADY-COMPLETE aims-proofing-suite §18 dual-discharge gate. The section’s own body confirms every §08.6 rule change is NO edit except one doc_encoded matrix row (TF-N/A) — this is documentation-coherence maintenance, not calculus authorship. The graph and code recon below corroborate every symbol the section cites (BurdenRegistry, eliminate_burden_ops, the five CH-* theorem names) as real, live code and confirms all five theorems exist verbatim in the committed Coexistence.lean.

The decisive finding, however, is NOT about the rule-file content — it is a route-state discrepancy this dossier is positioned to catch:

  1. [JOIN] The canonical plan.json route state (read via the sanctioned read.py API) reports s-d7008993 as status: "not-started", reviewed: false — while the section BODY content (read in full) shows every subsection 08.1 through 08.6 checked off with verified commit-level detail, the 08.N completion checklist fully checked including /tpr-review passed (final); /impl-hygiene-review passed, and 00-overview.md’s plan-wide mission-criteria checklist marking the §08 line [x] complete with an “Outcome:” note describing the shipped rule-file state. This is a genuine content-vs-route desync: the body reads DONE, the route substrate says NOT-STARTED. A consumer picking up this section via /continue-roadmap (which drives off plan.json, never body content per plan-read-discipline.md §2.1) will be told to EXECUTE §08 from scratch — re-running already-completed rule-file edits risks re-opening settled, reviewed prose and re-triggering the §08.2 cross-plan-coordination hazard with aims-proofing-suite §12/§17 (below). The FIRST action on re-entry to this section MUST be reconciling this discrepancy (verify against git log / git blame on the four rule files whether the described edits are actually landed at HEAD, then flip the route state via the sanctioned write API — never hand-execute the subsections again on the assumption the route status is truth).
  2. [JOIN] compiler_repo/aims-proof/scripts/lean-no-placeholder-lint.sh currently reports 10 banned-pattern hits — but ALL 10 are inside lean/scratch/*.lean prose comments (the words “admit-population” / “no sorry/admit” as design vocabulary, not the Lean admit tactic), NOT inside the committed lean/AimsProof/*.lean corpus this section’s “ checklist item claims is clean. The committed corpus (Coexistence.lean, Transfer.lean, Realization.lean, etc.) is verified zero-hit by direct grep. This is a real, currently-reproducible tooling-precision gap: the lint script’s glob (aims-proof/ recursively) does not exclude lean/scratch/, the explicitly-sanctioned exploration zone per arc.md §CP-4 (“Keep scratch Lean OUT of the committed corpus… NEVER edited into AimsProof/*.lean”). The checklist claim (“exits 0”) is either stale (scratch files added after the checkbox was ticked) or was run scoped-only against the committed dir. Either way, running the bare script today gives a FALSE fail on a section whose actual committed-corpus obligation is clean.
  3. The BUG-07-165 public-leak hazard sits directly on this section’s neighboring test surface. compiler/ori_arc/src/lower/burden_lower/tests.rs (the Phase-5 emission tests §08 cross-references via eliminate_burden_ops’s call graph) carries an OPEN, medium-severity bug: ~60 test comments cite wrapper plan-sections (§03.2/§07A.1/§07A.2) and wrapper rule-file paths, leaking private layout into the public upstat-io/ori-lang repo. §08.6 enforces boundary-hygiene strictly on the .proof/.lean files IT touches (CLAUDE.md §Public Repo Hygiene, verbatim in the section header) — the sibling code file one hop away in the call graph does NOT meet that bar today. Not this section’s touches:, but a live hazard a downstream section (§09/§10/§13, which DO touch burden_lower) will walk directly into.

Decisions this package forces before any further work on §08:

  1. Reconcile the route-state-vs-body-content desync FIRST (item 1 above) via the sanctioned plan-corpus write API — never re-execute subsections on the unverified assumption that not-started means “nothing happened”.
  2. Treat the lean-no-placeholder-lint.sh scratch-directory false-positive (item 2) as a tooling-precision gap, not a corpus regression — verify the committed corpus directly (grep -rn '\bsorry\b\|\badmit\b' lean/AimsProof/*.lean, confirmed clean by this dossier) before trusting the bare script exit code.
  3. aims-proofing-suite §11 (Coexistence Handshake Proofs) and §08 (Decision Predicate Proofs — complete) are the SAME proof family §08.6 re-validates; §11 is currently in-progress with aims-proofing-suite reporting 135 blockers across its 8 remaining open sections. §08.2’s explicit “second mover rebases onto the first’s aims-rules.md state” coordination clause is live and load-bearing — re-check aims-rules.md’s current §3/§4/IC-3 state against aims-proofing-suite’s latest landed section before any re-edit.
  4. File /add-bug (or fold into an existing open bug) for the lean-no-placeholder-lint.sh scratch-directory scope leak — it is a tooling-precision defect independent of this section’s content, discovered while grounding this dossier (per CLAUDE.md §ZERO DEFERRAL).

DIG DEEPER

python -m scripts.plan_corpus.read plans/aims-burden-tracking   # confirm current route status
compiler_repo/aims-proof/scripts/lean-no-placeholder-lint.sh    # reproduce the 10 scratch-dir false hits
grep -rn '\bsorry\b\|\badmit\b' compiler_repo/aims-proof/lean/AimsProof/*.lean   # confirm committed corpus clean (0 hits)
scripts/intel-query.sh cypher "MATCH (b:Bug {bug_id:'BUG-07-165'}) RETURN b.status, b.severity, b.subsystem" --human

(full dossier: rule-file-sync-arc-md-aims-rules-md-canon-md-7-1-missions—s-d7008993.intel.md)