Repository navigation
docs(r3): unify TC3 strict-fire gate into single two-stage authority - #1290
Conversation
Manager brief Lane 2 gate listed only R2-Grounding-Rust + R2-Grounding-Python while calling it the "Shape A 3-target grounding precondition." Worker brief already correctly required all three (Rust + Python + Go). Add Go to manager gate to match — single-authority discipline per INVARIANTS §P2. Co-Authored-By: Claude Opus 4.7 (1M context) <noreply@anthropic.com>
Net-position summary listed "3 narrow slices landed (#1014/#1171/#1183/#1192)" which read as a 3-vs-4 count mismatch. #1171 is the outstanding/suspended bridge (#bridge_include_str_side_channels_retired open), not a landed slice. Restate as 2 landed (canonical lens / lower-helper) + 1 outstanding (#1171) + 1 R3-deferred + 1 retired, totaling 5 — and reference closure-ledger PR #1283 which now tracks the include_str row separately. Co-Authored-By: Claude Opus 4.7 (1M context) <noreply@anthropic.com>
Manager brief promoted T-FormalGrounding-Verification to a third lane while the structural authority docs/r3-structure.md L108 names exactly "2 lanes + 1 ledger gate" for Verification scope. That created parallel scope authority violating INVARIANTS §P2. Resolved by deferring to r3-structure.md authority: TC1/TC2/TC3 bundle is now an absorbed cross-cutting responsibility (audit cadence + strict-fire tracking folded into manager cadence), matching r3-pb-t-fixedpoint-worker.md L181 "ownership moves" wording. TC3 substrate-introduction worker brief, when its prerequisites land, joins the existing 2-lane scope as a substrate-introduction sub-task — not a new lane row. If Director ratifies a third lane in r3-structure.md itself, this brief updates accordingly; until then 2-lane scope is the authority. Co-Authored-By: Claude Opus 4.7 (1M context) <noreply@anthropic.com>
Lane 1 brief had a dissolution-trigger note claiming L5 cross-target corpus could absorb per-target L4 receipts. That conflates two categorically different claims per THESIS.md L179-180: L4 compares emit-target output vs .dag evaluation (per-target), L5 compares Rust/Python/Go behavior cross-target. L5 passing does not entail any target matching .dag eval, so L5 cannot subsume L4. Replace with honest stability invariant matching upstream PR-D pattern, plus explicit note that L4 has no current structural dissolution trigger (per codex BLOCKING f5f63c7: NOT a Lens<C> instance, runtime-corpus by design). Co-Authored-By: Claude Opus 4.7 (1M context) <noreply@anthropic.com>
TC bundle brief was reframed as absorbed responsibility (not a lane) but retained "this lane" wording in five places. Replace with "this bundle" throughout to match the locked 2-lane framing per r3-structure.md L108. Editorial fix per cursor reviewer optional finding. Co-Authored-By: Claude Opus 4.7 (1M context) <noreply@anthropic.com>
Lane 1 brief had: - Slice 3 narrowing L7 to "at least one named law" (weakened the closure bar vs r3-structure.md L54 which requires every algebra × every applicable law). - Single made-up gate name verification_l4_l7_direct_per_target_equivalence_landed parallel to the authoritative l4_emit_eval_match + l7_algebraic_laws_witnessed pair (single-authority drift per INVARIANTS §P2). Lane 2 brief similarly used made-up verification_l5_cross_target_consistency_landed parallel to authoritative l5_cross_target_consistency. Manager brief acceptance section restated to cite both authority gates for Lane 1 + L5 authority gate for Lane 2; explicit "partial-coverage early slices do NOT close the lane" framing. Slice 3 in Lane 1 now explicitly marked as coverage-seed only with closure gate referring to full r3-structure.md authority. Co-Authored-By: Claude Opus 4.7 (1M context) <noreply@anthropic.com>
TC3 status table named only substrate-introduction prerequisites under "Strict-fire gate" while §Acceptance separately required T-FixedPoint completion for strict-fire. Two competing gate descriptions for one claim violated single-authority discipline. Restate as a single two-stage gate: (a) substrate-introduction prereqs land tc3_strong_normalization_substrate_introduced (b) T-FixedPoint completion fires the full theorem witness Both stages required; no fire-before-(b) path exists. Stage names match §Acceptance authority below. Co-Authored-By: Claude Opus 4.7 (1M context) <noreply@anthropic.com>
briansrls
changed the title
|
Review metadata
Verdict: APPROVE — The net diff is one documentation row in The new text cross-references No findings that cite a diff line as a violation of the pinned rubric. |
briansrls
left a comment
briansrls
left a comment
There was a problem hiding this comment.
Review metadata
- Provider / model:
codex/unknown - Commit:
02ca1f29· Trigger:schedule - Thinking:
140s wall
Non-blocking — Strengths
docs/briefs/r3-v-formal-grounding-tc-bundle.mdThe TC3 wording cleanly separates substrate introduction from strict-fire while preserving one ordered verification authority.
✅ No blocking concerns in this docs-only gate clarification.
|
Review metadata
Verdict: APPROVE The diff is a one-line documentation clarification in |
|
Review metadata
1. Story of the diffThis PR changes a single load-bearing TC3 planning row in 2. Invariant categories
This is documentation-only, but it does discuss substrate authority;
Single-authority and fail-closed are handled correctly:
The diff is pure documentation; no Rust implementation shape, helper placement, method/free-function choice, error carrier, or naming convention is changed.
No executable test is added, and that is appropriate for this diff:
No locked design decision is modified in the diff. The changed line instead aligns the TC3 plan with existing named authorities: P1 substrate-fact-introduction, B5 audit, T-Substrate-Lens-Primitive, and T-FixedPoint completion at
The staged shape is tracked rather than open-ended: 3. VerdictAPPROVE The PR is a small docs correction, and the changed TC3 row improves the authority model rather than weakening it. I found no diff-line-backed invariant, coding, testing, locked-design, or debt issue to request changes on. |
1 participant
Summary
Follow-up to PR #1282 (R3 Verification Manager spawn briefs, merged as
fbbcf094b). Resolves the TC3 single-authority drift flagged by gpt-5-5-pro reviewer at PR #1282 c#4355424... — review landed after merge, this is the standalone fix.Files
docs/briefs/r3-v-formal-grounding-tc-bundle.md— TC3 row "Strict-fire gate" cell restated as a single two-stage gate:tc3_strong_normalization_substrate_introduced.Both stages required; explicit "no fire-before-(b) path exists" framing closes the parallel-authority gap (status table previously listed only stage-(a) prereqs while §Acceptance separately required T-FixedPoint completion).
Test plan
🤖 Generated with Claude Code