Dev - #5

…signatures

Prim gains S (= T², diag(1,i)), X, and Z, exact in the dw ring; both
engines dispatch unary gates through one shared Store::apply_gate1, so
lockstep stays a single-implementation comparison. apply_signature and
the qvm entry points take &[Prim] — any length, any gate set; every
existing call site coerces unchanged. qcensus grows --sig (names,
comma-separated) with the actual order stamped into the report header;
the canonical frozen five remain the default and Prim::ALL.

The odd-sector monitor panics on foreign-gate effects: its mask algebra
is derived for the canonical universe only, and an alternate-universe
trace reaching it is a scoping bug, not data.

Verified: lockstep qvm-vs-qeval green on two alternate universes (the
six-prim frozen+S and a Pauli-heavy five), exact S/X/Z single-qubit
actions pinned, full suite 135 passed; qcensus --sig with the canonical
order is byte-identical to the default run at 4..22.

Co-Authored-By: Claude Fable 5 <noreply@anthropic.com>

…ugh application heads

bb_nf now threads a spine flag (root's own head-reduction demand,
carried through head descents and β-contracta, dropped at argument
descents and under binders). A Diverge landing on-spine via redex-
history reoccurrence or redloop certifies the root has no weak head
normal form; oracle fires never qualify (no-nf leaves a whnf
possible). Verdicts, check order, and every meter charge are
bit-identical to the unparameterized engine.

The census keeps a monotone cross-size set of no-whnf facts and kills
App-rooted terms whose head (a strict subterm, hence a closed term
adjudicated at a smaller size) is in the set: M no-whnf ⇒ M N no-whnf
⇒ no nf, for every N. Kills feed the λ-wrap memo as Diverge seeds and
are no-whnf facts themselves. Facts ride the checkpoint (v2, W lines)
and the memo files, making them part of the delta protocol: a cold
delta run is halt-identical but may report Unknown where the sweep's
accumulated facts prove Diverge.

Measured on the full 4..40 sweep: halt/diverge/unknown bit-identical
to canonical at every size; 638 head-memo kills rerouted around the
ladder (escal column drops accordingly, e.g. 256636→256514 at n=40);
24,178 no-whnf facts. Zero frontier flips — all six App-rooted
standalone-diverging heads of frontier unknowns prove out as
off-spine divergers (they have whnfs), so the 8 candidate unknowns
are genuinely compositional. Canonical table regen to follow for the
escal column and sorted unknown order.

Co-Authored-By: Claude Fable 5 <noreply@anthropic.com>

…, classical-skeleton kills

The quantum census was a single-rung engine (one qvm run per program,
no escalation path). This adds the ladder's instruments:

- --dump-unknowns FILE: programs with any Unknown leaf, sorted per size;
- --terms-file FILE: batch re-adjudication under any budget/signature,
  one line per program with leaf-fate counts and exact summed halt mass;
- --skeleton CAP: classical adjudication of the program applied to one
  free rigid variable per signature slot, via the new oracle-free
  bb::normal_form_spine. Only skel=nowhnf transfers to the quantum run:
  a head chain that never terminates never demands a primitive, so the
  classical and quantum chains are isomorphic under the substitution and
  no branch can Halt — a proven diverger. Off-spine skeleton divergence
  sits in argument positions where a measurement outcome could erase it,
  and skeleton halts prove nothing (δ-rules continue where the rigid
  form stopped).

normal_form_spine disables the syntactic oracle so every Diverge is
history/redloop and spine-attributable — the oracle fires first on
exactly the Ω-shapes the history would prove on-spine (canonical path
unchanged: the oracle gate defaults on, verdicts bit-identical).

First measurement, sizes 4..26 (120 Unknown programs, led by Ω sig and
its λ-wraps): 108/120 skel=nowhnf — proven divergers — and 12/120
off-spine; zero skeleton halts or unknowns. 16× transition budget
resolves none of the 120, confirming budget was never the frontier.
Full 4..41 sweep queued behind the classical regen.

Co-Authored-By: Claude Fable 5 <noreply@anthropic.com>

Fates provably invariant: halt/diverge/unknown, max|nf|, and beta_total
bit-identical to the previous generation at every size (verified
column-wise pre-commit); the subtraction identity holds unchanged
(raw 4532 = 297 kills present + 4235 frontier). What moves: the escal
column (747 head-memo kills at n=41 alone reroute around escalation —
47,007 no-whnf facts accumulated across the sweep), witness lines now
recorded per size under the partition-independent total tie-break, and
unknowns.txt reordered to sorted (content-identical; accumulation order
was thread-count dependent). Ω/K outputs are untouched by construction
(they depend only on fates and nf sizes).

Co-Authored-By: Claude Fable 5 <noreply@anthropic.com>

…holes

Codex's adversarial round disproved the shape-replay lemma behind
treating normal_form_spine's history fires as certified transfers:
bot_free conflates live placeholders with dead ⊥ while simplify
distinguishes them (simplify(D x) = x x but simplify(D ⊥) = D ⊥), so
equal stored shapes do not determine the next stored shape. No false
verdict was found (a 1,061-fire smoke test under four substitutions
came back clean), but discovery and certification are now split per the
repo's standing pattern: normal_form_spine discovers, src/skel.rs
certifies.

The checker reduces p X₁…X₅ by plain leftmost-outermost β — named
opaque holes as root-free variables, no simplify, no oracle, no
history abstraction — and aborts the moment the search touches a
hole-headed application. Verdicts, each with an exact transfer
theorem: Loop (exact state recurrence ⇒ the deterministic chain is
infinite, no δ ever demanded ⇒ zero Ω_success mass), HoleFree (closed
residual ⇒ classical SEMANTIC verdicts transfer both ways — Halt with
empty store at full mass, or proven no-NF), NormalWithHoles (inert
holes in a normal form are bare-primitive values under σ ⇒ quantum
Halt), HoleDemanded / CapOut (no claim).

qcensus --skeleton-only sweeps a terms file through the checker plus a
classical ladder on hole-free residuals, never touching qvm (the qvm
rerun per Unknown was the dominant cost of the naive plan). Tier-1
caps (256 steps, 16k bits) are microseconds-grade and verdict-
equivalent to 4096/1M caps on the measured population: the ≤26-bit
frontier adjudicates as loop=81 div=7 holedemanded=5 capout=27 in
0.0s — 88/120 TRUSTED kills against 108/120 discovery candidates, the
gap being growing loops that never exactly recur (hole-parametric
pattern recurrence is the designed rung above).

Co-Authored-By: Claude Fable 5 <noreply@anthropic.com>

Co-Authored-By: Claude Fable 5 <noreply@anthropic.com>

…rived f64 display

The census checkpoint machinery moves to src/ckpt.rs as a generic
Ckpt<R: CkptRecord> (v3 format: driver-owned body lines between G/E
markers, config-pinned header, torn suffixes discarded at the first
malformed line). census::Stats and qcensus::Tally implement the record
trait; qcensus grows --checkpoint/--groups with the same group-
sequential per-size loop, deferred unknown dumping under resume, and
everything verdict-relevant pinned in the header (range, budgets,
cond-k, the signature universe).

One real fix surfaced by the port: the report's f64 columns came from
the running float mirror, whose rounding is merge-order dependent —
a checkpointed run could differ from monolithic in display low bits.
They now derive from the exact ring values whenever those hold
(correctly rounded and grouping-independent); the mirror only surfaces
for OVERFLOW rows.

