Cost is a type,
not a measurement.

The finding

A budget refused an exponential blow-up before running it — and was right.

An agent had to pick one of four plans under a fixed budget. The highest-utility plan was a trap: an exponential tower. Weave certified each plan’s cost class statically; the kernel annihilated the unaffordable classes; the survivor ran to a real answer. Then we ran the refused tower anyway — it detonated, vindicating a refusal made with no execution.

How the stack composes

Two languages, one decision.

The author writes ordinary-looking Elixir. The analyzer (Weave) reads the IR and certifies cost. The kernel (box-and-box) governs. Execution is the last step — and only for what survived the floor.

End to end · the actual transcript

One agent. Four plans. One budget.

elixir surface/weave_govern.exs — Elixir surface → Weave certificate → box-and-box kernel → execution. Every rank below is the real Weave.classify verdict; the floor decision is real box-and-box; the values are real reductions.

①  Weave authors (defweave) + STATICALLY certifies each plan — no execution:

   sum_small  (fold + [1..5])   util= 5  →  certificate: rank 1  polynomial
   sum_big    (fold + [1..20])  util= 7  →  certificate: rank 1  polynomial
   pow        (c3 c2)           util= 9  →  certificate: rank 2  exponential
   blast      (c2^5 tower)      util=12  →  certificate: rank 2  exponential

   ⚠ a naive utility-maximizer would pick the highest util: "blast" (util 12).

②  box-and-box governs the certificate (admit rung ≤ 1; floor-then-gradient):

   ▸ verdict: sum_big (fold + [1..20])   (margin 2 over runner-up)
   ranking (affordable, by utility):
        7  sum_big    (fold + [1..20])
        5  sum_small  (fold + [1..5])
   annihilated by the floor (0̲):
        ✗ pow    (c3 c2)       (raw util 9  → 0̲)  σ: cost:exponential@rung2
        ✗ blast  (c2^5 tower)  (raw util 12 → 0̲)  σ: cost:exponential@rung2
   ledger (closed/conserved): funded 5 → spent 3 on the verdict → 2 remain.

③  The [&] agent RUNS the governed choice — a real answer, cheaply:

   ▸ sum_big (fold + [1..20])
     normal  ⇒  210   (157 interactions)

④  VINDICATION — run the refused, highest-utility plan anyway:

   ▸ blast (c2^5 tower)
     💥 OVER-SPACE — DETONATED after 623 interactions (budget blown).
     The certificate refused it STATICALLY — Weave never had to run it to know.

══════════════════════════════════════════════════════════════════════
  naive agent → 💥 detonation.   [&] agent → 210.   Cost is a type, and the type decided.
══════════════════════════════════════════════════════════════════════

The mechanism

The floor annihilates a class, not a number.

A budget admits a cost class (here: polynomial and below). A program in a higher class isn’t “expensive” — it’s a class the budget can’t price, so it carries an unresolved conflict and the bridge’s floor sends it to 0̲. No utility, however large, resurrects it. This is the same floor pattern box-and-box already uses for forbidden actions.

box-and-box is the eight-rung [&] governance kernel; this demo lives on its resource rung (the affine ledger). box-and-box’s rung is a runtime ledger — “what was spent.” Weave supplies the missing piece: the static certificate — “what can be spent, in what class, with termination guaranteed.”

New · the lego layer

The same floor that refuses also lets capabilities compose.

Weave’s certificate is one input to a bigger move: in box-and-box (the [&] governance kernel, now npm i box-and-box) a capability is a Brick — a holder, a |> contract, a modal value, a Weave cost certificate, and CC2 quantities, all in one object. Bricks snap together two ways, and the same absorbing floor 0̲ you just met keeps every composite honest. A brick of bricks is a brick.

graphonomous ▸ weave ▸ box-and-box composes itself: retrieve, then certify (the Weave certificate), then govern (floor-then-gradient) — and survives. Swap in an uncertified step and the pipe floors. The same three rungs that decide a one-shot verdict now decide a composite one.

# the kernel + the compose runtime, one zero-dep package
import { Brick, composeAnd, composePipe, ZERO } from "box-and-box/compose";

# a coalition (&) and a pipeline (|>)
const team = composeAnd(retrieve, certify);     // run together
const line = composePipe(retrieve, certify, govern); // run in phase

# an uncertified child poisons the composite to the floor
composePipe(retrieve, uncertified) === ZERO;   // 0̲  ✓

Proof you can check without running anything

Six claims, each backed by committed text.

The repo’s proofs/ holds the exact stdout of every script and a by-hand-checkable receipts bundle (finite differences, column scans, integer equality). If a committed file differs from what you regenerate, the proof was fabricated. It isn’t.

The honest ledger

The claim is exactly this large, and no larger.

Carried into the proof, not buried.

• Soundness is empirical over the tested population — not a mechanized theorem.
• classify’s rank is a validated proxy; EAL upgrades it to a certificate only on the inferable fragment, and abstains elsewhere — never “proven non-elementary.”
• The polynomial degree is measured; static LAL (Light-Affine, Baillot–Terui §-boxes) inference is the named next step.
• The HVM4 cross-check and the Elixir surface depend on external tools; their output is committed so a bare checkout can still see the result.