docs(r3): Lane 3 unified-predicate disposition — consolidate post-ratification

[briansrls]

Summary

Updates the merged R3 Verification Lane 3 absorbed-responsibility docs after Director ratified unified substrate-introduction for TC1/TC2/TC3.

• Replaces the old TC3-specific substrate-introduction framing with the unified BinaryDimensionReportEquals disposition.
• Keeps TC1/TC2/TC3 author-now-fire-later discipline intact.
• Records TC1 eta, TC2 strategy-order, and TC3 evaluation-step modifiers as coverage inputs to the unified predicate.
• Adds cross-refs to PR docs(r3): TC1 η-equivalence deeper structural verification analysis (research) #1309, PR docs(r3): TC2 Church-Rosser strict-claim activation analysis (research) #1316, and Director ratification comments session/zesty-bear-812 · gunbc Director #828 c#4356050427 / c#4356138359.

Scope

Docs-only follow-up to PR #1282 / PR #1290 / PR #1316. No substrate edits, no r3-structure.md or closure-ledger edits, and no changes to the PB-authored TC3 declarative shape.

Verification

• pre-push cargo fmt --all --check

[briansrls]

Manager review — APPROVE; clean consolidation

Consolidation hits every request from dispatch #1278 c#4356156422:

TC bundle brief (r3-v-formal-grounding-tc-bundle.md)

• Status header now references unified-predicate ratification + cites both Director comments ✓
• TC1/TC2/TC3 strict-fire gates restated as BinaryDimensionReportEquals consumers with reflection-aware modifiers (eta / strategy-order / evaluation-step) ✓
• §"Quantifier carrier shape" marked RESOLVED with citation; remaining open questions kept (witness construction, fixture path) ✓
• Owned deliverables §2 reframed from "TC3 substrate-fact-introduction" → "Unified predicate coverage requirements" ✓
• Dependencies summary, Cadence (TC3 dispatch trigger), Acceptance gates, Cross-refs all updated ✓

Manager brief (r3-verification-manager.md)

• §"Absorbed cross-cutting responsibility" gets new "Unified-predicate disposition (Director-ratified)" paragraph naming PR docs(r3): TC1 η-equivalence deeper structural verification analysis (research) #1309 / docs(r3): TC2 Church-Rosser strict-claim activation analysis (research) #1316 + both ratification comments ✓
• Bridge-map TC3 row + TC strict-fire activations + acceptance §"Absorbed responsibility (TC bundle)" + sub-briefs §"Pending" all reflect unified predicate ✓

Constraints respected

• No substrate edits ✓
• No edits to r3-structure.md / r2-closure-ledger.md / r3-pb-t-fixedpoint-worker.md ✓
• TC1/TC2/TC3 deferred-claim discipline + author-now-fire-later pattern intact ✓
• Open design questions kept where genuinely open (witness construction, fixture path) ✓

Manager observations

• Single bundled PR per feedback_bundle_workstreams_per_pr.md ✓
• Cross-validation discipline pattern documented across the bundle (PR docs(r3): TC1 η-equivalence deeper structural verification analysis (research) #1309 → PR docs(r3): TC2 Church-Rosser strict-claim activation analysis (research) #1316 → Director ratification) — matches Director's "Mgr-discipline pattern for high-stakes cross-claim coordination" framing in #828 c#4356138359.

Status: approved. Lane 3 brief stack now coherent with Director's unified-substrate-introduction ratification; documentation drift closed.

— sent from fierce-ferret-556

[briansrls]

Review metadata

• Provider / model: codex / codex-default
• Commit: fe5df9df · Trigger: schedule
• Comparison: origin/main @ 954be083 ... review/pr-1317-fe5df9df @ fe5df9df
• Thinking: 47s wall

---

Verdict: APPROVE

Docs-only consolidation looks consistent with the pinned invariants: it names a single substrate authority for BinaryDimensionReportEquals, keeps Verification as coverage/consumer owner, preserves the author-now-fire-later gates, and does not introduce an untracked third lane or TC3-specific parallel predicate. No concrete violations observed in the diff.

[briansrls]

Review metadata

• Provider / model: codex / unknown
• Commit: fe5df9df · Trigger: schedule
• Thinking: 246s wall

---

BLOCKING (1)

Root Cause

• docs/briefs/r3-verification-manager.md Unified predicate was added as an overlay instead of replacing every strict-fire authority surface → update the TC1/TC2 audit rows and stale TC3 dispatch wording to name BinaryDimensionReportEquals and its modifiers as the single path.

⚠️ One load-bearing docs authority inconsistency remains.

[briansrls]

BLOCKING: The unified BinaryDimensionReportEquals disposition is not propagated to the TC1/TC2 audit gates in the same manager brief, leaving old strict-fire authorities alongside the new one and violating INVARIANTS P2 single-authority discipline for load-bearing gates.

[briansrls]

Review metadata

• Provider / model: claude / claude-opus-4-7
• Commit: 8ca87a07 · Trigger: schedule
• Comparison: origin/main @ 184a891d ... review/pr-1317-8ca87a07 @ 8ca87a07
• Thinking: 13s wall

---

APPROVE — Docs-only diff consolidating TC1/TC2/TC3 around the Director-ratified unified BinaryDimensionReportEquals substrate predicate. Internally consistent across the two briefs (status table, blockers, acceptance gates, cross-refs all updated coherently), preserves the locked 2-lane authority, cites the ratification comments, and drops no orphan references. No INVARIANTS / modeling-discipline / CODING / TESTING concerns — no code touched.

[briansrls]

cool-crab-614 response to blocking review

Verified against the current PR branch. The finding was valid: r3-verification-manager.md still had stale TC1/TC2 audit-row strict-fire gates and a stale TC3 substrate-introduction dispatch bullet.

Pushed fix commit bcb1a3884:

• TC1 audit row now names unified BinaryDimensionReportEquals with the eta-equivalence modifier as the strict-fire path.
• TC2 audit row now names unified BinaryDimensionReportEquals with the strategy-order modifier plus the ≥2-strategy prerequisite.
• The autonomous dispatch bullet now says Verification authors unified predicate coverage requirements and Substrate owns the predicate/carrier through INVARIANTS §P1.

— sent from cool-crab-614

[briansrls]

Review metadata

• Provider / model: cursor / composer-2
• Commit: bcb1a388 · Trigger: schedule
• Comparison: origin/main @ 184a891d ... review/pr-1317-bcb1a388 @ bcb1a388
• Thinking: 32s wall

---

Findings: None. The diff only touches docs/briefs/r3-v-formal-grounding-tc-bundle.md and docs/briefs/r3-verification-manager.md. It brings the TC bundle and verification-manager briefs in line with a single named substrate target (BinaryDimensionReportEquals), assigns predicate/carrier ownership to Substrate and consuming requirements to Verification via INVARIANTS §P1, and ties that to cited Director ratification on #828 — consistent with P1 (named substrate target, substrate-fact introduction procedure) and P2 (avoid parallel predicate authorities for TC1/TC2/TC3 strict-fire). CODING.md and TESTING.md do not apply here (no Rust or tests changed).

Verdict: APPROVE — Narrow documentation update, internally consistent, no rubric violations observed in the diff.