Verified: qcensus chunked, restored, and kill-9/torn-tail resumed runs
byte-identical to monolithic at 4..26 (exact and f64 columns both);
census v3 chunk-equivalence bit-identical on 4..30; suite 143 green,
clippy clean.

Co-Authored-By: Claude Fable 5 <noreply@anthropic.com>

…er term depth

The full-frontier skeleton sweep overflowed rayon's default 2MB worker
stacks (deep Term recursion in step/beta plus recursive Rc drops on
grown terms); same lesson and same fix as the census escalation pool.

Co-Authored-By: Claude Fable 5 <noreply@anthropic.com>

STATUS carries the day's measured state: fate-invariant canonical regen
under the r7 engine, the checkpoint/delta protocol, parametric
signatures, and the quantum frontier adjudication (815,700 proven
divergers, 74.45% of unknown mass, Ω_success bracket 3.91× tighter)
with the escalation-lane docket and the queued signature-universe
campaign. Ledger entry for the session; README driver table touch;
crate version 1.1.0 on dev (crates.io release stays 1.0.1 until a9
publishes).

Co-Authored-By: Claude Fable 5 <noreply@anthropic.com>

…on, settled protocols

escalation.md rewritten to state the discovery/trusted-checker split as
the architecture, with the bot_free/simplify counterexample on record;
rung 2 (erasure) marked implemented; new rung 3 = ratified
hole-parametric pattern-recurrence design; canonical kill-manifest
protocol section added. STATUS: div provenance split (58,373 oracle /
45,028 bb), 37 residual-Unknowns corrected (residuals 74..11,978 bits,
none in-range — the 28 frontier members are source programs), tier-2
sweep stopped by design pending CapOut telemetry, docket reordered.
Sorted-stream digests double-computed (Codex + local, identical).

Co-Authored-By: Claude Fable 5 <noreply@anthropic.com>

…s, lab feature

blc/{term,wire,enumerate} + crate-private reduction kernel; classical/
{reference,machine,oracle,escalation,certificate}; quantum/{reference,
machine,scalar,sig,certificate} with shared semantic types at the pillar
root and radical merged into scalar; odd+oddmin behind the non-default
lab feature, certificate discovery routed through cfg(any(test, lab)) so
the soundness battery stays in default `cargo test` as a crate unit test.

Library deps drop to im-rc alone (rayon is cli-feature-only; ckpt uses
available_parallelism). parse_prefix is now an explicit-stack parser —
deep wire-legal towers no longer abort — with exhaustive ≤20-bit
round-trip, prefix-boundary, and strict-prefix-EOF tests. Dead surface
deleted (Pool::emit, trace_accepts, var_weight, HeadPat::matches,
Abort::DescendCap, Sink::var default body, seven stray FROZEN copies →
quantum::sig::FROZEN, Prim::ALL → CANONICAL_SET); pools hide their
arenas behind node()/len(); decode_str rejects junk instead of coercing.

Verification: fmt/clippy clean (-D warnings, all feature combinations),
147 tests green all-features + 107 no-default-features, spot-check 4..28
and qcensus 4..30 bit-identical to canonical tables, rustdoc -D warnings
clean. Bins unchanged in behavior; docs update lands with the docs pass.

Co-Authored-By: Claude Fable 5 <noreply@anthropic.com>

src/cli/: shared parser (typed errors, --help at every node, duplicate/
leftover rejection, strict read_terms_file), dispatch grouped by
epistemic tier, ckpt.rs moves in from the library. census's --term/
--terms-file become `blam adjudicate`; qcensus's --skeleton-only becomes
`blam q skeleton`; qradical+qcomplement merge as `blam q galois
idiom|complement` (one parametric mentions walk, one witness cap); new
engine-exposure commands `blam normalize` and `blam q run`. qpilot is
deleted — the frozen signature lives as quantum::sig::FROZEN with an
order-pinning test. One range grammar everywhere: positional [MIN] MAX.
Lab-gated commands are recognised without the feature and say how to
get themselves. Scripts, CI (+ default-features test run), certlean
banner, and README's driver table updated in the same change.

Verified: payload byte-identity against captured baselines for all
twelve legacy invocations (census/adjudicate/solomonoff/q census/
q selfint/cert search/trace single/slots/galois idiom+complement/
q oddmin); 297 Lean certificate bodies regenerate byte-identically;
fmt/clippy/doc -D warnings clean across feature combos; spot-check 4..32
bit-identical; 21 help nodes and 26 error cases exercised.

Co-Authored-By: Claude Fable 5 <noreply@anthropic.com>

`classical::ladder` is now the single implementation of prescan ->
oracle -> KN rung1 -> KN rung2 -> escalation -> KN rescue.  census,
adjudicate, and solomonoff each had their own copy; the three had
already drifted (adjudicate ran the KN rungs at the machine's 1<<22
transition floor instead of the measured 64x-beta caps, and took its
big-budget attempt before the escalation engine rather than after).
LadderCfg's Default is the census-measured configuration that generated
data/classical/census_table.txt; LadderOutcome is a typed verdict plus
the rung and the telemetry the census reports.

The census's cross-size memos stay in the census driver, on top of the
ladder: they reuse one term's fate for a different term, which is a fact
about an enumeration, not about a term.

Engine env-freedom: the work-meter multiplier and redloop probe fuel are
an explicit EngineCfg threaded from LadderCfg, with a Run context
carried down the recursion in place of the ORACLE_ON thread-local.  WORK
and HEAD_DIVERGE get Drop-restoring guards, so a panicking worker no
longer leaves a poisoned meter behind for every later term on its
thread.  normal_form/normal_form_spine keep their signatures as thin
env-reading shims for the quantum drivers and the slot search, which
migrate with their own lanes.  Meter parity is untouched: no charge site
and no evaluation order moved.

Escalation surface: LamN/AppN fields private; emit_bits replaces
lterm_bits and solomonoff's emit_lterm; LTerm::from_pool replaces three
copies of lterm_of; DEFAULT_CAP; simplify private.

Census cleanups: rung2_over deleted (it counted successes past a cap
that was also the run's transition limit, so it was 0 by construction);
the redex-free prescan count is now reported per size; --dump-unknowns
truncates on the run's first write instead of accumulating across runs;
--chunk under --checkpoint warns; one Rec codec now serves both the
memo file and the checkpoint body.

Ckpt hardening: blamckpt v4 pins the record format, the engine tunables,
and the sha256-16 of any --memo-in file (dependency-free SHA-256 with
the published vectors asserted).  Ckpt::open streams the file instead of
slurping it, treats a header-less file as fresh, and the config-mismatch
refusal prints both configs.  tests/ckpt_resume.rs drives the real
binary: SIGKILL and a deterministic torn tail both resume to the
monolithic table, and six different flag changes are each refused.

Verified: spot-check 4..32 bit-identical to the canonical table; census
4 36 stdout table rows and stderr bit-identical to the pre-change binary
(only the new prescan line and the rung2 rewording differ); solomonoff
4 24 summary and table byte-identical; the 4..30 -> 31 delta protocol
still reproduces the monolithic row; adjudicate produced 1,039,287
verdict lines across the full 4..26 and n=32 populations plus the first
50 census unknowns with zero changed lines.

Co-Authored-By: Claude Fable 5 <noreply@anthropic.com>

Phase 3 Lane B. The certificate layer had the same ladder written twice
and the same helpers written four times; this collapses each to one.

- search_impl::try_kill(t, &CertBudgets) is the ONE sweep — discovery
  streams candidates through verify, try_htr, try_selector, first
  acceptance wins — returning a typed Kill carrying the trusted
  checker's own report. `cert search` (which keeps its hnf descent on
  top) and the soundness battery both route through it. CertBudgets
  carries steps/nodes/lemma_steps with SWEEP and THOROUGH named, and
  the measured kill-equivalence comment lives with them.
