Dev - #4

qeval grows run_traced (per-leaf root-to-leaf Effect paths: New/H/T/Cnot
with qubit+epoch, Meas with outcome; beta-stuttering erased by
construction). New bin qselfint: quote + check harness, full 4..=24
population — quantum effect-trace 19,014 verified / 34 unresolved skips /
0 mismatches (independent qvm endpoint cross-check per run), pure-NF
19,014/34/0, witness45 reproduced, poisoned-seed-env canary. Five pinned
tests. DESIGN-QBLC obligation 2 records the measured constant: tight
within the intL protocol, optimality open, bisimulation stays the proof.

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

…ly n=53

New bin qradical: lambda^5-idiom slice ({h,meas,new,t} all-mentioned
filter, count cross-checked exactly against Codex's independent DP at 53),
exact Z[omega] per-size aggregation with sqrt2-coefficient extraction,
per-program mass-conservation assert, FATEDIV accounting (per-program
Sigma-halt-mass irrationality), optional [beta] [trans] args.
enumerate.rs grows split_tasks_at (seeded-root task splitting; the
lambda^5 slice runs under a fixed 10-bit prefix) + coverage test.
qvm pins P53 = first_fate_divergent_nondyadic_witness_at_53.

Measured 46..53: per-size sqrt2-coefficients exactly 0 through 52, then
-1/4 at 53 — fatediv = 1, the unique program bit-exactly P53; unknowns
at 53 (752) are beta-insensitive at 8x/64x budgets.

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

… next

Three ledger entries for the day: E_q = intL I (176 bits) measured and
effect-trace verified; the swap-involution broken by Codex's P53; the
radical-aggregate census landing the idiom-sector threshold at exactly
n=53 with P53 the sole fate-divergent survivor. AGENTS docket updated:
phase-2 primitive-taint over the non-lambda^5 complement is the single
remaining blocker on the full-population claim.

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

Spec form of qBLC proof obligation 2 (Codex skeleton, rounds 2-3 on
thread qblc-selfint). World-indexed generated relation R_k with runtime
diagonals and the full synchronized frame grammar; binary Meas
transitions; divergence-sensitive clauses; case ledger with C-DESCEND
as the opening rule; L1 extensional over implementing closures (the VAR
closure carries a dead wire suffix); pair vs cons' separated; L3 as a
full weak-head/ArgView decomposition; L4 readback collapse closing the
gap to the measured bit-exact pure-NF identity; base theorem
signature-free with a compatibility rule so the pure-NF corollary
actually follows. All obligations open; measured evidence indexed.
Round-3 ratification conditional on six corrections, all incorporated.

AGENTS docket: pickup order recorded (bisim L1/L2 proof lane first,
then phase-2 taint; complete taint design in thread qblc-omega-
witnesses round 2).

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

…e protocols

By-type layout picked by a9: docs/ takes DESIGN-BLC, DESIGN-QBLC,
SPEC-BISIM, LEDGER (names unchanged); data/ takes the canonical
outputs with the 41-bound suffix dropped (range lives in-file and in
AGENTS; n=42 regenerates in place with zero path churn); scripts/
encodes the standing protocols (spot-check, census-regen with kill
subtraction + identity check, recert-kills at 4x + certlean + lake,
solomonoff-regen) — CI's spot-check job now calls the script.
Sub-labs under tools/ deliberately intact; src/ left flat (module
regroup = public-API break on the published crate). Ledger entries
before 2026-08-04 keep historical paths. Verified: fmt, clippy -D,
cargo test --release (17/17 green), spot-check 4..32 bit-identical,
recert smoke 25/25 byte-identical, regen smoke reproduces the
canonical frontier slice exactly, lake build Certs green.

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

README picks up the two newest qBLC headlines (E_q = intL I = 176
bits; idiom-sector dyadicity threshold at exactly n=53) and a
current-only roadmap. DESIGN-QBLC's header no longer says S1 is
cleared to build (S1-S3 core landed) and the irrationality open
question records the measured n=53 layer plus the phase-2 route.
DESIGN-BLC drops the crate-name question resolved by publishing as
blam. AGENTS: qBLC docket compressed from staging narrative to
current-state form (engines / measured state / next), live state
dated 2026-08-04, spot-check bullet points at the script, gaslamp
thread list completed. Ledger entry extended; historical entries
untouched.

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

Arms release.yml to publish on the next main merge.

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

Install -> library tour -> drivers -> verification, with the results
list collapsed into one Selected-results paragraph pointing at docs/
and data/ via absolute links (the crate tarball ships neither). The
two new usage snippets are committed as runnable examples
(examples/normalize.rs, examples/bell.rs — the Bell program is 41
bits, the census's entanglement threshold, amplitudes exact) so the
CI clippy/test bar keeps the README code honest.

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

Dev

Bumps [actions/checkout](https://github.com/actions/checkout) from 6 to 7.
- [Release notes](https://github.com/actions/checkout/releases)
- [Changelog](https://github.com/actions/checkout/blob/main/CHANGELOG.md)
- [Commits](actions/checkout@v6...v7)

---
updated-dependencies:
- dependency-name: actions/checkout
  dependency-version: '7'
  dependency-type: direct:production
  update-type: version-update:semver-major
...

Signed-off-by: dependabot[bot] <support@github.com>

…eckout-7

ci: bump actions/checkout from 6 to 7

…che-6

ci: bump actions/cache from 4 to 6

Exact (loud-overflow Dw accumulator), radical_parts, is_dyadic, and
show_parts move from qradical's bin-local defs to blam::radical, plus
a new sqrt2_part re-embedding the √2 coefficient of a real mass as a
rational ring element — phase 2 (qcomplement) accumulates threshold
coefficients on their own overflow-independent track. Pure move for
qradical; behavior unchanged.

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

The non-λ⁵ complement instrument (thread qblc-omega-witnesses rounds
2-3): rung-0 syntactic filter (leading-λ count from leading zeros;
consumed-required mention masks, sound by the provenance lemma; counts
double-validated against Codex's independent inclusion-exclusion DP at
n=46 bit-exactly), hunt-budget sweep with uncapped unresolved
streaming, and a separate adjudicate mode — the two-pass composition
is unit-tested against a straight canonical sweep. The threshold
deliverable (per-size √2-coefficient of Σ_success) rides its own
overflow-independent accumulator; rejects contribute exactly 0 to it,
so it is sector-complete even though the rational subtotal is
survivors-only.

Validation: complement 42..45 (5.65B programs, 264.9s) reproduces the
exhaustive hunt's ground truth — √2-coefficient exactly 0 at every
size, zero fate-divergent programs (witness45 is idiom-sector, k≥5,
correctly invisible here).

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

Kernel-proved: wire_intL (the 170-bit int.lam transcription pinned by
decide — the certlean wire-identity pattern applied to the interpreter
itself), |E_q = intL I| = 176, and the quote-linearity size identity
|stream(M,R)| = 14|p| + zeros(p) + |R| (closed tails). Stated as open
obligations (Codex round-4 ratification, thread qblc-selfint): the
extensional translation contract Implements (head reduction is exactly
right there), and the strategy-faithful parser targets — ParserResult
exposes the residual tail U (the r4 counterexample kills a naive
'C Q R' under head reduction: int.lam's VAR branch passes
cont list1 (skipvar list1), and headStep never enters argument
position), with the continuation quantified inside. L2 is the VAR
engine, ParserStatement the induction motor, closed L1 the corollary.
Over pure Term this is the β-non-forcing theorem; the effectful
poisoned-seed lifting stays a later obligation.

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

Codex hand-compilation closed the §8 lane's first rung: no
two-entry/single-knot family reaches ≤175; intL I and its root-fused
spelling tie at 176 with identical (L,A,X). DESIGN-QBLC obligation-2
text updated; .phase2/ (the complement-run working dir) ignored.

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

Optional 'i/m' slice spec runs every m-th interleaved task: a
disjoint exact cover of the enumeration, so n=52/53 partition into
independent runs under the ≤1-2h-per-run protocol; slice tallies
merge by exact addition (unit-tested against the full sweep,
including the exact accumulators).

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

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

…176 rung closed

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

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

AGENTS: complement √2 ≡ 0 measured through 47; remaining blocks
chunked; next-session pickup order set (a9's pick: the G_k / Object B
lane — output-convention spar, exact sandwich constants, first
G_1/G_2 approximant runs), with the parked threads listed. SPEC-BISIM
§7: the Lean seed recorded (ParserResult residual-tail form and why;
proof order per r4). DESIGN-QBLC: phase-2 status un-staled (taint
design superseded by the ratified two-pass instrument; measured
through 47). README: complement-through-47 and the two-entry
176-minimality, one breath each.

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

Complement 48/49: √2 ≡ 0 exactly at both, fatediv 0 — dyadicity
measured through 49; first complement nondyadic pair (K-plumbed
H·T·H·meas sandwiches, σ-paired, decoded) and first unkT (2 at 49).

Theorem lane (Codex rounds r1-r3, qblc-omega-witnesses): Tier-A
accounting identity sharpened; T1 finite-trace Galois twist ratified
(paired configurations, semantic Z, Δ(C) for limits); P53 =
witness45 + 8-bit split verified; n_{1/3} ≤ 85 measured through
qeval; oddmin stage-1a design frozen (open transducers, trusted
constructor-closure certificate).

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

Per-qubit may-set S ⊆ {X,Y,Z}×{even,odd} replayed over qeval effect
traces: H swaps X↔Z, T feeds X/Y both ways grade-flipped, meas
accepts on (Z,odd) and resets; cnot latches conservative accept
pending stage 1b. Sound by the product-structure argument (any
Galois-odd leaf mass forces an odd Born factor). Tests: sandwich
accepted, seven dyadic hand-paths quiet, all four witnesses' odd
leaves accepted on real traces, exhaustive ≤22 sweep tight (6,069
programs, zero accepts) in 0.01s.

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

The parked irrationality-strata note, upgraded: the finite-trace
Galois identity with its configuration-paired proof, Δ(C) for
limits, the measured threshold table (45/48/49/51/53/85), the
r3-frozen oddmin architecture, and the informal why-the-pattern-held
summary.

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

Three new σ-paired witnesses (two payload extensions of the 48
K-frame, one λ⁴ re-plumb discarding cnot), all verified (2±√2)/4
by qeval replay and added to the odd.rs fixture. Dyadicity now
measured through 50; unkT 10, cap 41k noted for adjudication.

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

Codex r4 rejected the all-trace DP: cnot becomes OutOfScope (verdict
enum Even/MayOdd/NeedsCnot), Call edges must be ordered, prototype
gated on measured summary growth. src/odd.rs rewritten to build-step
1 with certificate-grade trace validation (epoch tracking, retire on
meas, forged-trace rejection) and pure step kernels. 28-bit cnot
witness constructed and verified; ledger + docket updated.

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

…lemma

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

…uage-DFAs

Ports for higher-order values (the λx.x vs λx.HD;x merge was unsound),
capability-action protocol, five-way heads, structural canonicalization,
accept strictly by external product. Gate-zero adversarial checks added.

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

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

…ton, accept product

17-mask automaton (independently cross-derived), bisimulation-quotient
canonicalization that preserves ports, external accept product per
SPEC-ODDMIN §3. Transfers and gate-zero checks are the next brick.

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

…lings

BindId specialization product replaces edge-index binding; CallTarget
ends the bare-Call(1) trap; full CapRel on both interface directions;
EvalHead/Apply/NF-descent protocol. Foundation repairs: root-role
assert, may_accept_latent rename with scope docs. Spec §4 rewritten;
gate-zero grows to nine checks.

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

…sses

√2 ≡ 0 exact at 51, fatediv 0 — full-population dyadicity through 51.
The pre-registered call (wrapped witness45 ⇒ nondyadic ≥ 4, fatediv 0)
confirmed with 24 σ-paired leaves across 12 programs: both predicted
wires byte-exact, plus the id/eta wrappers at interior λ-depths, two
K-plumbs, and one (1 1)-argument echo of P53. All 12 wires
replay-verified in the odd.rs fixture.

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

…ain revisions

The reference DP is live and gate-green: var/lam/app transfers over
the r5b schema, continuation-specialized composition with closure-env
restriction, one-shot closed evaluation, and the oddminproto growth
driver. witness45 composes to 44 nodes and accepts; cnot28 rejects;
exact vs qeval on all 6,069 closed programs ≤22 (zero looseness, nine
Ω-family ⊤ cells); 96/751/6,346 summaries at W=16/20/24 under the §8
stop rule. The letter-enumerated observation fan, maximal call-stack
erasure, unrestricted captured envs, and staged signature application
were each measured fatal and replaced (SPEC-ODDMIN §9, pending r6
ratification). Open: component-scoped Top widening for Ω.

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

…ands, zero splice-top

Codex reran cdd4610 and ratified the star fan, ctx frames, epsilon,
and one-shot closed evaluation. Amendments landed: must-bound freeness
dataflow (bound-anywhere was unsound per the dominance ruling), the
quarantined materialized_accept_any_root rename, the measured
closed-resolution invariant (Abort::UnresolvedAmbient with
continuation-chain liveness), and the narrow-rung pure-component
widening (Head::PureWiden, capture-depth gated, purity-checked) —
zero splice-top through W=24, driver at 1.1s. The new assertion
exposed a latent formal-renumbering bug (Call{Formal} targets kept
old side-local indices across flatten; fixed via PreLabel::CallF).
Remaining top cells: 19 nested-descent formal-identity cases <=22,
all concretely non-odd — the alpha-only port-identity canon loss
heading the stage-2 queue.

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

…ers to r6

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