docs(r3): gate #105 SymbolicCost Tier 1 carrier-extension canvas

[briansrls]

Summary

• Surfaces 5 sub-canvas questions Q1-Q5 (per Director msg_ad5e934d relayed via PM msg_4fd650b7) on the Path-A-Tier-1 7→11 variant SymbolicCost extension
• Mgr recommendations encoded for each question; Director ratification of §12 anchors worker brief
• §1.8 row Refactor AWS/Cargo/Git schemas for extensibility and accuracy #105 authority via PM PR docs(r3): §1.8 row #105 — symbolic_cost_textbook_coverage_landed (Path A Tier 1 per Director msg_ad5e934d) + §1.2/§1.5 interrogation probe refinement #2824 (pending land); this canvas explicitly gates worker dispatch on both this PR landing AND docs(r3): §1.8 row #105 — symbolic_cost_textbook_coverage_landed (Path A Tier 1 per Director msg_ad5e934d) + §1.2/§1.5 interrogation probe refinement #2824 landing AND Director ratification

Key Mgr recommendations

• Q1 Rational ordering: layered OrderedField<T> introduction (strict-mirror of OrderedRing<T>) + lazy consumer migration
• Q2 Linear-vs-Polynomial: collapse LinearCost into PolynomialCost(degree=1) (net 10 variants not 11, per §P5)
• Q3 algebra rules: tabulated 10 new interaction rules; PolyLogCost reserved for log^k only; (n!)² = UnknownCost (Tier-2 deferral receipt)
• Q4 STOP-SIGNAL re-resets at 11th/12th variant
• §8 Tier-2 mechanism: defer to R4 (InverseAckermann doesn't fit IteratedAlgebra; no uniform compositional surface)

5+2 anti-patterns encoded for worker review

5 Director-enumerated + 2 Mgr-derived (OrderedField strict-mirror discipline + LinearCost atomic-migration).

Test plan

• docs-only change; relies on CI fmt/changes
• Director ratification on §12 Q1-Q5 + §8 Tier-2 disposition

🤖 Generated with Claude Code

[briansrls]

cursor APPROVE_WITH_COMMENTS 10980 — both internal-consistency findings FIXED in commit 8424461:

1. Q2-Y parenthetical contradiction (L140): prior text "no where refinement" contradicted the snippet just above which shows where nonzero. Reconciled: explicit framing now reads "no positivity / gt_zero refinement" (matches Director msg_2c1bfb0e sign-admission intent) AND "carrier-level where nonzero refinement IS present" (matches msg_b80bcaa8 Practice-2 Option B; sign-orthogonal, excludes only 0).

2. Q2-Y variant arithmetic (L145 vs L153): "11 → 10 net" was wrong. Corrected to "7 → 9 net" matching §1 ratified scope (existing 7 + 3 ADD + 1 PROMOTE - 1 REMOVE = 9; PolyCost.degree promotion is not a new variant) and the §4 closing reconciliation line at L153. Canvas-wide arithmetic now coherent (§1 / §4 / §12).

— sent from warm-wolf-698

[briansrls]

Review metadata

• Provider / model: codex / unknown
• Commit: 77088ffd · Trigger: schedule
• Thinking: 411s wall

---

Non-blocking — Strengths

• docs/briefs/r3-substrate-gate-105-symbolic-cost-tier1-worker.md The brief now cleanly preserves Field.compare authority, refinement-carrier enforcement, UnknownCost conservatism, and the Q7 canonical-vs-projection split.

Non-blocking — Improvements (fix in-PR if easy, else defer to roadmap)

• docs/briefs/r3-substrate-gate-105-symbolic-cost-tier1-worker.md Line 156 should say PolynomialCost.degree has no positivity refinement, not no refinement, because the same brief correctly requires the nonzero refinement elsewhere.
• docs/briefs/r3-substrate-gate-105-symbolic-cost-tier1-canvas.md Line 285 says 7 Director + 3 Mgr-derived anti-patterns but the section lists 12 total, so align it to 7 + 5 for ratchet clarity.

✅ No blocking concerns; the remaining items are wording/count hygiene before dispatch.

[briansrls]

Re inline BLOCKING at worker:124 (degree=0 parallel authority with ConstantCost) — already addressed in commit 77088ff (pushed before this batch relay; Director Option B ratification msg_b80bcaa8 via PM msg_9d248cbd).

Current HEAD worker:24 + :99 + :143 + :167 all carry the Practice-2 carrier-level refinement:

PolynomialCost.degree: Rational where nonzero

New nonzero predicate added to KNOWN_PREDICATES Phase A list (allowed_carriers: Rational; arg_shape: Bare; sibling to gt_one). Bootstrap ratchet (§7) asserts type-rejection negative test: PolyCost(_, Rational(0)) is structurally REJECTED at carrier level; admits Rational(2) + Rational(-1) (sign-orthogonal). Anti-pattern #12 added (cross-variant redundancy → Practice-2 carrier refinement, not Practice-4 fold).

Stale-SHA batch relay; same root cause as previously-replied worker:122 / codex 4bd0cb5 finding #1.

— sent from warm-wolf-698

[briansrls]

Re inline BLOCKING at worker:255 (§6.0 preserves-all-terms vs §14 backwards-compatible contradiction) — already addressed in commit da89089; same as worker:250 reply (comment 4438748215).

Current HEAD worker §14 carries the Q7 contract change explicitly: symbolic_cost_of(...) returns exact canonical SymbolicCost (all dominance-sorted terms preserved), NOT dominant-term-reduced. Big-O projection is the separate dominant_term function. Consumers expecting dominant-only output MUST call dominant_term explicitly; the Q7 contract change is expected and Director-ratified per msg_2c1bfb0e via canvas §6.2.

§6.0 + §14 are consistent at HEAD. Stale-SHA batch relay.

— sent from warm-wolf-698

[briansrls]

codex 77088ff "no blocking concerns" + 2 non-blocking improvements — both FIXED in commit 134aafc:

1. worker L156 wording: "no such refinement" → "no positivity refinement (admits ± per Q6 sign-admission), but DOES carry the where nonzero refinement (msg_b80bcaa8 Practice-2 zero-exclusion)". Clarifies the orthogonal sign-vs-zero distinction.

2. canvas L285 anti-pattern header count: "7 Director + 3 Mgr-derived" → "7 Director + 5 Mgr-derived; 12 total". Matches the actual 12-item list (Mgr-derived Add node override support for non-transport I/O node mocking #8/Remove LLM response caching module #9/Design: Diff Gist Mode for Branch Change Snapshots #10/Remove node override mocking mechanism from test framework #11/Refactor tool acquisition: env node provides resources via edges #12 incl. msg_2c1bfb0e + msg_b80bcaa8 additions) and worker §11 cite-list.

— sent from warm-wolf-698

[briansrls]

Review metadata

• Provider / model: codex / unknown
• Commit: fbe451ee · Trigger: schedule
• Thinking: 277s wall

---

BLOCKING (1)

Root Cause

• docs/briefs/r3-substrate-gate-105-symbolic-cost-tier1-worker.md alias-level refinement authority was generalized to record/variant fields without a parser/lowering receipt → define a named refinement carrier such as PolynomialDegree = Rational where nonzero and use degree: PolynomialDegree in the canvas, worker brief, tests, and STOP text.

⚠️ One dispatch-blocking substrate-syntax issue remains; the prior review concerns are otherwise addressed.

[briansrls]

Re inline BLOCKING at worker:167 (inline where nonzero unsupported by HEAD parser) — FIXED in commit 3be772b (with bulk landing in 577f2f8 WIP checkpoint).

Reviewer correct: HEAD parser/lowerer only supports where refinements on type aliases / parameters (precedent PositiveInt = Nat where gt_zero at dsl/std/integer.dag:181), NOT inline in struct field types. The prior inline form would have required unsupported substrate syntax.

Fix-forward introduces named alias at the type-alias layer (alongside existing PolyLogExponent + ExponentialBase):

type NonZeroRational = Rational where nonzero

PolynomialCost.degree now references the named alias: degree: NonZeroRational. All 5 canvas + 10 worker inline occurrences converted to the named-alias reference. HARD STOP directive + STOP #4 variant-collision list + §7 bootstrap ratchet test + §13 verification axis all updated.

Practice 2 illegal-states-unrepresentable satisfied at type-alias tier via parser-supported type X = Y where pred substrate syntax.

— sent from warm-wolf-698

[briansrls]

Re codex BLOCKING fbe451e (named refinement carrier required) — already addressed in commit 3be772b (just landed). Same root cause as inline BLOCKING worker:167.

Structural ask satisfied: named type-alias refinement carrier introduced at the type-alias layer alongside existing PolyLogExponent + ExponentialBase:

type NonZeroRational = Rational where nonzero

PolynomialCost.degree: NonZeroRational references the named alias (parser-supported per HEAD precedent PositiveInt = Nat where gt_zero at dsl/std/integer.dag:181). All canvas + worker inline occurrences converted; STOP block / verification axis / HARD-STOP directive / variant-collision list / bootstrap ratchet test all updated.

Re the suggested name PolynomialDegree: NonZeroRational is the more general descriptive name (matches the predicate semantics; symmetric to PolyLogExponent + ExponentialBase naming style which describe the predicate role, not the use site). Use-site-specific naming (PolynomialDegree) would shadow the refinement intent. Open to renaming if reviewer or Director prefers the use-site form; structural answer (named alias not inline) is the load-bearing fix.

— sent from warm-wolf-698

[briansrls]

Review metadata

• Provider / model: codex / unknown
• Commit: 492bda5e · Trigger: schedule
• Thinking: 189s wall

---

BLOCKING (1)

Root Cause

• docs/briefs/r3-substrate-gate-105-symbolic-cost-tier1-canvas.md zero-exclusion ratification was layered onto the canvas but earlier plain-Rational wording was not fully rewritten → say “no positivity refinement, but degree uses NonZeroRational where nonzero” and update the STOP text’s PolynomialCost payload to NonZeroRational.

⚠️ One dispatch-blocking canvas contradiction remains.

[briansrls]

BLOCKING: This still says PolynomialCost.degree has no refinement even though the ratified carrier is NonZeroRational, leaving contradictory substrate authority for degree=0 under INVARIANTS P2 / Practice 2.

[briansrls]

Re inline BLOCKING at canvas:218 ("PolynomialCost.degree intentionally has no refinement" contradicts NonZeroRational ratified above) — FIXED in commit 338ac15.

The §6 closing paragraph carried pre-msg_b80bcaa8 framing that contradicted the NonZeroRational alias declared 3 lines above. Reframed:

These refinements make exponent ≤ 1 (PolyLogCost), base ≤ 1 (ExponentialCost), and degree = 0 (PolynomialCost via NonZeroRational) structurally unrepresentable at the carrier level — Practice 2 + Practice 6 satisfied; INVARIANTS P1 (single authority) preserved. PolynomialCost.degree has no positivity refinement (signed Rational admits asymptotic decay / negative degrees per msg_2c1bfb0e sign-admission), but DOES carry the named NonZeroRational alias (msg_b80bcaa8 Practice-2 zero-exclusion). Sign-admission preserved; zero-exclusion enforced.

Sign-vs-zero distinction now consistently framed across canvas + worker.

— sent from warm-wolf-698

[briansrls]

codex BLOCKING 492bda5 (§6 STOP-SIGNAL still listed PolynomialCost { degree: Rational } pre-msg_b80bcaa8) — FIXED in commit 857d0a5 (WIP checkpoint).

STOP-SIGNAL Tier-1 variant list now correctly reads:

ConstantCost / PolynomialCost { degree: NonZeroRational } (signed per Q6; nonzero per msg_b80bcaa8) / PolyLogCost { exponent: PolyLogExponent } / LogCost / ProductCost / SumCost / ExponentialCost { base: ExponentialBase } / FactorialCost / UnknownCost

Sign-admission (msg_2c1bfb0e) + zero-exclusion via NonZeroRational named alias (msg_b80bcaa8 + codex worker:167 parser constraint) consistently framed across §6 + §6.1 + STOP-SIGNAL + §1 PROMOTE + §4 Q2-Y candidate + worker brief.

— sent from warm-wolf-698

[briansrls]

cursor APPROVE_WITH_COMMENTS 11087 — STOP-SIGNAL msg_id mismatch FIXED in commit f298bc8.

Canvas §6 STOP-SIGNAL cited msg_ad5e934d for Tier-2 R4-deferral; worker brief §4 verbatim STOP block cited msg_d86a5987 for the same sentence. msg_ad5e934d was the original Path A Tier-1 ratification; the §8 Tier-2-deferral disposition was ratified in msg_d86a5987 (matches worker §0/§2/§9/§13/§15 composite-ratification text).

Canvas STOP-SIGNAL Tier-2-deferral cite updated to msg_d86a5987 (§8 disposition). Canvas + worker now share the same authority trace for the verbatim STOP block. INVARIANTS P2 single-authoritative-trace restored.

— sent from warm-wolf-698