- check_common_shape holds the five gates all three verifiers share;
  the eraser and P gates stay beside their own obligations.
- peel_to_bottom and htr_eraser_candidates are exported from the
  untrusted layer (placement is the trust argument) and replace four
  verbatim copies of the peel plus certdiag's private candidate pool
  and its private rename_meta.
- init_search became init_landing, returning the landing state whole
  (steps, tower, binders, trail). certlean reads its Lean data off that
  return instead of replaying the head trace and re-deriving it, so the
  replay loop and its drift panic are gone.
- impl FromStr for PTerm, the exact inverse of Display, with a
  round-trip test; certlean's private parse_pterm family is deleted.
- cert's private shift is now shift_above, noting that its cutoff
  convention (>) differs from escalation's (>=).

Verified: battery green under default features (and no-default and
all-features); `cert search` byte-identical on 100 frontier unknowns and
on all 297 kills (every RATCHET/RATCHET2/SELECTOR and -ARG format);
regenerated lean/Certs byte-identical; `cert diag` CSV byte-identical on
60 frontier terms; scripts/recert-kills.sh end-to-end — 297 kills
reproduced at 4x budgets, lake kernel-check green.

Co-Authored-By: Claude Fable 5 <noreply@anthropic.com>

…e ladder

Phase 3 Lane C. Science output is byte-identical throughout; the three
verification sweeps and the checkpoint codec round-trip all reproduce the
pre-change binary exactly.

scalar
  ExactSum replaces `Exact` and qcensus's private `Ex` twin. Overflow is
  structural (enum Value/Overflow), so there is no field that reads the
  same whether or not the sum held: `value()` is the Option, `expect_exact`
  the loud accessor, `partial()` the explicitly diagnostics-only one. It
  carries the f64 mirror and the one checkpoint codec both files needed.
  `Dw::real_parts` becomes the single place that recognises a real element;
  is_real, try_sign_real, and radical_parts are built on it. try_sign_real
  is the fallible variant, so cmp_real's documented f64 fallback now covers
  the whole path rather than just the subtraction; sign_real's two
  unreachable equality arms (a² = 2b² has no nonzero integer solution)
  collapse into one predicate with a debug_assert.

machine
  QProgram { enc, len, cond, order } folds run_program_into and
  run_conditioned_into into `run_into_with`, retiring the
  too_many_arguments allow. `machine::run` is the one-call entry that owns
  its arenas. Budget::validate is shared by both engines: a degenerate
  budget is where their β-check placement stops agreeing, so neither
  accepts one. The readback's defensive frame arms keep their release
  behaviour behind a debug_assert.

sig / certificate
  `sig::with_holes` and `sig::church_numeral` are the one source of the
  skeleton shape, used by the trusted checker and by the census's
  --skeleton column, which had hand-rolled both. `adjudicate` returns
  Result<_, OpenProgram>: an open program's own free variables would be
  silently reinterpreted as signature slots. CapOut carries reason
  (Steps|Size), steps, and high_water_bits — escalation.md's rung-3
  prerequisite. `adjudicate_with_transfer` promotes the residual ladder out
  of the CLI to sit beside the transfer theorems that license it, and
  builds the residual straight from the tree instead of round-tripping it
  through the wire format.

sweep
  quantum::sweep::run_and_summarize is the per-program step all three
  sweeps share, with the mass-conservation battery inside it so no sweep
  can quietly skip what the others assert.

