Structural-quadratic walls DELIVERABLE 1: complexity-mechanism coverage audit + execution receipt

.githooks/pre-push

@@ -86,6 +86,7 @@ fresh_artifact_path() {
     docs/plans/reference-grounding-migration.md*) return 0 ;;
     docs/plans/typescript-gap-census.md*) return 0 ;;
     docs/plans/fleet-acceptance-criteria.md*) return 0 ;;
+    docs/plans/structural-quadratic-wall-coverage-audit.md*) return 0 ;;
     dag/**) return 0 ;;
     src/v2/**) return 0 ;;
   esac

dag/gunbc/plan_registry_batch_g.dag

@@ -12,6 +12,7 @@ import gunbc.plans.representation_minimization { representation_minimization_pla
 import gunbc.plans.reference_grounding_migration { reference_grounding_migration_plan }
 import gunbc.plans.typescript_gap_census { typescript_gap_census_plan }
 import gunbc.plans.fleet_acceptance_criteria { fleet_acceptance_criteria_plan }
+import gunbc.plans.structural_quadratic_wall_coverage_audit { structural_quadratic_wall_coverage_audit_plan }
 
 data batch_g_plans: List<Plan> = [
   ci_humming_plan,
@@ -24,5 +25,6 @@ data batch_g_plans: List<Plan> = [
   representation_minimization_plan,
   reference_grounding_migration_plan,
   typescript_gap_census_plan,
-  fleet_acceptance_criteria_plan
+  fleet_acceptance_criteria_plan,
+  structural_quadratic_wall_coverage_audit_plan
 ]

dag/gunbc/plans/expressibility_frontier.dag

@@ -56,7 +56,7 @@ fn expressibility_frontier_body() -> List<MarkdownBlock> {
     },
     p(text: "The reading: anemic-modeling and complexity are not analogous by coincidence — they are **two samples of one structure**. Each has a constructive core (①), a detectable-but-not-yet-walled middle (②), and an undecidable tail (③) that is honestly review-bound forever. The win in each is the **same move**: drag instances leftward — review → lens → construction — and *stop* at the decidability boundary."),
     h2(text: "4. The methodology (and its two failure modes)"),
-    p(text: "For any discipline D we propose to enforce: **partition D's instances into ① ② ③ *before* building enforcement.** The partition is the deliverable; the gate is downstream of it."),
+    p(text: "For any discipline D we propose to enforce: **partition D's instances into ① ② ③ *before* building enforcement.** The partition is the deliverable; the gate is downstream of it. The worked instance for algorithmic complexity is the [structural-quadratic wall coverage audit](structural-quadratic-wall-coverage-audit.md) — every live cost/complexity mechanism located on these three regions, with an execution receipt."),
     p(text: "The two ways to get the partition wrong are exactly DESIGN's two named traps:"),
     ul(items: [
       li(text: "**Region ③ priced as ①** → the **\"never\" trap** (§5): a ratchet sold as a wall. You build a \"gate\" that can never be complete (optimality, leaf-decomposition), then either it silently lets things through (coverage-by-illusion) or it grows without bound chasing completeness (the **purity trap**, §6 — the economic twin). Tell: the gate's success criterion contains \"never\" over an undecidable set."),

dag/gunbc/plans/structural_quadratic_wall_coverage_audit.dag

@@ -0,0 +1,65 @@
+module gunbc.plans.structural_quadratic_wall_coverage_audit
+
+import gunbc.plan { Plan, DissolutionTrigger, HasTrigger }
+import std.markdown { MarkdownBlock, TableBlock, AlignNone }
+import gunbc.plans.md_helpers { h2, h3, p, li, ul, ol, quote, cell, row }
+
+fn structural_quadratic_wall_coverage_audit_body() -> List<MarkdownBlock> {
+  [
+    quote(blocks: [
+      p(text: "Coverage audit + execution receipt (DELIVERABLE 1 of the structural-quadratic-wall lane), authored FIRST so the wall decision is *determined by the census, not searched* (the expressibility-frontier discipline: partition into wall / lens-residue / review BEFORE building enforcement). Goal of the lane: make the OBVIOUS, DECIDABLE bad complexity shapes fail-closed. NON-goals (stated by the brief): a general complexity oracle, and a cost-inference algebra. DESIGN refs: SS1 (displaced cost = time), SS5 (fail-closed; construction over validation; the \"never\" trap), SS6 (lenses are residue; coverage-by-illusion; the purity trap). This is the concrete instance-census under [expressibility-frontier](expressibility-frontier.md)'s \"algorithmic complexity\" column."),
+    ]),
+    h2(text: "1. What this audits, and the one question it answers"),
+    p(text: "The brief orders the census first. The question it must answer is not \"how do we detect quadratics\" but: **is a NEW structural-quadratic wall even on-dial, or is the decidable class already walled and the residue already correctly classified?** ROADMAP SS4 shelves the complexity-gate family explicitly (\"a new wall must displace a measured cost on a pillar path to un-shelve\"), so the census must locate every existing mechanism against the SS5 trichotomy and report what is already covered before proposing anything."),
+    p(text: "Method: inventory every mechanism that models, gates, budgets, or ratchets computational cost / algorithmic complexity / resource use; classify each as a WALL (fail-closed, bad state unwritable or errors), a RATCHET (a committed threshold that can be bumped), a RESIDUE LENS (a Bool check that concedes the bad state is writable), an AUDIT (emit-only, no gate), or INERT (machinery exists, nothing gates on it); record whether it is FLOOR-ENROLLED (a real consumer runs it green-by-execution); and mark whether it addresses STRUCTURAL/algorithmic complexity or merely RESOURCE budgeting."),
+    h2(text: "2. Execution receipt"),
+    p(text: "The one whole-corpus mechanism that runs today is the emit-only `complexity_linearity_audit` bin (a syntactic proxy, NOT floor-enrolled). Ran it against main at commit `6e881a11` via `ctrl-build -- cargo run --bin complexity_linearity_audit` (BuildBuddy remote, exit 0):"),
+    quote(blocks: [
+      p(text: "scanned 1132 file(s), parsed 1132, 10212 fn(s), 428 syntactic finding(s). cost syntactic proxy (Node.body walk): `syntactic_high_match_fanout` = 22 site(s). wildcard arms: total=406 on_roster=75 off_roster=331; triage kernel-permanent=52, migration-debt=23, closed-coproduct-debt=3, open-domain=328. resolved-half roster proxies: non_fold_residue total=78 unrostered=3, inert_carrier inert=12."),
+    ]),
+    p(text: "Reading of the receipt: the whole-corpus mechanism that actually executes is a *syntactic* proxy (match-fanout, wildcard arms) standing in for cost until fn-body reflection grounds (blocked on `decl_facts(roots)` #5966 and compile-graph access gunbc#5364). Its 22 `syntactic_high_match_fanout` hits are a match-count heuristic, NOT an asymptotic-class verdict. The REAL asymptotic engine (`src/v2/lens/cost.dag`, next section) is floor-enrolled but roster-bound, so it never walks these 1132 files. That gap -- whole-corpus reach vs. real asymptotic verdict -- is the entire subject of the lane."),
+    h2(text: "3. The inventory"),
+    TableBlock {
+      header: row(cells: [cell(text: "Mechanism"), cell(text: "Carrier"), cell(text: "Measures"), cell(text: "Class"), cell(text: "Floor?"), cell(text: "Struct/Resource")]),
+      alignments: [AlignNone, AlignNone, AlignNone, AlignNone, AlignNone, AlignNone],
+      rows: [
+        row(cells: [cell(text: "symbolic cost engine"), cell(text: "`src/v2/lens/cost.dag` (`SymbolicCost`, `asymptotic_class_of_cost`, `cost_lens`)"), cell(text: "asymptotic class Constant..Polynomial(deg)..Factorial/Unknown, folded over the Node kernel; loops lower to an iteration product (Linear x Linear -> Poly(2))"), cell(text: "**WALL** (`WallNow`; `UnknownCost` fails to top)"), cell(text: "YES (by exec, `cost/*_test.dag`)"), cell(text: "STRUCTURAL")]),
+        row(cells: [cell(text: "complexity lens"), cell(text: "`src/v2/lens/complexity.dag`"), cell(text: "projects SymbolicCost -> ComplexityBound over a curated roster"), cell(text: "RESIDUE / RATCHET (`RatchetForever`; `complexity_variables_admits` returns true -> concedes writability; roster-bound)"), cell(text: "YES (by exec)"), cell(text: "STRUCTURAL")]),
+        row(cells: [cell(text: "complexity-lowering catalog"), cell(text: "`src/v2/lens/complexity_lowering.dag` (`loop_invariant_hoist`, `catalog_is_sound`)"), cell(text: "whether a cost class is strictly lowerable O(n^2)->O(n); soundness = every rule strictly lowers"), cell(text: "RESIDUE + WALL-after-grounding (catalog soundness is the wall)"), cell(text: "YES (by exec)"), cell(text: "STRUCTURAL")]),
+        row(cells: [cell(text: "intent-linearity lens"), cell(text: "`src/v2/lens/intent_linearity.dag`"), cell(text: "simulated/unrollable chains + lowerable-cost nodes across term-chain / type-forest / import-graph"), cell(text: "WALL-after-grounding (`closure_drift` wall)"), cell(text: "PARTIAL"), cell(text: "STRUCTURAL")]),
+        row(cells: [cell(text: "synthesis / lower-bound gap"), cell(text: "`src/v2/lens/synthesis.dag`"), cell(text: "realization cost vs declared relation's structural lower bound"), cell(text: "RESIDUE / AUDIT (`AdvisoryLens`, never gates -- the SS5 region-(3) residue: optimality is Rice-undecidable)"), cell(text: "tests run; lens advisory"), cell(text: "STRUCTURAL (non-gating)")]),
+        row(cells: [cell(text: "complexity_linearity_audit bin"), cell(text: "`src/v1/stage0/src/bin/complexity_linearity_audit.rs` + `_project.rs`"), cell(text: "syntactic match-wildcard arms + `syntactic_high_match_fanout` (parse-only whole-corpus proxy)"), cell(text: "AUDIT / emit-only (exit 0 unless `--fail-on-findings`)"), cell(text: "NO (scaffold, until #5966)"), cell(text: "SYNTACTIC PROXY")]),
+        row(cells: [cell(text: "termination / DescentEvidence"), cell(text: "`dag/std/termination.dag`; v1 checker `src/v1/complexity.dag` + `CostBound`/`PolyCost` in `dag/std/induction.dag`"), cell(text: "well-founded descent; poly cost bound; `Strict|NonIncreasing|DescentUnknown` bounded lattice, bottom fails closed"), cell(text: "**WALL** primitive (`DescentUnknown` blocks a proof)"), cell(text: "via v1-seed consumers"), cell(text: "STRUCTURAL (termination)")]),
+        row(cells: [cell(text: "realization_width / memory_bounded_fit_count"), cell(text: "`dag/std/realization_width.dag`; actuator `cli_run.rs` `spawn_width_cap`"), cell(text: "memory-bounded parallel width = budget / per-shard peak; caps spawn width so co-resident VmHWM <= cgroup cap"), cell(text: "**WALL** / actuator (real floor consumer, fail-closed under-parallelize)"), cell(text: "YES (real consumer)"), cell(text: "RESOURCE (memory)")]),
+        row(cells: [cell(text: "budget tree (accounting)"), cell(text: "`dag/extdeps/accounting/budget.dag` (`admit_line_item`); `dag/product/budget_tree.dag` (`node_conserves`); `dag/gunbc/ci_budget_tree.dag`"), cell(text: "capped-resource -> line-item admission (Memory); conservation Bool"), cell(text: "admission construction (over-cap unwritable on the admit path) + RESIDUE (`node_conserves` for raw literals)"), cell(text: "YES (`*budget*_witness_test.dag`)"), cell(text: "RESOURCE (memory/money)")]),
+        row(cells: [cell(text: "node_wall_clock_ratchet"), cell(text: "`dag/gunbc/test_node_wall_clock_ratchet.dag`"), cell(text: "committed roster of test names permitted to emit wall-clock/time warnings"), cell(text: "RATCHET (bumpable roster)"), cell(text: "via testgen oracle"), cell(text: "RESOURCE (wall-clock)")]),
+        row(cells: [cell(text: "EffortBudget (op-count)"), cell(text: "prose only in `dag/gunbc/plans/budget_tree.dag`; nearest live: `estimate_expr_size` `budget: Int` guard in `src/v1/complexity.dag`"), cell(text: "op-count recursion budget"), cell(text: "INERT (no `EffortBudget` type exists in the tree)"), cell(text: "NO"), cell(text: "RESOURCE (op-count)")]),
+        row(cells: [cell(text: "algebraic-rewrite optimization"), cell(text: "`dag/gunbc/plans/algebraic_rewrite_optimization.dag`"), cell(text: "design spec for an O(n^2)->O(n) rewrite catalog + `Unknown` dissolution"), cell(text: "INERT / design-only (POST-STABILITY; no rewrite rows exist)"), cell(text: "NO"), cell(text: "STRUCTURAL (unbuilt)")]),
+        row(cells: [cell(text: "resolver-pathology quadratics"), cell(text: "targets in `v1_compiler_infer.rs` `build_type_env` / `seed_kernel_intern_table`; tracked `dag/gunbc/plans/representation_minimization.dag`"), cell(text: "whole-ancestry-per-module resolve, `func_env.sigs` module x closure-width, per-module intern_table copy"), cell(text: "AUDIT / MEASURED (VmHWM probe; being killed by sibling lanes) -- NO shape gate against reintroduction"), cell(text: "symptom bounded by the memory WALL (#8), not the shape"), cell(text: "RESOURCE symptom, STRUCTURAL root")]),
+      ],
+    },
+    h2(text: "4. The verdict -- the structural-quadratic class partitioned"),
+    p(text: "Placing the census on the expressibility frontier's three regions for algorithmic complexity yields a clean, and somewhat surprising, result: **the decidable structural-quadratic WALL already exists.**"),
+    ul(items: [
+      li(text: "**Region (1) -- Wall (already built).** Budget-dominance over the symbolic cost fold is decidable and IS walled: `cost.dag` `cost_lens` carries `WallNow`, folds `SymbolicCost` over the Node kernel, and detects Poly(2) structurally (Linear x Linear). `termination.dag` + the v1 `DescentEvidence` checker wall non-termination fail-closed. The memory actuator (`realization_width`) walls the resource symptom. So the OBVIOUS decidable quadratic *shape* -- a per-element loop whose body is itself linear in the whole input -- is already caught where the cost engine reaches."),
+      li(text: "**Region (2) -- Lens-residue (the real gap).** The cost wall is **roster-bound** -- it does not walk the 1132-file corpus. Whole-corpus reach (ROADMAP SS3 `3-gates-whole`) is a SS5 residue that is *decidable but not yet unwritable*, and it is **blocked on the same reflection host-builtin** (`decl_facts(roots)` #5966, compile-graph gunbc#5364) that the emit-only audit bin is scaffolding around. The resolver-pathology quadratics live here too: measured, being killed by sibling lanes (bold-ibex-109 compositional `build_type_env`; representation-minimization), but with NO structural wall against *reintroduction* -- the floor memory cap bounds the symptom, not the shape."),
+      li(text: "**Region (3) -- Review forever.** Optimality (\"is this minimal cost?\") is Rice-undecidable; synthesis (\"produce a faster version\") has no constructive patch. `synthesis.dag` is honestly `AdvisoryLens` / never-gates, and `complexity.dag` is honestly `RatchetForever`. Pricing either as a wall would be the SS5 \"never\" trap."),
+    ]),
+    h2(text: "5. Recommendation (what the census determines about the wall)"),
+    ol(items: [
+      li(text: "**Do NOT build a new complexity oracle or cost-inference algebra.** The brief forbids both, and the census confirms the asymptotic engine already exists (`cost.dag`); a second one would be a SS3 fork of the cost authority."),
+      li(text: "**The only on-dial structural-quadratic wall increment is extending `cost.dag`'s reach whole-corpus** -- but that is region-(2) residue **blocked on `decl_facts(roots)` #5966 / gunbc#5364**, the identical blocker that shelves ROADMAP SS3 `3-gates-whole`. Until that host-builtin grounds, a whole-corpus asymptotic wall cannot be built without duplicating the emit-only syntactic proxy, which is exactly the scaffold to be dissolved, not extended."),
+      li(text: "**The measured-cost residue with the strongest pillar claim** is a *reintroduction wall* for the resolver-pathology quadratic shape once the sibling lanes land their fix -- a structural fence so the killed O(corpus^2) `build_type_env` shape cannot be re-authored. This is the single candidate that could \"displace a measured cost on a pillar path\" (ROADMAP SS4's un-shelve bar), and it should be sequenced AFTER bold-ibex-109 lands, co-designed with that lane, not raced ahead of it."),
+      li(text: "**Net:** DELIVERABLE 1 says the decidable class is already walled where reflection reaches; the wall lane's real content is not a new detector but (a) the blocked whole-corpus reach and (b) a post-fix reintroduction fence -- both gated on other lanes. Escalate the sequencing decision rather than improvising a redundant oracle."),
+    ]),
+  ]
+}
+
+data structural_quadratic_wall_coverage_audit_plan: Plan = Plan {
+  slug: "structural-quadratic-wall-coverage-audit",
+  title: "Structural-quadratic wall -- coverage audit and execution receipt",
+  body: structural_quadratic_wall_coverage_audit_body(),
+  dissolution: HasTrigger {
+    text: "Dissolves when the whole-corpus asymptotic cost gate grounds (`decl_facts(roots)` #5966 + compile-graph gunbc#5364 land, flipping cost.dag from roster-bound to whole-corpus): at that point the region-(2) \"un-walled residue\" rows close, the emit-only `complexity_linearity_audit` bin is deleted, and this census is superseded by the live gate's own coverage report. Also re-run the section-2 receipt whenever a sibling lane lands a resolver-pathology quadratic fix, to confirm the reintroduction-fence candidate is still measured-live."
+  }
+}

docs/plans/expressibility-frontier.md

@@ -52,7 +52,7 @@ The reading: anemic-modeling and complexity are not analogous by coincidence —
 
 ## 4. The methodology (and its two failure modes)
 
-For any discipline D we propose to enforce: **partition D's instances into ① ② ③ *before* building enforcement.** The partition is the deliverable; the gate is downstream of it.
+For any discipline D we propose to enforce: **partition D's instances into ① ② ③ *before* building enforcement.** The partition is the deliverable; the gate is downstream of it. The worked instance for algorithmic complexity is the [structural-quadratic wall coverage audit](structural-quadratic-wall-coverage-audit.md) — every live cost/complexity mechanism located on these three regions, with an execution receipt.
 
 The two ways to get the partition wrong are exactly DESIGN's two named traps: