diff --git a/docs/briefs/r3-substrate-gate-105-symbolic-cost-tier1-canvas.md b/docs/briefs/r3-substrate-gate-105-symbolic-cost-tier1-canvas.md new file mode 100644 index 00000000000..9484861f7ba --- /dev/null +++ b/docs/briefs/r3-substrate-gate-105-symbolic-cost-tier1-canvas.md @@ -0,0 +1,345 @@ +--- +status: Mgr canvas (substrate-shape question for Director ratification; surfaced per feedback_substrate_shape_belongs_in_mgr_canvas after PM msg_4fd650b7 formal canvas-trigger relay of Director ratification msg_ad5e934d 2026-05-13) +authority parent: R3 Substrate Manager (warm-wolf-698) +authoring date: 2026-05-13 +gate: §1.8 ledger row #105 `symbolic_cost_textbook_coverage_landed` (added via PM PR #2824) +ratification anchor: PM msg_4fd650b7 relaying Director msg_ad5e934d — Path A Tier 1 RATIFIED + 5 sub-canvas questions Q1-Q5 routed +operator framing: "current list looks very slim ... we need to land this all in R3 please" (2026-05-13) +authority docs: + - `src/v3/std/algebra.dag:190-197` — current 7-variant `SymbolicCost` + - `src/v3/std/algebra.dag:69-72` — `STOP SIGNAL: wanting an eighth variant` (will reset) + - `docs/design-symbolic-cost-algebra.md` — current algebra + - `dsl/std/algebra.dag:268-286` — existing `OrderedRing` witness pattern + - `dsl/std/algebra.dag:294` — `Field` carries `compare: fn(T, T) -> Ordering` (foundational order primitive; derived predicates lt/le/gt/ge live lens-local under Q1-α) + - `dsl/std/rational.dag:26` — `type Rational = Field>` (inherits `Field.compare` via Field-shape) + - `feedback_groundedness_gates_lenses` (Tier 2 structural-extension caveat) +--- + +# Gate #105 — SymbolicCost Tier 1 carrier-extension canvas + +## §0. Status + +Director ratified Path A Tier 1 on 2026-05-13 (PM msg_4fd650b7 relaying msg_ad5e934d). Net 7 → 9 SymbolicCost variants; one promoted (PolynomialCost.degree to Rational). This canvas surfaces 5 sub-questions for Director ratification before worker brief authoring. + +PR #2824 (PM) carries §1.8 row #105 authority anchor; landing pending. Worker brief authoring **gates on this canvas being Director-ratified AND PR #2824 landing**. + +## §1. Ratified Tier 1 variant list (verbatim per Director msg_ad5e934d) + +1. **PROMOTE**: `PolynomialCost { var: SizeVariable, degree: NonZeroRational }` — **signed Rational with carrier-level `where nonzero` refinement** (Director RATIFIED scope-extension msg_2c1bfb0e — sign-admission intent — AS REFINED BY msg_b80bcaa8: Practice-2 carrier-level exclusion of degree=0 to prevent parallel authority with ConstantCost; sign-admission preserved — refinement excludes ONLY 0, admits ±). Subsumes positive degrees: √n = n^(1/2), ∛n = n^(1/3), n^(2/3), non-integer 2.373/2.807, existing integer poly. Subsumes negative degrees: 1/n = n^(-1), 1/√n = n^(-1/2), 1/n² = n^(-2) (asymptotic-decay coverage per operator directive 2026-05-13). Arbitrary roots + inverse roots covered uniformly; degree=0 structurally unrepresentable per Practice 2. +2. **ADD**: `PolyLogCost { var: SizeVariable, exponent: PolyLogExponent }` for log² n, log^k n (PolyLogExponent = Rational > 1 refinement; supports log^7.5 n / AKS Tier-1 case per operator BLOCKING PR #2824:333) +3. **ADD**: `ExponentialCost { base: ExponentialBase, var: SizeVariable }` for 2^n, c^n with c ≥ 2 (ExponentialBase = Int ≥ 2 refinement) +4. **ADD**: `FactorialCost { var: SizeVariable }` for n! + +Net `src/v3/std/algebra.dag:190-197` final variant count: **9** (was 7). + +Tier 2 R4-DEFERRED per Director with named-consumer-trigger requirement: +- LogLogCost (vEB trees) +- InverseAckermannCost (α(n) union-find) +- IteratedLogCost (log* n) +- HyperExponentialCost (n^n super-exp) + +**Structural-extension caveat** (Director-named): if this canvas surfaces a compositional mechanism for Tier 2 satisfying `feedback_groundedness_gates_lenses` + composing with Sum/Product algebra + carries consumer-evidence justification, accept that mechanism IN-R3 instead of named variants. Canvas §6 addresses. + +## §2. State at HEAD (grep-verified 2026-05-13) + +- `src/v3/std/algebra.dag:190-197`: current 7 variants (ConstantCost, LinearCost, PolynomialCost with `degree: DegreeAtLeastTwo`, ProductCost, SumCost, LogCost, UnknownCost) +- `src/v3/std/algebra.dag:69-72`: STOP SIGNAL "wanting an eighth variant" +- `dsl/std/algebra.dag:268-286`: `OrderedRing` witness with `compare/lt/le/gt/ge` already defined +- `dsl/std/algebra.dag:287-295`: `Field` — **CORRECTION per operator BLOCKING 2026-05-13 (canvas:48)**: Field ALREADY has `compare: fn(T, T) -> Ordering` (line 294). The earlier "defined WITHOUT order operations" claim was wrong. Field is missing the derived order predicates (lt/le/gt/ge/eq/ne) that `OrderedRing` carries (lines 268-286), but the foundational `compare` operator IS already on Field. +- `dsl/std/rational.dag:26`: `type Rational = Field>`. Per above correction: Rational already carries `compare` via Field — order primitive is present. What's missing is the convenience-predicate set (lt/le/gt/ge/eq/ne). This invalidates the original Q1 premise; see §3 revised candidate set below. +- `dsl/std/computation.dag:8`: "algebra.dag says 'Int inhabits OrderedRing'" — Int is ordered, but Rational is not + +## §3. Q1 — Rational dominance lattice (Director RATIFIED Q1-α per msg_676ad4e7 2026-05-13; supersedes msg_d86a5987 Q1-c) + +**Premise correction**: Earlier canvas authoring claimed Rational "carries no order witness." This was wrong — `Field` at `dsl/std/algebra.dag:294` already has `compare: fn(T, T) -> Ordering`. Rational therefore already carries the foundational order primitive. What's missing is the **derived order predicates** (lt/le/gt/ge/eq/ne) that `OrderedRing` carries on top of `compare`. + +The original Q1-a/Q1-b/Q1-c framing — and the prior Director-ratified Q1-c disposition — was based on the stale premise. Introducing `OrderedField` now would create **parallel order authority** with the existing `Field.compare` field. Anti-pattern. + +### REVISED Candidate Q1-α — Use `Field.compare` directly + derive helpers as free functions + +Scope: +- Cost-lens fold uses `Rational.compare` directly via existing `Field>.compare` +- Where lt/le/gt/ge convenience predicates are needed in cost-lens body, define them as free functions on `Rational` in cost-lens module (e.g., `rational_lt(a, b) = compare(a, b) == Less`) +- **No `OrderedField` introduction**; no `Rational` re-declaration; no modifications to `dsl/std/algebra.dag` or `dsl/std/rational.dag` + +Pros: +- Zero new substrate; uses existing `Field.compare` +- Cost-lens-local convenience helpers; no foundational algebra touched +- No parallel order authority + +Cons: +- lt/le/gt/ge live as free functions, not on the carrier (mild Cost-of-Change-2 for future predicate sites if free functions need refactor) + +### REVISED Candidate Q1-β — Extend `Field` with derived order predicates (in-place) + +Scope: +- Add `lt: fn(T, T) -> Bool`, `le`, `gt`, `ge`, `eq`, `ne` to `Field` at `dsl/std/algebra.dag:287` — mirroring the OrderedRing record's predicate set +- No new type; `Field` becomes the single authority for ordered-field operations +- Refit Rational stays at `Field>` + +Pros: +- Strict in-place extension of foundational carrier; no parallel-rep +- Single authority — `Field.compare` is foundational; derived predicates compose on it +- Cost-lens fold uses `Rational.lt`, `Rational.le`, etc. directly (Cost-of-Change-1 for future predicate sites) + +Cons: +- Touches foundational `Field` shape; affects all `Field` consumers (witness record gets 6 new fields) +- Migration: existing `Field` witness realizations must populate the new predicate fields + +### REVISED Candidate Q1-γ — `OrderedField` strict-superset (former Q1-c REVISED with explicit reconciliation) + +Scope: +- Add `type OrderedField` extending Field with the missing 6 predicates, EXPLICITLY reconciled: `Field.compare` is the foundational primitive; OrderedField inherits compare from its Field-shaped sub-record and adds derived predicates +- This requires DSL support for sub-record inheritance / type-level inclusion — check at HEAD whether the grammar supports this + +Pros: +- Cleanest Practice-4 layering; OrderedField is structurally Field-plus-predicates +- Field consumers unchanged; OrderedField consumers gain full predicate set + +Cons: +- DSL inheritance grammar may not exist at HEAD (worker brief must grep-verify before authoring) +- Two carriers (Field + OrderedField); the prior parallel-authority concern returns unless inheritance is structural, not parallel + +**Revised Mgr recommendation**: **Q1-α** (use `Field.compare` + cost-lens-local free functions). Reasoning: +- Zero new substrate; zero foundational-algebra-touch +- `feedback_strict_mirror_vs_novel_substrate_fact` does NOT apply here — there's no need for a new witness shape since Field already carries the foundational primitive +- `feedback_no_short_term_solutions` is also irrelevant — this is the canonical use-existing-substrate pattern, not a workaround +- Q1-β is acceptable if Director prefers carrier-uniform predicate set, but the migration scope is broader +- Q1-γ requires DSL-grammar prerequisite check; defer unless Q1-α is rejected + +**Director ratified Q1-α** (msg_676ad4e7 2026-05-13, explicit retraction of msg_d86a5987 Q1-c). Director acknowledged discipline-miss (failure to grep `dsl/std/algebra.dag` for existing Field carrier shape before ratifying); will fold incident as Case 3 in `feedback_grep_substrate_before_naming_ratification`. + +Q1-β REJECTED: doubles Field carrier surface (7→13) for predicates derivable from Ordering pattern-match. + +Q1-γ REJECTED: DSL grammar inheritance/superset typing R4-scope at earliest. + +## §4. Q2 — Linear-vs-Polynomial split reconciliation + +Current shape: `LinearCost(SizeVariable)` is a distinct variant; `PolynomialCost { degree: DegreeAtLeastTwo }` excludes degree=1. After PolynomialCost.degree → Rational, the structural separation question: + +### Candidate Q2-X — Keep Linear separate + +```dag +| LinearCost(SizeVariable) +| PolynomialCost { var: SizeVariable, degree: Rational where degree ≠ 1 } +``` + +Pros: +- Preserves all existing LinearCost-consumer paths (no migration) +- Linear is a meaningful named case; reviewers can grep for it + +Cons: +- `degree ≠ 1` refinement is awkward; structural separation no longer matches algebraic reality (n = n^1 is exactly poly degree=1) +- Algebra rules need a branch for Linear vs PolynomialCost in sum/product (e.g., `LinearCost · LinearCost = PolynomialCost(degree=2)` introduces a cross-variant rule) + +### Candidate Q2-Y — Collapse Linear into Polynomial(degree=1) + +```dag +| PolynomialCost { var: SizeVariable, degree: NonZeroRational } +``` +(LinearCost removed; `LinearCost(v)` ≡ `PolynomialCost { var: v, degree: 1 }`. Per Director scope-extension msg_2c1bfb0e + msg_b80bcaa8: **no positivity / `gt_zero` refinement** — signed Rational admits negative degrees for asymptotic-decay coverage; **carrier-level `where nonzero` refinement IS present** to exclude degree=0 collision with ConstantCost per Practice-2 (Director Option B ratification msg_b80bcaa8).) + +Pros: +- Single uniform variant for all positive-degree polynomial bounds +- Sum/product algebra closes uniformly: `PolyCost(d1) · PolyCost(d2) = PolyCost(d1+d2)` no Linear special case +- 7 → 9 net (per §1 ratified scope: PROMOTE PolyCost.degree + ADD 3 new variants + REMOVE LinearCost = +3 net new variants over the existing 7; LinearCost-absorption aligns with §P5 Progress Is Dissolution). PolynomialCost.degree promotion is not a new variant — see §4 closing line for the variant-count reconciliation. + +Cons: +- **Migration**: all LinearCost-consumer paths must rewrite to PolynomialCost(degree=1) +- Reviewers lose the named "Linear" landmark in cost analysis output (cosmetic) + +**Mgr recommendation**: Q2-Y. The `degree ≠ 1` refinement (Q2-X) is exactly the kind of structural fudge §P5 progress-is-dissolution discipline rejects. LinearCost as a separate variant in a Rational-degree world is a pre-Rational vestige. Migration scope is bounded (cost-lens consumers) and per `feedback_load_bearing_ratchet_preservation` the dissolution-receipt is the standard pattern. + +Net Tier 1 final variant count under Q2-Y: **9**, not 10 (PolynomialCost.degree promotion is not a new variant). Reviewer-ratchet adjusts accordingly. + +## §5. Q3 — Sum/Product algebra interaction rules + +Existing rules (from `docs/design-symbolic-cost-algebra.md` + algebra.dag fold operators): +- `PolyCost(d1) + PolyCost(d2) = PolyCost(max(d1, d2))` (sum takes dominant) +- `PolyCost(d1) · PolyCost(d2) = PolyCost(d1 + d2)` (product adds degrees) +- `LogCost(v) + ConstantCost(c) = LogCost(v)` (log dominates constant) + +**New rules required** (per Director Q3): + +| Operation | Result | Justification | +|---|---|---| +| `PolyCost(d) · LogCost(v)` | `PolyLogCost { var: v, exponent: 1 }`? OR composite ProductCost? | Canvas question (see §5.1) | +| `PolyLogCost(v, k1) · PolyLogCost(v, k2)` | `PolyLogCost(v, k1+k2)` | log^a · log^b = log^(a+b) | +| `PolyCost(d) + ExpCost(c, v)` | `ExpCost(c, v)` | exp dominates poly | +| `PolyCost(d) · ExpCost(c, v)` | `ProductCost([PolyCost(d), ExpCost(c, v)])` | composite, NOT absorbed — n^d · c^n is NOT O(c^n) (operator BLOCKING worker:140); additive absorption above is sound, multiplicative is NOT | +| `ExpCost(c1, v) · ExpCost(c2, v)` | `ExpCost(c1·c2, v)` | c1^v · c2^v = (c1·c2)^v | +| `ExpCost(c1, v) + ExpCost(c2, v)` (c1 < c2) | `ExpCost(c2, v)` | dominant base | +| `FactorialCost(v) + ConstantCost / PolyCost(_,v) / LogCost(v) / PolyLogCost(v,_) / ExpCost(_,v)` | `FactorialCost(v)` | factorial dominates same-variable Tier-1 below | +| `FactorialCost(v) + FactorialCost(w)` (v ≠ w) | `SumCost([FactorialCost(v), FactorialCost(w)])` | cross-variable preserved as composite (no inter-variable dominance) | +| `FactorialCost(v) + UnknownCost(reason)` | `SumCost([FactorialCost(v), UnknownCost(reason)])` | UnknownCost is conservative-top; never absorbed | +| `FactorialCost(v) + SumCost([…]) / ProductCost([…])` | distribute then re-fold per §6 | composite-fold delegates to algebra rules | +| `FactorialCost(v) · PolyCost(d)` | `ProductCost([FactorialCost(v), PolyCost(d)])` | composite, NOT absorbed (n! · n^d not O(n!)) | +| `FactorialCost(v) · ExpCost(c, v)` | `ProductCost([FactorialCost(v), ExpCost(c, v)])` | composite, NOT absorbed (n! · c^n not O(n!)) | +| `FactorialCost(v) · FactorialCost(v)` | `FactorialCost(v)`? OR `UnknownCost("v! · v! exceeds Tier 1")` | Canvas question (see §5.2) | + +### §5.1 — PolyCost · LogCost normalization + +Two candidate shapes: +- (a) `PolyCost(d) · LogCost(v) = PolyLogCost { var: v, exponent: 1 }` if d=0, but d=0 means ConstantCost not PolyCost; if d=1 then it's `v · log(v)` which is canonically n log n +- (b) Keep as composite `ProductCost([PolyCost, LogCost])`; PolyLogCost only constructed from explicit log² n etc. + +Mgr recommendation: (b). PolyLogCost is for log^k n only (single variable, rational-exponent log per Q1-α + PolyLogExponent refinement). The n log n shape is `ProductCost([PolynomialCost { var: n, degree: 1 }, LogCost(n)])` — representable via PolynomialCost(degree=1) post-Q2-Y collapse (LinearCost dissolved); the algebra fold via ordered-dominance correctly identifies it. Avoiding (a) prevents semantic-collision between "poly times log" and "polylog". + +### §5.2 — FactorialCost · FactorialCost + +Two candidate shapes: +- (a) `FactorialCost(v) · FactorialCost(v) = FactorialCost(v)` (factorial absorbs) +- (b) `UnknownCost("(v!)² exceeds Tier 1 — pending R4 named-variant canvas")` per Tier-2-deferral receipt + +Mgr recommendation: (b). `(n!)²` is genuinely outside Tier 1; it's super-factorial / hyperfactorial territory. Per Director anti-pattern #5: "UnknownCost used for textbook-Tier-1-coverable bounds post-promotion (STOP-SIGNAL violation)" — (n!)² is NOT Tier-1-coverable, so UnknownCost("...pending R4...") is the correct disposition. + +### §5.3 — Normalization (rational-degree polynomial) + +- `PolyCost(d1) · PolyCost(d2) = PolyCost(d1 + d2)` — uses `Field.add` on Rational (Q1-α; Rational inherits Field's Ring-shape add) +- `PolyCost(1/2) · PolyCost(1/2) = PolyCost(1)` — and per Q2-Y, this is PolyCost(degree=1), the absorbed Linear +- `PolyCost(d1) + PolyCost(d2) = PolyCost(max(d1, d2))` — uses `Field.compare` on Rational via cost-lens-local `rational_max` helper (Q1-α; NO OrderedField) + +## §6. Q4 — STOP-SIGNAL update + +Current `src/v3/std/algebra.dag:69-72`: +> STOP SIGNAL: wanting an eighth variant. Pause and escalate rather than extending; the thesis claim is that seven covers the asymptotic surface, and any new variant should carry its own dissolution receipt. + +**Post-extension proposed text** (Mgr recommendation): +> STOP SIGNAL: wanting a 10th variant (or 11th if Tier-2 IteratedLog/LogLog/InverseAckermann/HyperExp surface). Pause and escalate. Tier-1 textbook coverage (gate #105 carrier-extension 2026-05-13) lands 9 variants covering ConstantCost / PolynomialCost { degree: NonZeroRational } (signed per Q6; nonzero per msg_b80bcaa8) / PolyLogCost { exponent: PolyLogExponent } / LogCost / ProductCost / SumCost / ExponentialCost { base: ExponentialBase } / FactorialCost / UnknownCost — sufficient for the asymptotic surface that R3-load-bearing lenses reason about. Tier-2 (LogLog / InverseAckermann / IteratedLog / HyperExp) is R4-DEFERRED per Director ratification msg_d86a5987 (§8 disposition); new variants in R4 require consumer-evidence-justified canvas. UnknownCost("reason: ...") remains algebra-top, but reviewer-tier STOP-SIGNAL fires if a Tier-1-coverable bound is collapsed to Unknown — that is anti-pattern #5 per gate #105. + +**Type-level refinement carriers (CORRECTED per PM msg_a52ed981)** — refinement-mechanism `type X = Y where predicate` is ALREADY RATIFIED at HEAD per gunbc#828 issuecomment-4390333451 Path 3 + Director Option 2 (gunbc#828 issuecomment-4390199218). Precedent: `dsl/std/integer.dag:181` (`PositiveInt = Nat where gt_zero`). KNOWN_PREDICATES registry at `src/v3/compiler/src/lower.rs:798-862`: `range / non_empty / brand / gt_zero / unicode_scalar`. NO fresh-records / inductive-sum carriers — refinement over canonical carrier is the canonical path: + +- ~~`PositiveRational = Rational where gt_zero`~~ — **DROPPED per Director msg_2c1bfb0e scope-extension**: PolynomialCost.degree is plain `Rational` (signed; admits negative-degree decay). No gt_zero allowed_carriers extension needed for PolynomialCost. +- `ExponentialBase = Int where range(min: 2)` — IMMEDIATELY available via `range` predicate (allowed_carriers includes Int) +- `PolyLogExponent = Rational where gt_one` — REQUIRES NEW `gt_one` predicate (allowed_carriers: Rational + Int; mirrors `gt_zero` shape; atomic with carrier landing per Phase A) +- `NonZeroRational = Rational where nonzero` — REQUIRES NEW `nonzero` predicate (allowed_carriers: Rational; arg_shape: Bare). **Named alias** per HEAD parser constraint (codex BLOCKING worker:167): `where` refinements only attach to type aliases / parameters at HEAD (precedent `dsl/std/integer.dag:181 type PositiveInt = Nat where gt_zero`), NOT inline in struct field types. Used as `PolynomialCost.degree: NonZeroRational` per Director Option B msg_b80bcaa8. +- `PositiveInt = Nat where gt_zero` — ALREADY EXISTS at `dsl/std/integer.dag:181`; worker reuses + +These refinements make `exponent ≤ 1` (PolyLogCost), `base ≤ 1` (ExponentialCost), and `degree = 0` (PolynomialCost via NonZeroRational) **structurally unrepresentable** at the carrier level via the ratified refinement mechanism — Practice 2 + Practice 6 satisfied; INVARIANTS P1 (single authority) preserved. PolynomialCost.degree has **no positivity refinement** (signed Rational admits asymptotic decay / negative degrees per Director msg_2c1bfb0e sign-admission), but DOES carry the named `NonZeroRational` alias (msg_b80bcaa8 Practice-2 zero-exclusion to prevent ConstantCost collision). Sign-admission preserved; zero-exclusion enforced. + +## §6.1 — Q6 Asymptotic-dominance ordering with signed degrees (Director RATIFIED msg_2c1bfb0e) + +Signed-Rational degrees require explicit dominance rules across the sign boundary. Director-verbatim conjecture (RATIFIED): + +> - For positive degree a, b > 0: `n^a > n^b` iff `a > b` (existing rule). +> - Between positive + negative: any positive-degree term dominates any negative-degree term (`n^a > n^(-b)` for a, b > 0; positive grows → ∞, negative decays → 0). +> - Between negative + constant: `1 > n^(-a)` for any a > 0 (constant dominates decay-to-zero in asymptotic-magnitude lattice). +> - Between two negatives: `n^(-a) > n^(-b)` iff `a < b` (least-negative dominates; 1/n > 1/n²). +> +> **Conjecture**: the dominance rule is "compare degrees with reverse-sign-convention" — asymptotic dominance ≡ algebraic ordering of degrees, but the carrier-to-asymptotic-direction mapping handles sign. + +**Authority**: Q1-α already provides `Field.compare: fn(Rational, Rational) -> Ordering` on the signed-rational carrier. Worker encodes the dominance rule as a derived ordering on `(SizeVariable, Rational)` pairs using `Field.compare` for the magnitude comparison — no new ordering authority introduced. + +**Zero-degree exclusion via carrier-level refinement** (Director RATIFIED Option B per msg_b80bcaa8, supersedes prior canonicalize-fold approach): plain signed `Rational` would admit `degree = 0` which structurally collides with `ConstantCost` (n^0 ≡ 1) — Director rationale (verbatim): "degree=0 is P1 violation, not just Practice-4 normalization … type enforcement > API enforcement; Practice-2 carrier refinement = type-tier, Practice-4 canonicalize-fold = API-tier. Type wins." Resolution: **carrier is `Rational where nonzero`** — exclusion of degree=0 at carrier level via new `nonzero` predicate added to KNOWN_PREDICATES (Phase A; analogous to `gt_one` addition; orthogonal to sign — admits ± rationals). Practice 2 illegal-states-unrepresentable satisfied at type tier; no canonicalize-fold needed for this collision. + +**Practice-2 vs Practice-4 disambiguation rule** (Director-distilled msg_b80bcaa8, NEW load-bearing discipline): +> Same-variant redundancy (e.g., LinearCost vs PolyCost(d=1)) → Practice-4 collapse (Q2-Y precedent). Cross-variant redundancy (e.g., PolyCost(d=0) vs ConstantCost) → Practice-2 carrier refinement. Type-level state-space tightening beats API-level normalization when redundant state crosses variant boundaries. + +## §6.2 — Q7 SymbolicCost preserves full expression; Big-O is a derived operation (Director RATIFIED msg_2c1bfb0e) + +Director-verbatim disposition (RATIFIED): + +> SymbolicCost preserves the full expression ("symbolic" name commits to symbolic-representation, NOT pre-applied asymptotic-simplification). Sum-normalization rule: keep all terms in canonical sorted form (by dominance), DON'T drop sub-dominant terms during canonical-form construction. +> +> Big-O projection is a **derived operation** (separate function `dominant_term(SymbolicCost) -> SymbolicCost` or `asymptotic_class(SymbolicCost) -> ComplexityClass`); SymbolicCost itself is exact. + +**Rationale**: per `feedback_compositional_not_templating` — preserve info structurally; consumer projects as needed. Asymptotic-simplification at canonical-form construction would destroy info. + +**Implication for §5 algebra fold rules**: same-variable sums (e.g., `n + log(n) + 1/n`) canonicalize to `SumCost([PolyCost(n, 1), LogCost(n), PolyCost(n, -1)])` (dominance-sorted), NOT to the dominant term alone. The `+ ExpCost(c, v)` → `ExpCost(c, v)` style dominance rules in §5 are **derived-operation rules**, not canonical-form rules — they apply when computing `dominant_term`, not when constructing SymbolicCost. Worker brief Phase D encodes both: canonical-form preservation + dominant_term derivation. + +Variant count: **9** post-Q2-Y (Director-ratified; PolynomialCost.degree promotion is not a new variant), or **10** if Q2-X is ratified. + +## §7. Q5 — Carrier-shape canvas before worker dispatch — THIS DOC + +This canvas IS the Q5 carrier-shape canvas. On Director ratification of Q1-Q4 + this canvas, worker dispatch proceeds with brief authored per ratified shape. + +## §8. Tier-2 structural-extension caveat (Director-named) + +Director: "if your canvas surfaces a compositional mechanism for Tier 2 that satisfies `feedback_groundedness_gates_lenses` + composes with Sum/Product algebra + carries consumer-evidence justification, accept that mechanism IN-R3 instead of named variants for Tier 2." + +### Candidate compositional mechanism — `IteratedAlgebra` + +Hypothesis: most Tier-2 bounds are **iterates** of Tier-1 functions: +- LogLogCost = `IteratedAlgebra` (log applied twice) +- IteratedLogCost = `IteratedAlgebra` with iteration-count = log*(n) +- InverseAckermannCost = inverse of `Ackermann` iterate — doesn't fit cleanly +- HyperExpCost = `IteratedAlgebra` + +Sum/Product composition under iterate: complex — LogLog · LogLog = LogLog², which is itself a polylog of a logarithm. Composition discipline rapidly degrades. + +**Mgr finding**: a uniform compositional mechanism for ALL Tier-2 cases is **not surfaced by this canvas**. InverseAckermann in particular doesn't fit the iterate pattern. Recommendation: **defer Tier 2 to R4 per Director default**; do NOT accept IteratedAlgebra in this canvas as a structural-extension shortcut. The consumer-evidence triggers (vEB trees, union-find, log*-bounded data structures) can drive named-variant canvases in R4. + +## §9. Practice 4 (coproduct dissolution) classification + +For each Tier-1 addition under §1: + +| Addition | Practice 4 classification | +|---|---| +| PROMOTE PolynomialCost.degree to Rational | 🟢 GREEN — refines structural payload; no new sum-type arm; dissolution-trigger if Rational lands order | +| ADD PolyLogCost | 🟢 GREEN — new variant for distinct asymptotic class (log^k n); consumer evidence: polylog-time algorithms (Strassen, FFT preliminaries) | +| ADD ExponentialCost | 🟢 GREEN — distinct asymptotic class; consumer evidence: brute-force search, exponential-time hypotheses | +| ADD FactorialCost | 🟢 GREEN — distinct asymptotic class; consumer evidence: permutation enumeration, brute-force matching | +| REMOVE LinearCost (under Q2-Y) | 🟢 P5 dissolution — absorbed into PolynomialCost(degree=1); structural fact unchanged | + +No 🔴 RED introductions. Anti-pattern #2 (Director-enumerated): "Path B revival (RootCost as separate variant — Practice-4 RED)" — explicitly NOT done; roots are PolynomialCost(degree=1/2 etc.). + +## §10. Anti-patterns (7 Director-enumerated + 5 Mgr-derived; 12 total) + +### Director-enumerated + +1. Any Tier 2 variant named without consumer-evidence (premature variants) — §8 disposition: not introducing +2. Any Path B revival (RootCost as separate variant — Practice-4 RED) — §9: explicitly not done +3. Linear-Polynomial split decision authored without canvas (substrate-shape question goes through Mgr) — this canvas IS the §4 Q2 disposition +4. Dominance lattice fudging via string-tagged Rational (use real ordered-witness) — §3 Q1-α addresses via existing Field.compare +5. UnknownCost used for textbook-Tier-1-coverable bounds post-promotion (STOP-SIGNAL violation) — §6 STOP-SIGNAL text encodes +6. **Director-ratified msg_676ad4e7**: Introducing parallel ordered-algebraic-structure carriers (`Ordered`) when the underlying carrier already provides `compare: fn(T, T) -> Ordering`. Lens-local predicate derivation from Ordering pattern-match is the canonical path. — §3 Q1-α addresses +7. **NEW (Director ratified per operator BLOCKING PR #2824:333)**: Tier-1 variant constructed with raw Int/Rational exponent/base that admits illegal collapse values (exponent=0/1 for PolyLogCost; base=0/1 for ExponentialCost) bypassing the refinement type. PolyLogExponent + ExponentialBase are required at the type level (Practice 2/6; illegal-states-unrepresentable). **PolynomialCost.degree is excluded** from this anti-pattern — Director msg_2c1bfb0e scope-extension intentionally admits signed Rational degrees for asymptotic-decay coverage (Q6). + +### Mgr-derived (encoded for worker review) + +8. Multiplicative absorption rules where one variant absorbs another (`X · Y = X`) when X is asymptotically larger than Y additively — asymptotic absorption is sound for SUM but NOT PRODUCT (n^d · c^n is NOT O(c^n)); cross-class products must be `ProductCost` composite. §5 algebra rules table addresses (operator BLOCKING worker:140). +9. **PM-grep-corrected per msg_a52ed981 + codex 014544f4 finding #1**: Parallel rational-number carriers (fresh records like `{ num: PositiveInt; denom: PositiveInt }`, inductive sums, or any carrier shape OTHER than refinement) when the canonical refinement-mechanism (`type X = Y where predicate`) is RATIFIED at HEAD per gunbc#828 issuecomment-4390333451 Path 3 + Director Option 2. Refinement over canonical `Rational = Field>` is the canonical path; precedent `PositiveInt = Nat where gt_zero` at `dsl/std/integer.dag:181`. Anti-pattern fires on ANY fresh-carrier shape when refinement is available. +10. `LinearCost`-consumer paths preserved alongside `PolynomialCost(degree=1)` (Q2-Y atomic-migration; bridge variants violate §P5) +11. **Director-added msg_2c1bfb0e**: Introducing parallel `InverseCost(SymbolicCost)` / `ReciprocalCost` / `DecayCost` variants when carrier-extension via signed `degree: Rational` is structurally clean. Same Q1-α / Q1-c lesson class — don't bridge-wrap when carrier-extension dissolves the question (`feedback_dissolve_bridges` + `feedback_no_metadata_markers`). +12. **Director-added msg_b80bcaa8**: Introducing canonicalize-fold rules for **cross-variant redundancy** when carrier-level refinement (`where `) is structurally available. Practice-2 type-tier exclusion beats Practice-4 API-tier normalization when redundant state crosses variant boundaries (PolyCost(d=0) ≡ ConstantCost(1) → use `where nonzero`, not canonicalize-fold). Same-variant collapse (Q2-Y LinearCost ≡ PolyCost(d=1)) is the appropriate Practice-4 lane; cross-variant redundancy must be carrier-refined. + +## §11. Cost-of-change accounting + +Per `INVARIANTS.md` "Cost of Change": + +| State | Files to edit to add one new asymptotic-bound consumer | +|---|---| +| Pre-canvas (today) | ≥3 (variant if Tier-2-coverable; algebra rules; consumer site) | +| Post-canvas (9-variant Q2-Y) | 1 (consumer constructs the appropriate Tier-1 variant directly) | + +For exotic (Tier-2) bounds: still requires UnknownCost("reason") at consumer site — that's the R4-deferral receipt. + +## §12. Ratified dispositions (audit trail; all Q1-Q7 Director-ratified) + +- **Q1**: **RATIFIED Q1-α** (msg_676ad4e7, supersedes msg_d86a5987 Q1-c) — use existing `Field.compare`; NO `OrderedField` introduction; cost-lens-local rational_lt/le/gt/ge/eq/ne free functions +- **Q2**: **RATIFIED Q2-Y** (collapse LinearCost into PolynomialCost(degree=1)) +- **Q3**: **RATIFIED** §5 10-rule algebra interaction table; §5.1 b composite; §5.2 b UnknownCost (for (n!)²) +- **Q4**: **RATIFIED** §6 STOP-SIGNAL text re-reset at 10th variant (9 ratified + 1 trigger) +- **Q5**: **RATIFIED** this canvas (carrier-shape canvas before worker dispatch) +- **§8 Tier-2 mechanism**: **RATIFIED defer to R4**; IteratedAlgebra rejected per §8 analysis +- **Q6** (Director msg_2c1bfb0e): **RATIFIED** signed-Rational `PolynomialCost.degree` (drop `where gt_zero` refinement); asymptotic-dominance rule "compare degrees with reverse-sign-convention" using existing `Field.compare` authority. Practice 4 🟢 GREEN — no new sum-types; carrier extension. +- **Q7** (Director msg_2c1bfb0e): **RATIFIED** SymbolicCost preserves full expression; canonical-form is dominance-sorted SumCost preserving all terms; Big-O is derived operation via `dominant_term` / `asymptotic_class` projection functions. + +## §13. Reference + +- §1.8 row #105 (PM PR #2824 pending) — authority anchor +- `src/v3/std/algebra.dag:190-197` — current 7-variant SymbolicCost +- `src/v3/std/algebra.dag:69-72` — current STOP SIGNAL +- `dsl/std/algebra.dag:268-286` — OrderedRing precedent +- `dsl/std/algebra.dag:294` — Field carries `compare: fn(T, T) -> Ordering` +- `dsl/std/rational.dag:26` — Rational = Field> +- `docs/design-symbolic-cost-algebra.md` — current algebra +- Director ratification: PM msg_4fd650b7 / Director msg_ad5e934d +- `feedback_groundedness_gates_lenses` — Tier-2 structural-extension caveat +- `feedback_strict_mirror_vs_novel_substrate_fact` — Q1-α applies (strict-mirror via existing Field.compare) +- `feedback_load_bearing_ratchet_preservation` — Q2-Y migration discipline + +--- + +**Authored by**: warm-wolf-698 (R3 Substrate Mgr) +**Date**: 2026-05-13 diff --git a/docs/briefs/r3-substrate-gate-105-symbolic-cost-tier1-worker.md b/docs/briefs/r3-substrate-gate-105-symbolic-cost-tier1-worker.md new file mode 100644 index 00000000000..9253d87ac66 --- /dev/null +++ b/docs/briefs/r3-substrate-gate-105-symbolic-cost-tier1-worker.md @@ -0,0 +1,401 @@ +--- +status: dispatchable-on-cascade (worker brief; ratified shape per canvas PR #2828 Director-ratified 2026-05-13 via composite ratification — PM msg_a055c38b relaying Director msg_d86a5987 (Q2-Q5 + §8 base ratification) AS RECONCILED BY Director msg_676ad4e7 (Q1-α supersession of prior Q1-c); dispatch gates on PR #2824 row #105 anchor + PR #2828 canvas landing — both AND) +authority parent: R3 Substrate Manager (warm-wolf-698) +authoring date: 2026-05-13 +gate: §1.8 ledger row #105 `symbolic_cost_textbook_coverage_landed` +parent canvas: PR #2828 / `docs/briefs/r3-substrate-gate-105-symbolic-cost-tier1-canvas.md` — Q1-Q5 + §8 Tier-2 RATIFIED +ratification anchor: composite — PM msg_a055c38b relaying Director msg_d86a5987 (Q2-Q5 + §8) AS RECONCILED BY Director msg_676ad4e7 (Q1-α supersedes prior Q1-c) +row anchor: PM PR #2824 +--- + +# Gate #105 — SymbolicCost Tier 1 carrier-extension worker brief + +## §0. Status — DISPATCH-READY (cascade-gated) + +Director ratified all Q1-Q5 + §8 Tier-2 dispositions per **composite ratification**: PM msg_a055c38b relaying Director msg_d86a5987 (Q2-Q5 + §8 base) AS RECONCILED BY Director msg_676ad4e7 (Q1-α supersedes prior Q1-c). Worker dispatch gates on: +1. **PR #2824 merge** — §1.8 row #105 authority anchor lands +2. **PR #2828 merge** — canvas authored shape lands (both PRs may merge in parallel) + +This brief encodes the ratified Tier-1 4-addition + 1-collapse + 1-promotion structure as a single coordinated PR. **No sub-phase merges independently** (mirrors F-β.2 atomic-PR receipt; gate-row STOP discipline). + +## §1. Ratified scope summary + +Net 7 → **9** SymbolicCost variants: +- **PROMOTE**: `PolynomialCost.degree: DegreeAtLeastTwo` → `PolynomialCost.degree: NonZeroRational` (signed with carrier-level zero-exclusion per Director msg_2c1bfb0e sign-admission intent + msg_b80bcaa8 Practice-2 carrier-level refinement; sign preserved — refinement excludes ONLY degree=0 to prevent parallel-authority with ConstantCost) — subsumes positive (√n, ∛n, n^(2/3), n^2.373, absorbed Linear at degree=1) AND negative (1/n = n^(-1), 1/n² = n^(-2)); degree=0 type-rejected +- **REMOVE**: `LinearCost(SizeVariable)` — atomic migration to `PolynomialCost { var: v, degree: 1 }` (Q2-Y) +- **ADD**: `PolyLogCost { var: SizeVariable, exponent: PolyLogExponent }` for log^k n (PolyLogExponent = Rational > 1 refinement; supports log^7.5 n cited Tier-1 AKS case) +- **ADD**: `ExponentialCost { base: ExponentialBase, var: SizeVariable }` for c^n with c ≥ 2 (ExponentialBase = Int ≥ 2 refinement) +- **ADD**: `FactorialCost { var: SizeVariable }` for n! + +Sibling substrate (Q1 — Rational ordering; **Director RATIFIED Q1-α per msg_676ad4e7 2026-05-13**, retracting prior Q1-c msg_d86a5987): + +**Original Q1-c (OrderedField introduction) REJECTED**: `Field` at `dsl/std/algebra.dag:294` already carries `compare: fn(T, T) -> Ordering` (precedent: `OrderedRing.compare` at `:276`). Introducing `OrderedField` would have duplicated Field.compare authority, violating INVARIANTS P1 + row #24 + Q-MachineConstraint-Carrier "no dual representations". + +**Director-ratified Q1-α**: +- **NO `OrderedField` introduction** +- **NO `Rational` re-declaration** at `dsl/std/rational.dag:26` +- Cost-lens fold uses `Rational.compare` via existing `Field.compare` +- Cost-lens-local free functions: `rational_lt(a, b) = compare(a, b) == Less` (and `_le`, `_gt`, `_ge`, `_eq`, `_ne` as needed by §6 algebra rules) + +## §2. Authority chain (verbatim) + +- `src/v3/std/algebra.dag:69-72` — current STOP SIGNAL (will be rewritten per §4) +- `src/v3/std/algebra.dag:190-197` — current 7-variant `SymbolicCost` +- `dsl/std/algebra.dag:268-286` — `OrderedRing` precedent (`compare/lt/le/gt/ge` witness pattern) +- `dsl/std/algebra.dag:287-295` — current `Field` (carries `compare: fn(T, T) -> Ordering` at :294; missing derived predicates lt/le/gt/ge/eq/ne — see §3 Q1-α premise correction) +- `dsl/std/rational.dag:26` — `type Rational = Field>` +- `docs/design-symbolic-cost-algebra.md` — current algebra +- Canvas: PR #2828 / `docs/briefs/r3-substrate-gate-105-symbolic-cost-tier1-canvas.md` §§3-9 +- Ratification (composite): PM msg_a055c38b relaying Director msg_d86a5987 (Q2-Q5 + §8) RECONCILED BY Director msg_676ad4e7 (Q1-α supersedes prior Q1-c) + +## §3. Phase A — Rational ordering helpers (Q1-α; Director RATIFIED msg_676ad4e7) + +**Premise correction landed**: `Field` at `dsl/std/algebra.dag:294` carries `compare: fn(T, T) -> Ordering`. Original Phase A introducing `OrderedField` was based on stale premise (operator BLOCKING canvas:48); Director retracted msg_d86a5987 Q1-c via msg_676ad4e7. + +**Under Q1-α (ratified)**: + +- **NO `OrderedField` introduction** — Field carries `compare` already +- **NO `Rational` re-declaration** at `dsl/std/rational.dag:26` — stays as `Field>` +- **Cost-lens-local convenience helpers**: define lt/le/gt/ge as free functions on Rational in cost-lens module, derived from existing `Rational.compare`: + +```dag +// In src/v3/lenses/cost.dag (or equivalent cost-lens module). +// Convenience predicates derived from Rational.compare. Single source of +// truth remains Field.compare at dsl/std/algebra.dag:294. + +fn rational_lt(a: Rational, b: Rational) -> Bool = + rational.compare(a, b) == Less + +fn rational_le(a: Rational, b: Rational) -> Bool = + rational.compare(a, b) == Less || rational.compare(a, b) == Equal + +fn rational_gt(a: Rational, b: Rational) -> Bool = + rational.compare(a, b) == Greater + +fn rational_max(a: Rational, b: Rational) -> Rational = + match rational.compare(a, b) { + Greater => a + _ => b + } +``` + +**Witness realization**: Rational's Field-witness realization (`compare` for `FieldOfFractions`) uses Int cross-multiplication: `a/b ≶ c/d ⟺ ad ≶ bc` when b·d > 0. If this realization is NOT yet wired at HEAD, Phase A may need to land the data witness; worker grep-verifies before authoring. + +Q1-β (extend Field with predicate fields) REJECTED by Director — doubles Field carrier surface (7→13) for predicates derivable from Ordering pattern-match; violates cost-of-change minimization. + +Q1-γ (OrderedField as Field-superset via inheritance) REJECTED by Director — DSL grammar inheritance/superset typing R4-scope at earliest; forward-incompatible with R3 timeline. + +## §4. Phase B — STOP SIGNAL rewrite (Q4) + +Replace `src/v3/std/algebra.dag:69-72` block — and ONLY that 4-line block — with (Director-ratified verbatim per canvas §6): + +**DO NOT** touch lines `:49-67`: those carry the 4-pattern dissolution receipt (Pattern 1/2/3/4 commentary) and are out-of-scope for this PR. Phase B is a surgical replacement of the STOP-SIGNAL paragraph only; the dissolution-receipt prose updates (if any) belong to a separate canvas + PR (codex BLOCKING 10904 explicit warning). + +``` +// STOP SIGNAL: wanting a 10th variant (or 11th if Tier-2 +// IteratedLog/LogLog/InverseAckermann/HyperExp surface). Pause and +// escalate. Tier-1 textbook coverage (gate #105 carrier-extension +// 2026-05-13, PR #) lands 9 variants covering ConstantCost / +// PolynomialCost { degree: NonZeroRational } (signed per Q6 + Practice-2 zero-exclusion per msg_b80bcaa8) / PolyLogCost { exponent: +// PolyLogExponent (Rational > 1) } / LogCost / ProductCost / SumCost / +// ExponentialCost { base: ExponentialBase (Int ≥ 2) } / FactorialCost / +// UnknownCost — sufficient +// for the asymptotic surface that R3-load-bearing lenses reason about. +// Tier-2 (LogLog / InverseAckermann / IteratedLog / HyperExp) is +// R4-DEFERRED per Director ratification msg_d86a5987; new variants in +// R4 require consumer-evidence-justified canvas. UnknownCost("reason: ...") +// remains algebra-top, but reviewer-tier STOP-SIGNAL fires if a +// Tier-1-coverable bound is collapsed to Unknown — that is anti-pattern +// #5 per gate #105. +``` + +Cite gate #105 + PR #2828 + composite ratification (msg_d86a5987 base RECONCILED BY msg_676ad4e7 Q1-α supersession) in the comment block. + +## §5. Phase C — SymbolicCost carrier reshape (Q2-Y + variant additions) + +### §5.0 — Type-level refinement carriers (per codex BLOCKING on PR #2828) + +**Refinement-mechanism path (CORRECT per PM msg_a52ed981)**: the substrate refinement-mechanism `type X = Y where predicate` is **already ratified** at HEAD per gunbc#828 issuecomment-4390333451 (Path 3) + Director Option 2 ratification at gunbc#828 issuecomment-4390199218. Precedent: `dsl/std/integer.dag:181` — `type PositiveInt = Nat where gt_zero`. The `KNOWN_PREDICATES` registry at `src/v3/compiler/src/lower.rs:798-862` carries: `range` / `non_empty` / `brand` / `gt_zero` / `unicode_scalar`. + +This **invalidates** the prior product-shape carriers (codex BLOCKING 014544f4 finding #1 + operator BLOCKING worker:104). Canonical shape uses refinement over existing carriers: + +```dag +// ExponentialBase: Int ≥ 2. range(min: 2) — `range` predicate at +// lower.rs:817 with allowed_carriers Int + Nat. +type ExponentialBase = Int where range(min: 2) + +// PositiveRational: Rational > 0. REQUIRES KNOWN_PREDICATES extension: +// add `Rational` to gt_zero's allowed_carriers (currently Nat + Int). +// Worker authors atomic with carrier landing per Phase A. +// (PositiveRational DROPPED per Director msg_2c1bfb0e scope-extension — +// PolynomialCost.degree is plain signed Rational; admits negative-degree decay. +// No gt_zero allowed_carriers extension needed for PolynomialCost.) + +// PolyLogExponent: Rational > 1. REQUIRES KNOWN_PREDICATES extension: +// add NEW `gt_one` predicate (allowed_carriers: Rational + Int) to +// the registry. Mirrors `gt_zero` shape. Worker authors atomic with +// carrier landing per Phase A. +type PolyLogExponent = Rational where gt_one + +// NonZeroRational: Rational ≠ 0 (admits positive AND negative; excludes only zero). +// REQUIRES KNOWN_PREDICATES extension: add NEW `nonzero` predicate +// (allowed_carriers: Rational; arg_shape: Bare) to the registry. +// Per codex BLOCKING worker:167: `where` refinements at HEAD attach only to +// type aliases / parameters (precedent `PositiveInt = Nat where gt_zero` at +// dsl/std/integer.dag:181), NOT inline in struct field types. NonZeroRational +// MUST be named at the type-alias layer; field types reference the alias. +type NonZeroRational = Rational where nonzero +``` + +**Phase A KNOWN_PREDICATES extensions** (Mgr-tier scope; required for refinement-mechanism authority): +1. Add new `gt_one` predicate (allowed_carriers: `Rational + Int`; arg_shape: `Bare`) — required for `PolyLogExponent = Rational where gt_one` +2. Add new `nonzero` predicate (allowed_carriers: `Rational`; arg_shape: `Bare`) — required for `PolynomialCost.degree: NonZeroRational` (Director RATIFIED Option B per msg_b80bcaa8: Practice-2 carrier-level exclusion of degree=0 to prevent parallel authority with ConstantCost; sign-admission preserved — orthogonal to ±) +3. Extensions land in same PR as carrier-shape changes — atomic per §P5 + +(`gt_zero` allowed_carriers extension is **NOT** required: PolynomialCost.degree uses `where nonzero` (orthogonal to sign), not `where gt_zero`. `ExponentialBase = Int where range(min: 2)` uses the existing `range` predicate. Only `gt_one` + `nonzero` are genuinely new predicates.) + +**ZERO new authority introduced**: PolyLogExponent + PolynomialCost.degree are refinements of canonical Rational; ExponentialBase is a refinement of canonical Int. Director-distilled discipline (msg_b80bcaa8): cross-variant redundancy → Practice-2 carrier refinement (PolyCost(d=0) vs ConstantCost); same-variant redundancy → Practice-4 collapse (Q2-Y LinearCost ≡ PolyCost(d=1)). Type-level state-space tightening beats API-level normalization when redundant state crosses variant boundaries. Practice 4 / P1 / P2 / Q-MachineConstraint-Carrier hard constraint "no dual representations" all satisfied. + +**Authority chain for refinement mechanism**: +- gunbc#828 issuecomment-4390333451 (Path 3 RATIFIED) +- gunbc#828 issuecomment-4390199218 (Director Option 2) +- `dsl/std/integer.dag:171-181` precedent (`PositiveInt = Nat where gt_zero`) +- `src/v3/compiler/src/lower.rs:798-862` KNOWN_PREDICATES registry + +These refinements make `exponent ≤ 1` (PolyLogCost), `base ≤ 1` (ExponentialCost), and `degree = 0` (PolynomialCost via NonZeroRational) structurally impossible to construct — no fold-time enforcement required, no new authority. PolynomialCost.degree has **no positivity refinement** (admits ± per Q6 sign-admission msg_2c1bfb0e) but DOES carry the named `NonZeroRational` alias (msg_b80bcaa8 Practice-2 zero-exclusion to prevent ConstantCost collision; named-alias form per HEAD parser constraint). + +**HARD STOP**: do NOT author NonZeroRational / PolyLogExponent / ExponentialBase as fresh records / inductive sums when refinement over canonical carrier is available. That pattern is codex BLOCKING 014544f4 finding #1 + operator BLOCKING worker:104 anti-pattern (now §10 #8 below). All three MUST land as named type aliases following `type X = Y where pred` (codex BLOCKING worker:167 — inline `where` in field types is unsupported by HEAD parser; precedent `PositiveInt = Nat where gt_zero` at `dsl/std/integer.dag:181`). + +### §5.1 — Replace SymbolicCost variant set + +Replace `src/v3/std/algebra.dag:190-197` with: + +```dag +type SymbolicCost inhabits Semiring + = ConstantCost(Int) + | PolynomialCost { var: SizeVariable, degree: NonZeroRational } // Q2-Y: absorbs LinearCost via degree=1; Q6 signed Rational (admits decay) + | PolyLogCost { var: SizeVariable, exponent: PolyLogExponent } // NEW: log^k n; exponent > 1 by carrier (admits 2, 3/2, 7.5; rejects 0/1 collapses) + | ProductCost(NonSingletonList) + | SumCost(NonSingletonList) + | LogCost(SizeVariable) + | ExponentialCost { base: ExponentialBase, var: SizeVariable } // NEW: c^n with c ≥ 2 by carrier + | FactorialCost { var: SizeVariable } // NEW: n! + | UnknownCost(String) +``` + +9 variants. **LinearCost is REMOVED** (anti-pattern #7: no bridge variants; atomic migration). + +**Invariants encoded at carrier level** (Practice 2/6 — NOT fold normalizer): +- `PolynomialCost.degree: NonZeroRational` — **signed with carrier-level zero-exclusion** (Q6 sign-admission + msg_b80bcaa8 Practice-2 refinement); negative degrees admitted for asymptotic-decay coverage; degree=0 type-rejected (prevents parallel authority with ConstantCost). Asymptotic-dominance rule (Q6) is encoded in the algebra fold layer via `Field.compare` with reverse-sign-convention. +- `PolyLogCost.exponent: PolyLogExponent` — `exponent ≤ 1` is structurally impossible (excludes 0=ConstantCost-collapse + 1=LogCost-collapse semantic dups); supports rational exponents like log^7.5 n (AKS primality cited Tier-1 case) +- `ExponentialCost.base: ExponentialBase` — `base ≤ 1` is structurally impossible (excludes 0=degenerate + 1=ConstantCost-collapse) + +Reviewers MUST flag any attempt to use raw `Rational` / `Int` for these fields. + +## §6. Phase D — Algebra interaction rules (Q3 + Q6 + Q7) + +### §6.0 — Q7 canonical-form preservation (Director RATIFIED msg_2c1bfb0e) + +**SymbolicCost preserves the full expression.** The same-variable algebra fold rules below apply to **derived-operation** projection (`dominant_term: SymbolicCost -> SymbolicCost`), NOT to canonical-form construction. Sum-canonicalization sorts terms by Q6 dominance ordering and preserves every term: + +``` +canonicalize(SumCost([n + log(n) + 1/n])) + = SumCost([PolyCost(n, 1), LogCost(n), PolyCost(n, -1)]) // dominance-sorted, all terms preserved +``` + +Big-O projection is a separate function applied by consumers: + +``` +fn dominant_term(c: SymbolicCost) -> SymbolicCost { + // Apply §6.1 dominance rules ONLY here, NOT during SumCost construction. +} +fn asymptotic_class(c: SymbolicCost) -> ComplexityClass { ... } +``` + +Worker MUST implement BOTH `canonicalize` (preserves all terms) and `dominant_term` (applies §6.1 dominance fold). Tests assert canonical-form preservation under mixed-sign (e.g., `n + 1/n` canonicalizes to 2-term SumCost, not 1-term PolyCost(n, 1)). + +### §6.1 — Q6 Asymptotic-dominance ordering with signed degrees (Director RATIFIED msg_2c1bfb0e) + +Dominance rule (used by `dominant_term`, NOT by canonicalize): + +- Positive degrees a, b > 0: `n^a > n^b` iff `a > b` +- Positive vs negative: `n^a > n^(-b)` for a, b > 0 (positive grows; negative decays) +- Constant vs negative: `1 > n^(-a)` for any a > 0 (constant dominates decay) +- Two negatives: `n^(-a) > n^(-b)` iff `a < b` (least-negative dominates; 1/n > 1/n²) + +**Implementation**: encode as a derived ordering over `(SizeVariable, Rational)` pairs using `Field.compare` for the underlying Rational comparison — Q1-α authority. NO separate ordered carrier introduced. + +### §6.2 — Same-variable algebra fold rules (applied by `dominant_term`) + +Update sum + product fold logic to implement the Director-ratified rule table (canvas §5). + +**Variable-scoping precondition** (per codex BLOCKING 014544f4 finding #3): the rules below assume **same-variable operands**. Different-variable operations (e.g., `PolyCost(n, d1) + PolyCost(m, d2)` where n ≠ m) are NOT folded by dominance — they preserve as `SumCost` / `ProductCost` composite. Algebra dominance is variable-local; cross-variable dominance is undefined within Tier-1 substrate (requires Tier-2 or polynomial-multivariate ratification post-R3). + +Same-variable rules (operands share `SizeVariable`): + +| Operation | Result | +|---|---| +| `PolyCost(d1) + PolyCost(d2)` (`dominant_term` projection) | `PolyCost(max(d1, d2))` (uses `Rational.compare` (Q1-α free function `rational_max`)). Note: `degree=0` is type-rejected at carrier level (`where nonzero`); the d1+d2=0 case in multiplication below requires explicit STOP/surface — see next row. | +| `PolyCost(d1) · PolyCost(d2)` where `d1 + d2 ≠ 0` | `PolyCost(d1 + d2)` — uses `Rational.add` (Field) | +| `PolyCost(d1) · PolyCost(d2)` where `d1 + d2 = 0` | `ConstantCost(1)` — multiplicative cancellation produces n^0 ≡ 1; fold rewrites to ConstantCost arm. **Not a parallel-authority concern** because PolyCost-with-degree=0 is type-rejected (carrier `Rational where nonzero`); the fold maps the cancellation result into the canonical ConstantCost arm directly. | +| `PolyCost(d) · LogCost(v)` | `ProductCost([PolyCost(d), LogCost(v)])` (§5.1: composite, NOT PolyLogCost) | +| `PolyLogCost(v, k1) · PolyLogCost(v, k2)` | `PolyLogCost(v, k1+k2)` | +| `PolyLogCost(v, k1) + PolyLogCost(v, k2)` | `PolyLogCost(v, max(k1, k2))` | +| `PolyCost(d) + ExpCost(c, v)` | `ExpCost(c, v)` (exp dominates poly) | +| `PolyCost(d) · ExpCost(c, v)` | `ProductCost([PolyCost(d), ExpCost(c, v)])` — composite, NOT absorbed (n^d · c^n is NOT O(c^n) strictly; `n^d · c^n / c^n = n^d` is unbounded; multiplicative absorption is unsound per operator BLOCKING worker:140) | +| `ExpCost(c1, v) + ExpCost(c2, v)`, c1 ≤ c2 | `ExpCost(c2, v)` (dominant base) | +| `ExpCost(c1, v) · ExpCost(c2, v)` | `ExpCost(c1·c2, v)` (multiplicative composition) | +| `FactorialCost(v) + FactorialCost(v)` | `FactorialCost(v)` (same-variable absorption) | +| `FactorialCost(v) + ExpCost(c, v)` | `FactorialCost(v)` (factorial dominates exp, same-variable) | +| `FactorialCost(v) + PolyCost(d, v)` | `FactorialCost(v)` (factorial dominates poly, same-variable) | +| `FactorialCost(v) + PolyLogCost(v, k)` | `FactorialCost(v)` (factorial dominates polylog, same-variable) | +| `FactorialCost(v) + LogCost(v)` | `FactorialCost(v)` (factorial dominates log, same-variable) | +| `FactorialCost(v) + ConstantCost(c)` | `FactorialCost(v)` (factorial dominates constant) | +| `FactorialCost(v) + UnknownCost(r)` | `SumCost([FactorialCost(v), UnknownCost(r)])` — composite; UnknownCost is conservative-top per `src/v3/std/algebra.dag` documentation; NEVER absorbed (operator BLOCKING worker:158) | +| `FactorialCost(v) + FactorialCost(w)` (v ≠ w) | `SumCost([FactorialCost(v), FactorialCost(w)])` — composite; cross-variable dominance undefined per §6 precondition | +| `FactorialCost(v) · PolyCost(d)` | `ProductCost([FactorialCost(v), PolyCost(d)])` — composite, NOT absorbed (same unsoundness; n! · n^d / n! = n^d unbounded) | +| `FactorialCost(v) · ExpCost(c, v)` | `ProductCost([FactorialCost(v), ExpCost(c, v)])` — composite, NOT absorbed (n! · c^n / n! = c^n unbounded) | +| `FactorialCost(v) · FactorialCost(v)` | `UnknownCost("(v!)² exceeds Tier 1 — pending R4 named-variant canvas")` (§5.2 verbatim) | + +Normalization invariants in fold (canvas §5.3): +- `PolyCost(1/2) · PolyCost(1/2)` normalizes to `PolyCost(1)` via `Rational.add` (Field) +- Sum/product dominance applies `Rational.compare` (Field) for all max-style reductions +- The collapsed Linear (`PolyCost(d=1)`) participates uniformly in sum/product + +## §7. Phase E — Bootstrap ratchet test + +Mirror `src/v3/compiler/tests/integration/cementing/` shape (cf. `complexity_lens_behavioral_completion.rs`): + +`src/v3/compiler/tests/integration/cementing/symbolic_cost_tier1_carrier_test.rs` asserting: +- 9 variant count (assert against `cost.dag` or `algebra.dag` source); REMOVED LinearCost (PolynomialCost.degree promotion to Rational is not a new variant) +- All 9 variant names + field shapes structurally present +- **NEW (Director msg_b80bcaa8 + codex worker:167)**: type-rejection negative test asserts `PolynomialCost { var, degree: Rational(0) }` is structurally REJECTED at carrier level via `NonZeroRational` named-alias refinement. Test also asserts `type NonZeroRational = Rational where nonzero` is declared at the type-alias layer (NOT inline). Admits positive (`Rational(2)` → ok via NonZeroRational construction) + negative (`Rational(-1)` → ok); rejects only zero. +- Phase A Q1-α deliverables present: rational_lt/le/gt/ge/eq/ne free functions in cost-lens module; NO OrderedField type declared +- Phase A KNOWN_PREDICATES extension: both `gt_one` AND `nonzero` predicates added to lower.rs registry; bootstrap test asserts both predicates present with correct allowed_carriers. +- `Rational = Field>` UNCHANGED at `dsl/std/rational.dag:26` (Q1-α) +- Algebra rule sample tests (≥6 of §6 rules): assert fold output for representative inputs (e.g., `PolyCost(1/2) · PolyCost(1/2)` produces `PolyCost(1)`; `ExpCost(2,n) · PolyCost(d)` produces `ProductCost([ExpCost(2,n), PolyCost(d)])` — multiplicative cross-class is NOT absorbed per §6 + anti-pattern #9 (asymptotic absorption is sound for SUM but unsound for PRODUCT); `ExpCost(2,n) + PolyCost(d)` produces `ExpCost(2,n)` — additive cross-class absorption is sound; `FactorialCost(n)²` produces `UnknownCost` with the exact §5.2 reason-string) +- STOP-SIGNAL text at `:69-72` contains new "10th variant" wording + +## §8. Phase F — Consumer migration (atomic) + +Migrate cost-lens consumers from `LinearCost(v)` → `PolynomialCost { var: v, degree: 1 }` in the **same PR**. No bridge variant; no `LinearCost`-fallback path (anti-pattern #7). + +Inventory required (worker greps at HEAD before authoring): +- `git grep -nE "\\bLinearCost\\b" src/v3/ dsl/` — all consumer sites +- For each site, replace with `PolynomialCost { var: , degree: rational_from_int(1) }` (or canvas-ratified helper name) +- The fold algebra under §6 ensures correctness: `PolyCost(1) + PolyCost(1) = PolyCost(1)`; `PolyCost(1) · PolyCost(1) = PolyCost(2)` etc. + +## §9. Phase G — §1.8 row #105 ledger update + +After Phase A-F land + tests green, update `docs/r3-program-plan.md` §1.8 row #105 from DECLARED (or CANVAS_RATIFIED if PM ledger-maintenance landed first) → **CONSUMER_LANDED** with cite to this PR + canvas PR #2828 + composite ratification (Director msg_d86a5987 base + msg_676ad4e7 Q1-α supersession). + +## §10. STOP conditions + +1. **`OrderedRing` shape drift** at HEAD — if `dsl/std/algebra.dag:268-286` no longer carries the exact 14-field signature this brief mirrors, **STOP** and surface — strict-mirror authority broken. +2. **Existing `LinearCost`-consumer surface differs from canvas assumption** — if grep reveals consumer paths that can't migrate to `PolynomialCost(degree=1)` losslessly (e.g., type-level dispatches on LinearCost variant-tag), **STOP** — anti-pattern #7 atomic-migration discipline requires lossless migration. +3. **`Rational` carrier not at `dsl/std/rational.dag:26`** — if Rational has moved / changed shape since 2026-05-13 grep, **STOP** — Q1-α refinement target is wrong. +4. **Variant-name collision** at HEAD — if any of `PolyLogCost` / `ExponentialCost` / `FactorialCost` / `ExponentialBase` / `PolyLogExponent` / `NonZeroRational` appear from parallel landing, **STOP** for de-duplication. (`PositiveInt` already exists at `dsl/std/integer.dag:181` — reuse. `PositiveRational` is OUT of scope per Q6 — if encountered at HEAD as a parallel landing, that's an anti-pattern #7 fire.) +5. **Algebra rule §5.2 violation tempted** — if Phase D authoring tempts a named (n!)² variant or non-Unknown disposition, **STOP** — anti-pattern #5 fires; the rule disposition is Director-ratified. +6. **PR #2824 not merged at dispatch** OR **PR #2828 not merged at dispatch** — both gates AND; if either is unmerged, **STOP** and surface to Mgr; worker dispatch is blocked. + +## §11. 12 anti-patterns (7 Director-enumerated + 5 Mgr-derived per canvas §10) + +PR body MUST cite each verbatim + assert receipt-of-compliance: + +1. Any Tier 2 variant named without consumer-evidence (premature variants) +2. Any Path B revival (RootCost as separate variant — Practice-4 RED) +3. Linear-Polynomial split decision authored without canvas (substrate-shape question goes through Mgr) +4. Dominance lattice fudging via string-tagged Rational (use real ordered-witness) — §3 Q1-α addresses via existing Field.compare +5. UnknownCost used for textbook-Tier-1-coverable bounds post-promotion (STOP-SIGNAL violation) +6. **Director-ratified msg_676ad4e7**: Introducing parallel ordered-algebraic-structure carriers (`Ordered`) when the underlying carrier already provides `compare: fn(T, T) -> Ordering` — lens-local predicate derivation from Ordering pattern-match is the canonical path +7. **Director ratified per operator BLOCKING PR #2824:333**: Tier-1 variant constructed with raw Int/Rational exponent/base admitting illegal collapse values (exponent=0/1 for PolyLogCost; base=0/1 for ExponentialCost) bypassing refinement type — PolyLogExponent + ExponentialBase required at carrier level (Practice 2/6). **PolynomialCost.degree is excluded** per Director msg_2c1bfb0e scope-extension — signed Rational degrees intentionally admit negative values for asymptotic-decay coverage (Q6). +8. **PM-grep-corrected per msg_a52ed981 + codex 014544f4 finding #1**: Parallel rational-number carriers (`PositiveRational { num: PositiveInt; denom: PositiveInt }`, inductive `PolyLogExponentSuccessor | PolyLogExponentFractional`, or any fresh record/sum shape) when refinement over canonical `Rational = Field>` carrier is available via ratified `type X = Y where predicate` mechanism (gunbc#828 issuecomment-4390333451 Path 3 RATIFIED; precedent `PositiveInt = Nat where gt_zero` at `dsl/std/integer.dag:181`). Anti-pattern fires on ANY fresh-carrier shape when refinement is available. +9. Multiplicative absorption rules (`X · Y = X`) where one variant absorbs another asymptotically — sound for SUM, NOT PRODUCT (n^d · c^n is NOT O(c^n)); cross-class products MUST be ProductCost composite (per operator BLOCKING worker:140) +10. `LinearCost`-consumer paths preserved alongside `PolynomialCost(degree=1)` (Q2-Y atomic-migration; bridge variants violate §P5) +11. **Director-added msg_2c1bfb0e**: Introducing parallel `InverseCost(SymbolicCost)` / `ReciprocalCost` / `DecayCost` variants when carrier-extension via signed `degree: Rational` is structurally clean. Same Q1-α / Q1-c lesson class — don't bridge-wrap when carrier-extension dissolves the question (`feedback_dissolve_bridges` + `feedback_no_metadata_markers`). +12. **Director-added msg_b80bcaa8**: Introducing canonicalize-fold rules for **cross-variant redundancy** when carrier-level refinement (`where `) is structurally available. Practice-2 type-tier exclusion beats Practice-4 API-tier normalization when the redundant state crosses variant boundaries (e.g., PolyCost(d=0) ≡ ConstantCost(1)). Same-variant collapse (Q2-Y LinearCost ≡ PolyCost(d=1)) is the appropriate Practice-4 lane; cross-variant redundancy must be carrier-refined. + +## §12. 5 reviewer ratchets (Director-enumerated for PR review) + +1. **Q1-α integrity**: NO new OrderedField type; Rational ordering uses existing Field.compare via cost-lens-local free functions +2. **Q2-Y integrity**: NO LinearCost preservation paths alongside PolyCost(degree=1); atomic migration receipt required +3. **Q3 algebra rules**: §5.1 + §5.2 dispositions are load-bearing; reviewers flag deviation +4. **Q4 STOP-SIGNAL text**: must land at `src/v3/std/algebra.dag:69-72` with new variant cap at 10 (9 ratified + 1 trigger) +5. **All 12 anti-patterns enforceable** at PR review + +## §13. Verification + +- `cargo test --workspace` green +- New hermetic ratchet `symbolic_cost_tier1_carrier_test.rs` (§7) asserts all 4 verification axes (variant set / refinement carriers (PositiveInt/ExponentialBase/PolyLogExponent/NonZeroRational — all named type aliases per HEAD parser constraint; NOT PositiveRational) / algebra rules sample / STOP-SIGNAL text) +- **INVARIANTS P5 receipt for the new hand-Rust test file** (per claude APPROVE 10773 + codex BLOCKING 014544f4 finding #4): authoring `symbolic_cost_tier1_carrier_test.rs` adds new hand-Rust under `src/v3/compiler/tests/`. Per P5 "Pure Bootstrap" discipline, this PR's body MUST cite **exactly ONE P5 receipt category** with concrete path + LOC count: + - (a) **hand-Rust deletion of equivalent or greater LOC**: cite specific deleted file/lines + LOC count + - (b) **SG-0 census shrink receipt**: cite specific SG-0 cell + shrink delta + - (c) **named-lane T-PB-B ROADMAP row deferral**: cite the ROADMAP row by ID + explicit dissolution-trigger condition + + **Worker MUST pick exactly one and document with concrete numbers, NOT narrative.** Phase F (LinearCost variant removal + fallback dispatch collapse) is the LIKELY (a) source — but worker measures actual LOC at authoring time. If Phase F deletion LOC < new test file LOC, worker MUST pick (b) or (c). Codex 014544f4 BLOCKING explicitly: "feature migration as debt receipt" is NOT a clean P5 receipt — concrete numbers required. +- Pre-existing cost-lens behavioral tests still green (Phase F migration must preserve semantic equivalence: `LinearCost(v)` and `PolynomialCost { var: v, degree: 1 }` must produce identical lens output for all consumers) +- PR body cites: + - Gate #105 closure (Phase G ledger update) + - Canvas PR #2828 + composite Director ratification verbatim Q1-Q5 + §8 (PM msg_a055c38b relaying msg_d86a5987 Q2-Q5/§8 base RECONCILED BY msg_676ad4e7 Q1-α supersession of prior Q1-c) + - 12 anti-patterns receipt-of-compliance (§11) + - 5 reviewer ratchets (§12) — explicit assertion-of-compliance per item + +## §14. Out of scope + +- **Tier 2 variants** (LogLog / InverseAckermann / IteratedLog / HyperExp) — R4-deferred per Director §8. Worker must NOT add these. +- **`Field` consumer migration** beyond cost-lens — Q1-α; Field stays in place unchanged (compare already present) +- **InverseAckermann / IteratedAlgebra mechanism** — canvas §8 finding accepted; not introduced +- **Cost-lens behavioral changes** — this is a carrier-extension PR + Q7 canonical-form-preservation contract change. **Q7 OUTPUT SEMANTICS (Director RATIFIED msg_2c1bfb0e via canvas §6.2)**: `symbolic_cost_of(...)` returns **exact canonical SymbolicCost** with all dominance-sorted terms preserved — NOT dominant-term-reduced (no pre-applied asymptotic-simplification). Big-O projection is the separate derived function `dominant_term(SymbolicCost) -> SymbolicCost`. Consumers that previously expected dominant-only output MUST call `dominant_term` explicitly; this is the Q7 contract change, expected and ratified. Lens output for the Linear→Poly(d=1) atomic rewrite is lossless modulo the canonical-form change (multi-term SumCost where the prior shape may have been dominant-only). Worker tests assert: (1) canonicalize preserves all terms; (2) dominant_term applies §6.2 dominance fold; (3) consumers of `symbolic_cost_of` either accept multi-term output OR wrap with `dominant_term` for legacy single-term consumption. +- **`docs/design-symbolic-cost-algebra.md` rewrite** — out of scope; tracked separately as doc-drift sweep + +## §15. PR body framing template + +``` +Closes gate #105 symbolic_cost_textbook_coverage_landed. + +Carrier extended per Director-ratified Path A Tier 1 (canvas PR #2828; +ratification composite: PM msg_a055c38b relaying Director msg_d86a5987 (Q2-Q5 + §8 base) RECONCILED BY Director msg_676ad4e7 (Q1-α supersedes prior Q1-c) 2026-05-13. + +Net 7 → 9 SymbolicCost variants (Q2-Y collapse Linear into +PolynomialCost(degree=1)): +[paste §5 variant set verbatim] + +Companion substrate (Q1-α): +- Cost-lens-local Rational ordering helpers (NO new OrderedField; derived from existing Field.compare) +- Rational stays as Field> (UNCHANGED) + +STOP-SIGNAL re-reset to 10 (9 ratified + 1 trigger) at algebra.dag:69-72. + +Algebra rules §5/§6 implemented verbatim per canvas; (n!)² → UnknownCost +("(v!)² exceeds Tier 1 — pending R4 named-variant canvas"). + +12 anti-patterns receipt-of-compliance: +[enumerate each + cite that the implementation does not violate it] + +5 reviewer ratchets compliance: +[enumerate each + cite assertion] + +§1.8 row #105 updated: CANVAS_RATIFIED → CONSUMER_LANDED. +``` + +## §16. Reference + +- Director scope-extension ratification msg_2c1bfb0e (Q6 signed-Rational + Q7 SymbolicCost preserves expression + anti-pattern #11) + +- Canvas: PR #2828 / `docs/briefs/r3-substrate-gate-105-symbolic-cost-tier1-canvas.md` +- Director ratification (composite): PM msg_a055c38b relaying Director msg_d86a5987 (Q2-Q5 + §8 base) RECONCILED BY Director msg_676ad4e7 (Q1-α supersedes prior Q1-c) +- Row anchor: PM PR #2824 +- Sibling-witness precedent: `dsl/std/algebra.dag:268-286` (OrderedRing) +- Current SymbolicCost: `src/v3/std/algebra.dag:190-197` +- Current STOP-SIGNAL: `src/v3/std/algebra.dag:69-72` +- Rational: `dsl/std/rational.dag:26` +- `feedback_strict_mirror_vs_novel_substrate_fact` — Q1-α discipline (strict-mirror of existing Field.compare; novel only at lens-local helper layer) +- `feedback_state_space_vs_behavioral_invariants` — Q2-Y refinement-vs-fold discipline +- `feedback_naming_is_aliasing` — §5.1 PolyLog-vs-Product semantic-collision avoidance +- `feedback_no_short_term_solutions` — Q2-Y absorption-over-coexistence + +--- + +**Authored by**: warm-wolf-698 (R3 Substrate Mgr) +**Date**: 2026-05-13 +**Dispatch gate**: PR #2824 AND PR #2828 both merged.