cli/q
  q skeleton is a thin driver again; its per-item Mutex is gone in favour
  of for_each_init + atomics, and it regains the `--sig LIST` it lost in
  the Phase 2 extraction (slot count = the parsed signature's length).
  galois: consumed_mentions is the one parametric walker, CappedWitnesses
  the one witness-cap invariant across eight lists.

odd
  The S/X/Z arm becomes Malformed::OutOfUniverse — the soundness fence
  stays, it just reports instead of aborting a sweep.

Verified against the pre-change binary:
  q census 4 28 report + stdout + --dump-unknowns: identical
  q census --terms-file --skeleton [--cond-k 3] on 200 frontier lines: identical
  q census 4 22 --checkpoint resume vs monolithic: identical
  q galois idiom / complement 46 47 --mode count: identical (modulo timing)
  q skeleton on 200 frontier lines, sorted verdict stream: identical
  q run on witness45: identical
  fmt + clippy + tests green on all three feature combos

Co-Authored-By: Claude Fable 5 <noreply@anthropic.com>

…n, survivors on a work queue

A range-split `par_iter` balances generation well and expensive terms
badly: rayon splits by index range, so whichever task happens to contain
a nine-million-beta rescue owns that cost alone. The unit of parallelism
for an expensive term should be that term, not the enumeration subtree it
was generated in.

So each checkpoint group now runs in two phases. Phase A keeps generation
fused with the ladder's cheap rungs (memos, prescan, oracle, rung 1),
whose per-task cost is roughly proportional to terms emitted, and returns
the ~0.3% of terms that survived. Phase B re-schedules those one at a time
through an atomic counter, one long-lived Pool/Machine per worker.

The ladder gains two entry points onto the one implementation --
`adjudicate_fast` (rungs 1-3, returning `FastOutcome`) and
`adjudicate_slow` (rungs 4-6) -- with `adjudicate` defined as their
composition, so single-term drivers are untouched. A `Survivor` records
no telemetry, which is why the slow half can start from a fresh
`Telemetry` and the composition is identical on every field.

Groups stay sequential and are appended only after both phases, so the
checkpoint contract and format are unchanged: a kill during phase B costs
exactly the current group, as before.

Measured, on eighteen threads:

                        wall      user     CPU
  census 4 38          250.8s    425.7s    170%   ->  127.0s  438.2s  345%
  census 4 38 --ckpt   389.5s    399.1s    102%   ->  174.0s  408.5s  235%
  census 36 36          35.7s     45.9s    129%   ->   18.4s   45.6s  247%
  census 36 36 --ckpt   40.2s     44.7s    111%   ->   20.2s   45.5s  225%

(--ckpt = --groups 64.) Instructions retired across 4..38 move by
-0.017%; cycles by +4.7%, the cost of running the heavy terms
concurrently. The checkpointed path gains most because 64 sequential
groups per size meant 64 straggler tails.

Identity across 4..38: every scalar Stats field, the 397-member unknown
set, the 195,137 memo H/D/W records, redloop totals, and a per-term
manifest of all 140,883 terms reaching rung 2 (fate, rung, |nf|, beta,
rescue cause, rescue transitions, no-whnf flag, stuck fuel). Every one of
the 2,240 group records at --groups 64 is identical, S line and sorted
body. Also identical: threads {1,2,18} x groups {1,7,64}, a checkpoint
whose first 2,169 groups the old binary wrote and whose last 71 the new
one resumed, two SIGKILLs inside phase B (RSS-confirmed), and the
memo-seeded cold deltas at n=36 and n=38.

Co-Authored-By: Claude Fable 5 <noreply@anthropic.com>

Phase 4b. Every item measured before/after; every canonical output
verified unchanged (q census 4..28 rows against data/quantum/census_table.txt,
q census 4..31 report byte-identical, q skeleton verdict stream identical
over 2000 frontier lines). Wall-clock numbers are single-threaded,
interleaved A/B, min-of-N — the box was under load ~40 throughout.

1. Dw::raise_k is O(1) instead of O(Delta k). Two num_mul_sqrt2 are exactly a
   doubling ((w - w^3)^2 = 2), so an odd Delta k costs one num_mul_sqrt2 and the
   rest is a checked_mul by 2^(Delta k/2). The None contract is preserved point
   for point: iterated doubling is non-decreasing in max |coefficient|
   (|A+C| + |C-A| >= 2|A| and siblings) and an out-of-range coefficient always
   forces an out-of-range successor, so the loop returns None exactly when
   the final value leaves i128 — which is what the checked_mul tests. The
   all-zero numerator skips the factor, since iterated doubling never
   overflows on zeros. K_CAP bounds Delta k/2 <= 64, so the factor always fits.
   Measured: 104ms -> 12.3ms over a 200-value grid x Delta k 0..60 (8.5x).

2. Dw::reduce pair fast path: while k >= 2 and all four coefficients are even,
   shift right and k -= 2. Two inverse steps compose to a plain halving and
   all-even makes both integral, so it cannot over-reduce; the single-step
   loop still handles the tail.
   Measured: 4.09ms -> 0.95ms on values with a 20-bit reducible tail at
   k = 40 (4.3x).

   Items 1+2 at sweep level are a wash — census masses live at small k:
   q census 4 26 -0.6% median, q census 4 28 +0.7% median (both inside noise).
   The win is asymptotic safety, not throughput.

3. reference::run no longer materialises effect traces. run/run_traced share
   run_impl<const TRACE: bool>; Ctx::trace became Option<&mut Vec<Effect>> and
   the primitives emit through a closure, so under TRACE = false nothing is
   pushed, allocated, or cloned at a fork. run_traced is behaviourally
   unchanged.
   Measured: run vs run_traced on trace-heavy programs (gate chains depth
   8..64, and a 9-deep coin tree = 512 branches) -3% to -14%, median ~-6%;
   the QTerm cloning in beta/shift/subst dominates. Three-way interleaved
   lockstep suite (HEAD / items 1+2 / all, 15 reps, RAYON_NUM_THREADS=1):
   2.670s / 2.664s / 2.665s min — no measurable delta, because that
   population is dominated by programs that Err within a few steps and
   never grow a trace.

4. certificate::adjudicate walks each state once, not three times. One
   traversal (write_bits_max_free) produces the wire string, its length —
   provably equal to bit_size, since Var(n) writes n ones and a zero — and
   the largest free index; the buffer is reused across steps and only cloned
   into `seen` on a miss; the up-front bit_size call is gone, since every
   read of high_water is already preceded by the max in the same iteration.
   The recurrence key stays an exact String: Loop is only sound because
   equal keys mean equal states, so this is not a hash.
   Measured: q skeleton over 2000 frontier lines 2.689s -> 2.184s (-18.8%).

Gates: full suite green on all three feature combos (--all-features,
default, --no-default-features); clippy --all-targets and cargo fmt clean;
new exhaustive raise_k edge tests (Delta k odd/even/zero, the i128 boundary
including -2^127 and cancelling pairs, all-zero coefficients) and a reduce
equivalence test, each comparing against a test-local copy of the old
implementation.

Co-Authored-By: Claude Fable 5 <noreply@anthropic.com>

…ambient-apply

Optimization (byte-identical output at W=24 and W=28):

- `Summary::quotient` rebuilt the whole distinct-color BTreeSet inside
  the per-node closure and then scanned it linearly — O(n² log n), and
  16.3% of an oddminproto-28 run. The color vector is built once and
  ranked once through a color→class map.
- The eight library axioms and their adjacency are a process constant
  in a `OnceLock`, not eight `lam_ref`/`prim_summary` builds per splice.
- `closed_accepts` ignored its `MaskAutomaton` argument and built a
  fresh one internally per call. The argument is gone and the automaton
  is interned process-wide (`mask_automaton()`).
- Four per-node scans (explore, the `Cont::Match` dispatch, `side_pure`,
  `side_refs`) filtered the side summary's entire edge list. A per-side
  adjacency index is built once in `Composer::new`; explore and dispatch
  read it by index, so the per-node `Vec` copy is gone too.
- `stale_env` ran the staling twice, discarded the first result, and
  cost three env clones. Val interning is injective, so "holds a live
  distinguished handle" is one id probe; the rewriting path clones once.

Simplification and soundness hygiene:

- One `d_step` — the mask-product transition is the soundness core of
  this lane, and it was duplicated across `accept_product` and
  `accepts_closed`.
- One `defer_ambient_apply`, which ALWAYS performs the closed-mode
  unresolved-ambient check and the `Net::of_action` join. The
  `CPort::Recv` twin lacked the guard its live sibling has; unreachable
  under the collapsed fan, latently unsound the moment it is re-enabled.
- The collapsed observation fan is now explicit: `received_head`,
  `opaque_val`, `resolve_head`'s `PortRef::Received` arms and the
  descent guards say ★-only in the type or trip loudly, and `boundary()`
  moved behind the `pat != Any` test so it stops running per delivery.
- The trusted flatten/product layer no longer answers node 0 by
  default: the root lookups are `expect`, an unrooted exposed port is
  the new `Abort::UnrootedPort` (⊤), and the impossible shapes are
  `unreachable!` rather than a bare `return`.
- `LIB_SLOTS`/`MAX_PORTS` named; the library array is written from the
  `LIB_*` constants alone, with a const assertion on the slot count.
- `prim_arg`'s three H/T/Meas blocks are `unary_on_dcur`/`unary_on_other`
  over a `UnaryPrim` sub-enum, killing three `unreachable!()`s at the
  type level; the thrice-repeated spine idiom is `extend_spine`.
- The three `debug_*` pseudo-test modules are one `mod instruments`;
  `nf_descend` and `Mode::Descend` are test-gated, since the
  instruments are their only callers.
- Module header: the stale `may_accept_latent` sentence is rewritten
  for `materialized_accept_any_root`, and a "Do not simplify" block
  records the ten frozen shapes with their measured reasons.

Gates: `blam q oddmin 24` and `blam q oddmin 28` byte-identical to the
baseline binary (timing lines excluded) — uniq 6271 / closed 6271 /
splice-top 0 / closed-top 37 / accepts [] at 24. Full suite green on
all three feature combos; fmt and clippy clean.

Co-Authored-By: Claude Fable 5 <noreply@anthropic.com>

README, AGENTS, STATUS, both pillars' architecture docs, certificates,
self-interpreter, oddmin, galois, bisimulation: every path, invocation,
and flag now names the v2 tree and the single blam CLI; changelog voice
removed outside the ledger; the ledger gains the v2 reshape record with
verification evidence and deletion rationale. Real fixes along the way:
README's frozen-signature order was listed wrong (h/meas/new/cnot/t is
the pilot's order, now stated with its pinning test); the size identity
disambiguated (X sums 0-based indices); ref/AIT test-dependency
attribution corrected in README/AGENTS/CI (tromp_vectors inlines its
vectors; the submodule feeds uni.rs parity); oddmin's §6 battery is now
a claim→test table with two unbacked claims withdrawn; §7 gains the
measured W=25/26/28 rows (splice-⊤ first appears at 25) and STATUS's
odd-sector state follows; the no-whnf memo and checkpoint/scheduler
sections that were missing from classical architecture exist; the 166M
β/s figure has exactly one authority (STATUS). Census timing restated
from two same-day runs with the wall-vs-user caveat.

Co-Authored-By: Claude Fable 5 <noreply@anthropic.com>

Phase 4c. Four items kept, one dropped as a measured regression. Every
item measured by interleaved A/B leave-one-out (3-4 runs per arm) against
a binary built from the same tree, so ambient load hits both arms
equally — this box ran between 12 s and 39 s for the same binary during
the session, so user time is the signal and wall is reported beside it.

- `Pool::has_redex` answers from a decode-time flag. `decode` already
  visits every App it builds, so it now records whether any had a Lam
  function child and `has_redex` reads that back in O(1). The census ran
  the old body 11.1M times at n=36, each call allocating a traversal
  `Vec` to re-walk a term `decode` had just walked. The root-scoped
  traversal stays for pools built by `push`/`from_term` and for splicing
  callers holding several terms in one arena, where the answer is
  genuinely per-root. `clear` drops the cache, which is what makes it
  sound. Census 34..36: user 85.67 -> 84.11 s, wall 20.78 -> 20.07 s;
  every run of the new arm beat every run of the old.

- `interleave_tasks` permutes via `Option::take` instead of cloning each
  `GenTask`. AGENTS.md pins this order ("do not simplify the order
  back"), so the guard went in FIRST, against the pre-refactor code:
  goldens for the exact output order at m = 1,2,3,5,8,12, an independent
  bit-reversal characterization for m = 2..300, a permutation check, and
  a field-coherence check. Not separately measurable — ~1.1k tasks per
  size against a 20 s sweep — and the guard is the real deliverable.

- The census memo map and no-whnf set take a `BuildHasher` built on the
  engine's own splitmix64 `mix` rather than SipHash. Iteration order is
  never observable: both are only `get`/`contains`/`insert`/`len`/
  `is_empty`, and the one place either is iterated (the `--memo-out`
  writer) sorts by unique key immediately after. `mix` becomes `pub`.
  Census 4..36: user 90.16 -> 89.36 s, a ~1% win at the edge of noise.

- `probe_nf` reuses a thread-local (Pool, Machine) and builds the arena
  through a new `Pool::from_lterm` instead of an LTerm -> bit-String ->
  re-decode round trip. NO measurable win: redloop probes ~1.1k times
  across all of 4..36 (518 proofs + 623 fuel rejects), far too few to
  move a 45 s budget, and census 36 36 is unchanged within noise. Kept
  because the round trip had no reason to exist and because the probe
  comparison MUST stay exact string equality — redloop fires on
  nf(A) == nf(Q(A)), so a digest would turn a hash collision into a
  false divergence proof, an unsound census row rather than a slow one.
  That constraint is now written down at the function. A new test pins
  `from_lterm` node-for-node against the round trip it replaced.

- DROPPED — arena release. Replacing `= Vec::with_capacity(KEEP)` with
  `clear() + shrink_to(KEEP)` is a REGRESSION on the metric it targeted:
  census 36 36 peak RSS 2315-2516 MiB against 1819-2126 MiB for the
  status quo, with no time difference. `with_capacity` commits nothing —
  it is a bare `alloc`, and pages cost RSS only once touched — while
  dropping the vector `free`s the multi-GB block outright, which is the
  whole point of the block. A shrinking `realloc` can be satisfied in
  place and keeps the pages charged to us. `Vec::new()` measured
  equivalent to the status quo (2018-2283 MiB). Both machines keep the
  original code, now carrying the measurement so it is not re-proposed.

Tests: `has_redex` had no direct coverage before this. Four new cases
pin the cache — exhaustive agreement with a cache-free traversal over
all 19,048 closed terms 4..=24, a spliced multi-term arena, a second
decode into a live arena, and a `clear` whose rebuild lands the root on
the same index (that last one fails if the invalidation is removed;
verified by mutation).

scripts/bench.sh rebuilt. Default range 34..36 — the old 28..31 put
every rung at 0.03-0.09 s with ablations producing identical counts.
Rows now carry wall AND user AND the escal column (the "did this change
the work, not just the speed" check), median of 3. Ablations are the
current engine's: prescan, oracle, budget1, rescue-trans-mult, --chunk 1
relabelled as serial GENERATION rather than serial everything, --threads
1, checkpoint grouping, and the --memo-in/--memo-out delta protocol. The
--groups rung says out loud that K sets both the barrier count and the
task-split target (threads x 16 x K), so it is not a one-variable sweep.
Header states the memo warm-up dependence that makes rows incomparable
across start sizes (n=36 reports escal 25268 cold, 18729 from a 4..36
sweep), why user beats wall on a loaded box, and the ~30 min budget.
The build no longer hides errors behind 2>/dev/null.

Gates: full suite green on all three feature combos (206 / 175 / 144
tests); fmt and clippy clean on default, all-features, and
no-default-features. Census spot-check 4..32 bit-identical to
data/classical/census_table.txt. Census 4..36 identical to a
baseline-binary run on the table columns AND on all 112 narrative lines
(prescan counts, memo hits, no-whnf facts, redloop 518 proofs / 623
fuel rejects, max|nf| witnesses, unknown frontier). Solomonoff 4..24
report and solomonoff_table.txt byte-identical to baseline.

Co-Authored-By: Claude Fable 5 <noreply@anthropic.com>

The last environment read leaves the library: the deprecated
normal_form/normal_form_spine shims and their OnceLock env_cfg are gone.
TransferCaps carries an explicit EngineCfg for the residual run; the
q census skeleton column, q skeleton, and the slot search resolve
flag → env → default at the CLI layer like every other driver, and
cert search drops two knobs that never reached an engine. The
escalation test module pins the default-config verdicts as data —
including the spine flags, where an oracle fire (Ω) must NOT mark
no-whnf while a root-chain redloop fire must.

Comment currency: the meter-parity invariant and its per-site notes now
reference "the unshared walk" (an absolute baseline) rather than "the
old engine"; the unresolvable "instance #4" index is gone; solomonoff's
tie-break comment states the rule rather than the history; q skeleton's
module doc describes the tool, not its extraction. Stale BindId and
sig-invocation doc lines fixed; CI's ref/AIT comment attributes the
dependency to the parity step, not the conformance suite.

Co-Authored-By: Claude Fable 5 <noreply@anthropic.com>

…int tears heal

Repair lane R1 of the v2 release review. Three classes of defect, all
reproduced before the fix, plus the API freeze 2.0.0 ships.

INPUT VALIDATION. `Pool::decode_str` stopped at a complete prefix and
ignored the rest, so a longer string silently became a DIFFERENT program
(the code is prefix-free); it is exact now, and the CLI routes every
BITS argument and every terms-file line through one validator that
rejects stray characters, truncation, trailing bits, and open terms,
naming which. That preflight runs sequentially before any rayon fan-out,
so a bad file is exit 2 with a `file:line` rather than a worker panic
mid-sweep, and every consumer's later `expect` is now unreachable.
`q census --terms-file` gained the 1..=64-bit window it never had — a
68-bit halter used to be truncated into a Species error, a 66-bit line
hit an assert whose message checked canonicality, not packability.
Sizes above 63 are refused at parse time (`census 64` used to sweep
4..63 first), degenerate quantum budgets go through `Budget::validate`,
the engine knobs have floors, and a flag belonging to a mode the run is
not in is a refusal naming both flags rather than silence.

OUTPUT FILES. Every user-named output path is created (and truncated) at
startup, in a new `cli::out`: a mistyped `q census --out` used to panic
after the whole sweep. `--dump-unknowns` is one shared sink for both
censuses, truncated at run start, so a rerun replaces rather than
doubles (the quantum one doubled every time, and a stale mixed-size file
then fed `q skeleton` inflated tallies) and a zero-unknown run leaves an
empty file rather than last week's frontier.

CHECKPOINT TEAR. A resume discarded the torn tail from its own view but
appended past it on disk, so every group computed after the tear was
invisible to every later resume — correct results, unbounded
recomputation. `Ckpt` now tracks the offset after the last complete
record and truncates to it before appending; the test resumes twice and
asserts on the file length and the restored-group count.

API FREEZE. `QProgram` validates its bits behind private fields;
`quantum::sweep` moves to the drivers as `cli/q/sweep.rs`; `blc::term`
becomes pub(crate) (the types keep their re-exports); `Pool::reset` is
`clear`; dead `take_head_diverge` is gone; the public error types get
Display + Error. CI gains a rustdoc gate, an MSRV job, and a scan for
invocations of binaries that no longer exist — which caught the one
stale reference left in the tree, in generated Lean headers.

Verified: fmt, clippy -D warnings and cargo test --release across
all-features/default/no-default, rustdoc -D warnings, MSRV 1.87,
spot-check 4..32 bit-identical, and `census 4 24` / `q census 4 24` /
`solomonoff 4 22` byte-identical to their pre-change baselines.

Co-Authored-By: Claude Fable 5 <noreply@anthropic.com>

… banners

Repair lane R2 of the v2 release review. Documentation, scripts, and the
regenerated Lean tree only; no engine change.

- AGENTS.md / docs/classical/architecture.md: the engine-config bullet
  documented `args::apply_engine_env` and the `normal_form` /
  `normal_form_spine` shims, all deleted in 8f950e5. Restated as it is:
  the library reads no environment, every driver resolves flag → env →
  default at the CLI layer through `args::engine_cfg`, `blam slots` has
  no knob flags and resolves env-only through its private `OnceLock`, and
  `cert search` has no engine knobs at all (its budgets are the
  `head_step` steps/nodes/lemma-steps triple).
- docs/quantum/escalation.md and the self-interpreter results ladder now
  name `normal_form_spine_with` / `normal_form_with`, with the
  cfg-as-data note.
- STATUS + README: "the n=32 row has no unknowns, so BBλ(32) is fully
  mechanical" was false. `data/classical/census_table.txt` gives n=32 one
  unknown; it is discharged by the single 32-bit Ratchet kill in
  `data/certificates/ratchet_kills.tsv`, kernel-checked as
  `lean/Certs/Size32.lean`, which is why the frontier starts at 33 bits.
  BBλ(32) is settled modulo the certificate layer, not by the ladder.
- STATUS oddmin: splice-level top is 0, 0, 0, 2, 8 at W=16/20/24/26/28
  per the table in quantum/oddmin.md; the list said 2 at W=28 and then
  contradicted itself in a parenthetical.
- docs/quantum/architecture.md: the conditional Gács construction is §1
  of that same document with its docket in STATUS, not `galois.md`;
  galois.md now appears under what it actually documents.
- scripts/census-regen.sh: the pre-scheduler "~7.2 min" for 4..40 is now
  the measured ~6 min wall (323.6 s and 397.9 s, ~1,980 s user each),
  with 4..41's 16.5 min marked as an un-retimed upper bound.
- AGENTS.md: the "~40 min at eight threads" frontier sweep was never
  re-measured after the reshape. Replaced with a labelled estimate from a
  proportional 202-term sample (every 21st line of the 4,235-term
  frontier): 307 s wall / 1,400 s user at --threads 8, so about eight
  core-hours, order 1-2 h wall.
- AGENTS.md: `blam-reshape` added to the gaslamp thread list.
- README: `cargo add` is the library, `cargo install` is the CLI — a
  dependency does not install a binary. Plus a note that `blam cert lean`
  and the `scripts/` protocols default to repo paths the crates.io
  package does not ship.
- STATUS: a "Release risks" block — `--memo-in` is a trusted semantic
  cache (the checkpoint digest pins identity, not truth); checkpoint
  flush is process-kill recovery, not power-loss durability (no
  `sync_all`); alternate S/X/Z universes and very large budgets carry
  less evidence than the frozen five; the Pool/Node arena APIs assume
  their preconditions rather than checking them.
- docs/ledger/2026-08.md: appended (not edited) a closing paragraph for
  bc7724a and 8f950e5, and one noting the post-landing adversarial
  review.
- lean/: regenerated with the current binary, so the banners say
  `blam cert lean` / `src/cli/cert.rs` instead of `certlean` /
  `src/bin/certlean.rs`. Diff is banner lines only — 11 insertions, 11
  deletions across ten files, zero theorem bodies touched — and
  `lake build Certs` kernel-checks all 297 certificates green.

Co-Authored-By: Claude Fable 5 <noreply@anthropic.com>

Version 2.0.0 in manifest and lock — the reshape is breaking at both
the library and CLI surface. The release pipeline now triggers only on
a completed-and-successful CI run for a main push, with every checkout
pinned to the CI-validated SHA: publication can no longer outrun the
verification bar, and dev pushes never arm it. Publishing remains a9's
call (merge to main after external review).

Co-Authored-By: Claude Fable 5 <noreply@anthropic.com>

parse_prefix promised stack-safety and the value it returned broke it:
Display, to_bits, bit_size, max_free, and Rc's drop glue were all
recursive, so a 400k-bit lambda-tower file parsed fine and then aborted
the process in to_string() — with the reproducer shipped as an example.
All five are now explicit-stack iterative (Drop detaches sole-owned
children onto a work stack behind a thread-local sentinel); derived
PartialEq/Debug stay recursive, named as the exceptions on Term's doc.
The tower test runs at depth 1,000,000 and exercises every operation
plus a plain drop. var() now asserts the 1-based convention, and the
parse_file example prints errors through Display on stderr.

Co-Authored-By: Claude Fable 5 <noreply@anthropic.com>

The no-whnf fact rode a thread-local Cell set deep in bb_nf and read
back by the entry points into an unlabelled bool tuple — now it is
NoNf::Diverge { head_chain }, set at the three fire sites, and the
'_with' suffix on the entry points (whose plain twins no longer exist)
goes with it: escalation::normal_form / normal_form_spine return the
verdict alone. Verdict::Halt's (steps: 0, steps_exact: false) sentinel
pair becomes steps: Option<u64>; Telemetry::escalated (derivable from
rung) becomes LadderOutcome::escalated(); LadderCfg embeds EngineCfg
instead of re-flattening its fields, so drivers assign one struct.
classical::Budget — a mutable out-param counter one function used — is
gone: reference::normalize(t, limit) returns (nf, steps) like the
machine. CertBudgets moves out of the lab gate to sit beside the
trusted verify* checkers, which now take it instead of three bare
numbers in an order nothing else used; the CLI's third undocumented
2000/2000/200k triple is now a named RECHECK const. The four
certificate failure enums and Why get Display + Error. subst_dec skips
the per-binder re-shift of a pattern-closed argument (measured 2.03x
less CPU on the frontier sample; shift_above(s,1,0) is the identity
there). oracle::istest guards the n=0 underflow hand-built terms could
reach. Redloop theorem doc moves onto redloop(); the statics keep one
line each.

Verified: all three test shapes green, clippy clean, spot-check rows
4..32 bit-identical to data/classical/census_table.txt.

Co-Authored-By: Claude Fable 5 <noreply@anthropic.com>

The env arena's (Val, u32) tuple cost 16 B per cell and an enum load
per de Bruijn hop; the cell is now (term, env) with a rigid level
tagged in bit 31 of word 0, parents in their own dense u32 array —
12 B across two vectors, 4-byte hops, a bit test for the discriminant.
Pool::decode reuses an owned build stack instead of malloc'ing one per
term (11.1M times at census n=36; slots.rs learned this lesson long
ago and the flagship sweep never inherited it).

Measured, census 35 35 --threads 1: 24.75 s -> 21.7 s wall (-12%),
peak RSS 1136 -> 798 MiB (-30%). Census row and spot-check 4..32
bit-identical; all three test shapes green.

Co-Authored-By: Claude Fable 5 <noreply@anthropic.com>

Dw::reduce did unchecked i128 pairwise sums on every mul result — a
coefficient near the i128 edge could wrap, and an all-even wrap would
return a silently wrong scalar at k-1, exactly the 'never a wrong
number' contract's counterexample. reduce now tests overflow with
overflowing ops OR'd into one flag (the naive checked_* 4-tuple
measured a 9% census regression; wrapped values are never read), and
neg/conj/sub are fallible like add/mul. T and S apply omega/i as signed
coefficient rotations instead of 16 checked multiplies; H's butterfly
aligns once for both add and sub. ExactSum caches its powf denominators
(measured neutral, kept for the amortization). reference::Found drops a
dead bool and a variant handled identically at all five sites.
Store::amps is private behind an accessor; Store::empty and the
unreachable quantum Pool::len/is_empty are gone; # Panics sections on
the five degenerate-budget entry points and the enumerate asserts; Prim
gets Display/FromStr; q census defaults --trans to the canonical 2^26.

q census 4..30, q run x9 programs x3 universes, and examples/bell all
byte-identical before/after; census user-time at parity.

Co-Authored-By: Claude Fable 5 <noreply@anthropic.com>

blam census stdout now opens with # provenance (version, sizes, the
full ladder line) and marks every non-row line with #, matching q
census; spot-check's row extraction stops guessing by field count.
Ckpt::append returns the house error instead of unwrapping mid-sweep —
the one module whose contract is that a kill costs exactly one group no
longer aborts on a full disk. solomonoff accepts all nine ladder knobs
(it claimed 'the census ladder, verbatim' while accepting two) and
--table is opt-in rather than truncating a file in cwd by default.
File-read failures name their subcommand and hint like every other
refusal; trace scan requires --out instead of clobbering canonical
data; blam help <cmd> routes to that command's help; adjudicate -v
refuses single-term mode where it only duplicated a line. New
examples/adjudicate.rs and examples/enumerate.rs close the two
journeys the README described without code; docs.rs gets all-features
metadata and lab cfg markers; missing_debug_implementations is on with
the 19 offenders derived.

data/classical/census_table.txt regen deferred deliberately: rows are
unchanged (spot-check green against the checked-in table); the # lines
join it at the next canonical regen.

Co-Authored-By: Claude Fable 5 <noreply@anthropic.com>

Each transition allocates at most one env cell, so capping trans_limit
at LVL_TAG-1 makes the bit-31 index invariant structural — no hot-loop
check, and a caller asking for more than the index space gets an honest
Transitions verdict. The old (Val, u32) cell wrapped its u32 index at
2^32 with no guard at all; the tag bit halved the distance to that
latent cliff, so it gets the fence the original never had.

Co-Authored-By: Claude Fable 5 <noreply@anthropic.com>

Codex's adversarial pass over the sweep diff found three edge defects.
(1) reduce's break-on-overflow returned a NONCANONICAL value at the
i128 edge — numerically right, verdict-wrong: is_dyadic reads the
representation, so a dyadic 2^126 witness tested false. The inverse
step now computes its halves directly by the floor identities
((x+y)/2 = (x>>1)+(y>>1)+(x&y&1) and the sub twin) — the halves always
fit even where the sums do not, so reduce is total and always fully
canonical, with the witness pinned as a test. (2) real_parts asked
b == -d, and -d wraps at i128::MIN in release: a purely imaginary
value passed as real; now b.checked_add(d) == Some(0), witness pinned.
(3) Term's iterative Drop skipped shared children, so a hand-built
DAG chain still recursed one frame per level through derived glue —
detach now takes every interior handle unconditionally (only ever
mutating exclusively-owned nodes), and a 10k-level aliased chain plus
a shared-subterm-survives test pin it. Also fenced the term arena at
2^31 nodes, where a node index would alias the env tag bit (the old
u32 index wrapped at 2^32 with no guard at all), and repaired the
stale docs the recheck flagged (README snippet imports, three
pre-rename API mentions, the example's step count).

Co-Authored-By: Claude Fable 5 <noreply@anthropic.com>

The workflow recheck converged three lenses on one defect the clamp
commit created: --rescue past 67,108,863 silently lost its transition
multiplier to the 2^31-1 ceiling — exactly the knob AGENTS.md says to
raise before n=42 — while describe() stamped the multiplier that never
ran. Machine::MAX_TRANS now names the ceiling, args::check_rescue
refuses configs whose product exceeds it (all three ladder drivers, at
exit 2, naming the largest usable --rescue), and the rescue_trans_mult
field doc carries the constraint. Census provenance gains the
'# memo-in:' fingerprint — reproduced: two runs whose escal columns
differ by 1,800 terms stamped byte-identical headers, while the
checkpoint header had fingerprinted the memo all along. solomonoff
stamps the same three-line provenance census does, and --dump-max-x
without --table is a refusal instead of a silently inert flag. The
LVL_TAG and clamp comments now name the quantities actually protected
(node indices and depth, not env indices). Five rustdoc
private-intra-doc links introduced by the sweep are repaired — CI's
hard doc gate failed at the previous HEAD, which would have blocked
the armed release. Term documents its Drop/E0509 consequence;
certificate::search gets its docs.rs feature badge.

Co-Authored-By: Claude Fable 5 <noreply@anthropic.com>

The per-push 2^31 assert measured +4% census user time for a check
whose only consumer is the machine's env-cell tag — and every node
index the machine stores comes from the one pool it was handed. One
assert per normalize run fences the same aliasing exactly, at one
compare per term instead of one per node: census 33..36 back to
64.7 s user from 66.5, bit-identical rows. The # Panics contract now
lives on normalize_capped, where the fence actually is.

Co-Authored-By: Claude Fable 5 <noreply@anthropic.com>

Co-Authored-By: Claude Fable 5 <noreply@anthropic.com>

146 signature universes at sizes 4..=32 plus the top twelve permutations
to 34 (9,276 core-seconds), run as plain `blam q census --sig` sweeps so
the campaign is regenerable without a driver.

The frozen order `h meas new cnot t` is the maximum of the 120
permutations at every depth measured; the S1 tie with its h<->t mirror,
broken lexicographically in 2026-08-02, now breaks by measurement at
N=28 and holds strict through 34. Harness validated against the
canonical census table (rows 4..32 bit-identical) and against the S1
pilot's Omega_success(<=24) = 46757/2^24.

Two structural findings. The set axis has exactly one point: the
canonical five is the unique minimal complete signature over the
eight-gate alphabet, and s/x/z are lambda-definable over it. And
Omega_success is blind to the non-Clifford resource -- a Clifford-only,
non-universal signature scores the frozen five's exact tuple and every
leaf count -- so the predeclared functional ranks orders, never sets.

Retires the S1 prediction that the h<->t mirror ties break at larger N:
they first break at n=27, which places the shortest
superposition-plus-verdict-split program at 27 bits, the dyadic-mass
precursor of the 53-bit P53.

Co-Authored-By: Claude Opus 5 <noreply@anthropic.com>

…ling

P27, the 27-bit mirror-break witness, is
000000010110011110011101010 = \a.\b.\c. c (a (b c)) c. Exhaustive batch
re-adjudication of all 47,146 closed 27-bit programs under the mirror
pair finds exactly one mass difference and zero leaf-count differences,
and `blam q run` confirms the leaves: Err(Species) and Halt(live=0) at
1/2 each under h, mass 1 and 0 under t. The split is Halt/Err, closing
the question STATUS left open.

Odd-sector: W=30 (the docketed probe), W=32 and W=33 measured; stage-1a
acceptance is still zero at weight 33. W=33 is the tallest completable
run -- W=34 aborts at intermediate weight 30, whose slice is 5.7x the
same weight's own-run size. The standing "stop near W=33" projection was
read off the top-weight series, which is not the series that binds; the
ladder to 44 needs pruning that bites mid-ladder.

Co-Authored-By: Claude Opus 5 <noreply@anthropic.com>

--capout-telemetry FILE streams the rung-3 stratification input
(reason/steps/high-water per capout program); --residuals FILE writes
the manifest's residual-Unknown provenance rows (src bits, residual
bits, sha256 of the residual wire string, via a rung-1 rerun since
Transfer is Copy). Both sorted by program bits; prefix-freeness makes
full-line byte-lex equal bits order. The stdout verdict stream — whose
bits-sorted digest is canonical — is byte-identical with flags off or
on, and the flag-off sweep takes no new locks.

Co-Authored-By: Claude Fable 5 <noreply@anthropic.com>

The full spec §8.1 surface: trusted verifier (verify_pdr — OPEN/
UNWRAP/DROP/SEED via check_reduces plus the v1.2 INIT landing, same
shape gates as v3 extended to P), untrusted discovery (try_pdr reads
P off the OPEN trace's opaque-head endpoint, fourth rung of try_kill),
CLI arms (PDR search tag + summary column, cert lean PdrCert emission,
Blc.Passenger import in generated headers), and the Lean assembly
(lean/Blc/Passenger.lean: rank step 3kU+kD, diagonal descent 2kU per
level, non-uniform leftCost with the n=0 cycle closing by SEED at
Q := X0 P0). Nothing new in the trusted Lean layer — no renameMVar01
analog; env2 and constant environments cover all four obligations.

The 36-bit forcing exemplar certifies end to end with
kO=kU=kD=kS=1 (measured core-cycle gaps 2n+4, matching the assembly
formula), init lands with three trailing args, and v1/HTR/selector
all reject it. Soundness battery: zero fires across all 196,848
provable halters <=28 bits through the now-four-rung sweep. Assembly
adversarially reviewed by Codex (blc-conformance thread): survives,
all instantiation and lifting steps confirmed against the existing
lemma inventory.

Co-Authored-By: Claude Fable 5 <noreply@anthropic.com>

Escalation docket item 2, per the settled recording protocol
(quantum/escalation.md): data/quantum/skeleton_manifest.txt carries
checker+engine commit, the frozen signature, tier-1 caps, the residual
ladder config, sorted-input and sorted-verdict digests (both reproduce
the pinned values byte-identically under LC_ALL=C sort), per-size
verdict counts, the Div provenance split re-pinned from the driver's
own stream (58,373 oracle / 45,028 bb — closing the loop on Codex's
independent recount), exact masses under leaf-mass accounting
(killed 27,958,835/2^41; remaining 9,594,947/2^41; upper
6,857,971,973/2^41), all 37 residual-Unknown provenance rows with
residual SHA-256 identities and classical-frontier source membership
(28/37), and the exact regeneration commands. tools/skel_manifest.py
is the deterministic builder; the leaf-mass subtlety (killed programs
are single-branch, survivors carry resolved mass) is documented in
the tool and printed as a cross-check line. tools/capout_strata.py is
the docket-1 stratification analyzer.

Co-Authored-By: Claude Fable 5 <noreply@anthropic.com>

…en command

Codex's lockstep round (qblc-divergence) agreed on every number and
digest but caught a label conflation: the bracket's unresolved term is
Unknown + Capacity, and the census carries exactly one Capacity leaf
(qubit cap, 1/2^41). The manifest now reports the split — raw Unknown
37,553,781/2^41, Capacity 1/2^41, remaining Unknown 9,594,946/2^41,
remaining unresolved 9,594,947/2^41 — keeps the bracket upper
unchanged, and stops attributing the survivor program-mass excess
(7/2^41 over Unknown, 6/2^41 over unresolved), which would need
per-program tracking. Generator now enforces the set discipline the
artifacts happened to satisfy (no duplicate bits, identical bit sets)
and records the fully executable regeneration command.

Co-Authored-By: Claude Fable 5 <noreply@anthropic.com>

…docs

The first complete four-rung frontier sweep since the v2 reshape
(981.3 s wall / 6,630 s user, --threads 8) found eight
PassengerDiagonalRatchet kills — 36/38/39/40x4/41 bits, all the spec
§8.1 exemplar's 26-bit head family. Full new-kill protocol: recert at
4x budgets reproduces all 305 kills byte-identically; cert lean +
lake build Certs kernel-checks all 305 theorems (eight new PdrCert);
census regen fate-invariant on every row 4..41 with the subtraction
identity 4,532 = 4,227 + 305; solomonoff regen mass-invariant; exact
Omega trim 53/2^41 -> upper 0.124105092895. Frontier is 4,227.

Canonical census/solomonoff/unknowns now carry the provenance format
in-tree (the deferred release-regen item), AGENTS records the
measured sweep time in place of the estimate, STATUS closes
escalation docket 1+2 and classical docket 1 with tonight's
measurements, spec §8.1 is marked implemented, and the ledger carries
the overnight session.

Co-Authored-By: Claude Fable 5 <noreply@anthropic.com>

Co-Authored-By: Claude Fable 5 <noreply@anthropic.com>