Bk19xsa/aqida-certified-cell-ladder

Certified-Cell Ladder — trained cells, fixed schedule, closed certification bridge

A learned 8-bit-limb ALU beneath a fixed double-and-add / restoring-division schedule, computing (a * b) mod p exactly for primes to 2^2048 and operands to 4096 bits. The claim is the learned cells and their certified transitions, not discovery of the loop.

Results (official open-source scorer, full 1100-problem battery)

property	result
Tiers cleared	1–10 (highest_tier_above_90 = 10), overall 1.00 — every tier 100/100 (Tier 0 included)
Wall-clock	247.8 s against the 300 s budget (RTX 4060 laptop GPU)
Determinism	deterministic: true (harness check)
Weight randomization	every tier collapses to 0.00 (receipts/ablation_random_cells.json)
Weights	cells.pt md5 ae6c9fbd1dbf8e769ad8bb5e4e2f63cd (~4.5 MB, ~0.5M params)

Receipts: receipts/official_eval_1100.json (seed cafe2026), receipts/ablation_random_cells.json.

Architecture

Six tiny MLP cells — PG (carry propagate/generate), SCAN (prefix combine), FIN (sum finalize), NOT, BITS (bit decompose), SHL1 (shift) — each trained from random initialization and then exhaustively certified exact over its full finite input space (e.g. all 65,536 limb pairs for PG). A fixed schedule composes them: binary restoring reduction of each operand, then double-and-add over the multiplier bits, all on 8-bit limbs.

• The schedule's loop bounds key only on input bit-lengths; the identical op sequence executes for every input — no control-flow feedback from cell outputs. The conditional subtraction is data-flow selection (torch.where) over the trained borrow bit, in fixed wiring.
• load() memoizes each cell's argmax truth table over its full input space from the trained weights; inference gathers from those tables. They are indexed by internal 8-bit states, never by evaluation inputs; randomizing the weights randomizes the tables (see ablation).
• Schedule routing of the dynamic-width kind, disclosed: operands whose bit-length already proves them < p skip the (no-op) reduction pass and run at prime width. Exactness preserved by construction.
• Executes on GPU when available; identical integer semantics on CPU (slower than budget on our CPU — the receipts above are GPU runs).

The certification bridge — closed

Where comparable fixed-loop entries prove the integer algorithm and leave "the cell-to-step bridge connecting the trained weights to the proven step" open, this artifact closes that bridge by exhaustive enumeration: every single step the schedule ever executes is one of the six cells applied inside its certified-exact input space, so the composed pipeline is exact by fixed wiring — the empirical realization of a finite-certificate length-generalization theorem (machine-checked corpus: AQiDA Lean Files 26/28 — ZMod phase representation, binExp depth = bit length, dilation laws; per-cell certification logs in provenance.json).

Compliance disclosure (read before judging)

Stated plainly rather than obscured: the double-and-add and restoring-division schedule is fixed control flow authored by hand — the same shape as other current fixed-loop entries in the contributor network. The rules permit "a loop that feeds the model its input tokens one at a time … so long as the encoder receives no feedback from the model" and do not prohibit recurrent models as such, while prohibiting "by-construction arithmetic algorithms"; where this class falls is an open organizer ruling at the time of packaging. This entry is submitted transparently for that class-wide review and is not represented as guaranteed-compliant. Static-scan clean (no sympy/gmpy2, no int*int%int, no eval/exec/network/subprocess); per-argument preprocessing only; Tier-0 pure-multiplication cases are answered exactly by the same pipeline (reduction passes are provable no-ops there).

Reproduce

# from the challenge repo (github.com/SAIRcompetition/modular-arithmetic-challenge):
PYTHONPATH=src python -m modchallenge.cli evaluate <this-dir> --total 1100

Expected: overall 1.00, key 10, all tiers complete, under budget on a CUDA-capable machine.