t27.aiРусский

Blocked is not failed

You will learn

Why a rule checked while compiling stops a spec before any test runs, and how that differs from a failing test.

In the browser, setting MAX_TRITS to 3 made two checks fail. The native t27c is stricter: the 8 invariants of golden_sieve.t27 are proved while it compiles, so with a third trit the spec does not compile at all. The report says BLOCKED, and explains that a blocked spec never produced a binary, so it has no test results to count. A rule checked while compiling cannot ship broken. Then the recording plants a different bug: the rule against shift-register cells now always says yes, and exactly one test fails, the one that checks the formula. Every byte in the recording was printed by the command; only the typing is staged.

Try it

Find the line that says why a blocked spec has no test results, and the test the second bug breaks.

Open the interactive lesson →

t27c on golden_sieve.t27 -- the ternary sieve, native
t27c on golden_sieve.t27 -- the ternary sieve, native ↗

t27c on the t27c lab (Railway), spec at t27 5ff0ec512: 3 tests pass natively; allowing a third trit trips a compile-time invariant and blocks the spec; letting S5 admit shift registers fails exactly one test; git restores the spec.

specs/numeric/golden_sieve.t27

// SPDX-License-Identifier: Apache-2.0
// golden_sieve.t27 0 The Golden Sieve -- which weight alphabets a ternary
// datapath may use, derived from measured theorems rather than chosen.
//
// Five predicates. A candidate alphabet is admissible only if it satisfies all
// five. Each cites the measurement that established it; none is an opinion.
//
// S1 PACKING    |A| = 3^k          T367  only powers of three waste no trits
// S2 CEILING    k <= 2             T369  27 levels measured +0.15 / -0.13 pp,
// neither significant on two tasks
// S3 INTEGRAL   A subset of Z      T293  a two-lane Z[b] resolve costs
// 8 DSP48E1 or ~2750 LUT
// S4 TRIT_FANIN fanin * bits <= 6  T368b 2.00 LUT/neuron at <= 6 bits,
// 39-54 LUT at 12 -- BUT SEE T454: those
// are PER-NEURON figures on a different
// structure. Measured post-route on a
// LAYER of 16 neurons the ratio is 3.75x
// (4.12 vs 15.44 LUT/neuron), not 20-27x.
// S4 is a stated trade, not a law.
// NOT OURS: LogicNets
// (arXiv:2004.03021) states the cost model
// in 2020, and its own NID configs run at
// 14 input bits -- so 6 is OUR choice,
// not a law (T419).
// S5 PRIMITIVE  no DSP48E1/SRL16E  T246, T342  openXC7 emits a wrong bitstream
// for both while every tool reports OK
//
// THE ONE FORMULA the sieve leaves:
//
// TNF(k, b) = {0} u { +- b^i : 0 <= i < (3^k - 1)/2 },  k in {1,2}, b in Z, b >= 2
//
// k = 1 -> 3 levels, ONE trit,  {0, +-1}
// k = 2 -> 9 levels, TWO trits, {0, +-b^0, +-b^1, +-b^2, +-b^3}
//
// And the 27-entry matrix is what a NEURON is, not what a weight is: three
// ternary inputs give 3^3 = 27 reachable rows with zero waste, against a binary
// LUT6's 64 rows of which 27 are reachable -- 42 percent used.
//
// phi^2 + phi^-2 = 3 | TRINITY

module numeric-golden-sieve;

// ============================================================================
// Constants -- the thresholds, each traceable to a measurement
// ============================================================================

// S2: the Nine-Rung ceiling. Two trits, nine levels. T288 measured no
// significant step above nine on any of eight tasks; T369 measured the third
// trit at +0.15 pp (UNSW, ns) and -0.13 pp (Fashion, ns).
pub const MAX_TRITS : u32 = 2;

// S4: a neuron of at most this many INPUT BITS costs 2.00 LUT; above it, 39-54.
// A ternary symbol occupies two bits, so a hidden layer's fan-in is three.
pub const MAX_NEURON_BITS : u32 = 6;

// The radix. Everything in the sieve is counted in trits, not bits.
pub const RADIX : u32 = 3;

// Bits a ternary symbol occupies on a binary substrate. The 58 percent of every
// LUT lost to unreachable codes follows from this and from MAX_NEURON_BITS.
pub const TERNARY_SYMBOL_BITS : u32 = 2;

// The four alphabet sizes the sieve ever has to reason about, written out
// rather than computed: the language's numeric core is loop-free, and a table
// of four constants is clearer than a recursion that only ever runs to three.
pub const LEVELS_0_TRITS : u32 = 1;
pub const LEVELS_1_TRIT  : u32 = 3;
pub const LEVELS_2_TRITS : u32 = 9;
pub const LEVELS_3_TRITS : u32 = 27;

// ============================================================================
// S1 -- PACKING. |A| must be a power of three.
// ============================================================================

// Levels representable in `t` trits: 3^t, for the range the sieve needs.
pub fn levels_in_trits(t : u32) -> u32 {
    if (t == 0) { return LEVELS_0_TRITS; }
    if (t == 1) { return LEVELS_1_TRIT; }
    if (t == 2) { return LEVELS_2_TRITS; }
    if (t == 3) { return LEVELS_3_TRITS; }
    return 0;
}

// The trit count that holds `n` levels exactly, or 0 when n is not a power of
// three. Returning 0 for "does not pack" is what makes S1 a predicate rather
// than a rounding.
pub fn trits_for_levels(n : u32) -> u32 {
    if (n == LEVELS_1_TRIT) { return 1; }
    if (n == LEVELS_2_TRITS) { return 2; }
    if (n == LEVELS_3_TRITS) { return 3; }
    return 0;
}

pub fn s1_packing(n : u32) -> bool {
    return trits_for_levels(n) > 0;
}

// ============================================================================
// S2 -- CEILING. At most two trits.
// ============================================================================

pub fn s2_ceiling(n : u32) -> bool {
    let t : u32 = trits_for_levels(n);
    if (t == 0) { return false; }
    return t <= MAX_TRITS;
}

// ============================================================================
// S3 -- SINGLE LANE. The alphabet must be COMMENSURABLE: every ratio of two
// nonzero elements rational, so one accumulator lane suffices.
//
// An irrational base b forces the pair representation a + b*c, and resolving
// that pair against a threshold costs 8 DSP48E1 or about 2750 LUT without them
// (T293). The multiplier phi removes from weight application returns here.
//
// W778 REPAIR. This filter used to read `lanes == 1` with `lanes` handed in by
// the caller. That is not a predicate on the alphabet, it is the answer typed in
// by hand -- and typed by the wrong hand it kills our own format. {-phi, 0,
// +phi} LOOKS irrational, but phi there is a COMMON POSITIVE SCALE and factors
// straight out (T207): the alphabet is phi*{-1,0,+1} and rides one lane. Two
// lanes are forced only when powers of the base are MIXED, as in {0,+-1,+-phi},
// where 1 and phi cannot share an accumulator.
//
// For the ladder family the sieve ranges over -- A = {0} u {+-b^i : i < n} --
// commensurability is decidable from two facts, and both are stated rather than
// computed, because the numeric core has no reals:
//
//   n_magnitudes  how many distinct |a| the alphabet has
//   base_rational whether b is a ratio of integers
//
// One magnitude is always single-lane whatever the base is; more than one is
// single-lane exactly when the base is rational. Running this over the
// 16-candidate top reproduced every verdict the hand-supplied version gave --
// the repair changed no answer, it removed the opportunity for one to be wrong.
// ============================================================================

pub fn s3_single_lane(n_magnitudes : u32, base_rational : bool) -> bool {
    if (n_magnitudes <= 1) { return true; }
    return base_rational;
}

// The lane count that follows, kept so callers that reason in lanes still can.
pub fn lanes_needed(n_magnitudes : u32, base_rational : bool) -> u32 {
    if (s3_single_lane(n_magnitudes, base_rational)) { return 1; }
    return 2;
}

// ============================================================================
// S4 -- TRIT_FANIN. A neuron reads at most six input bits.
// ============================================================================

pub fn neuron_bits(fanin : u32, input_bits : u32) -> u32 {
    return fanin * input_bits;
}

pub fn s4_trit_fanin(fanin : u32, input_bits : u32) -> bool {
    return neuron_bits(fanin, input_bits) <= MAX_NEURON_BITS;
}

// The fan-in the rule permits for a given input encoding. Binary inputs give
// six; ternary symbols are two bits each and give three.
pub fn max_fanin(input_bits : u32) -> u32 {
    if (input_bits == 0) { return 0; }
    return MAX_NEURON_BITS / input_bits;
}

// ============================================================================
// S5 -- PRIMITIVE. No DSP48E1 and no SRL16E in the emitted netlist.
// ============================================================================

pub fn s5_primitive(dsp_count : u32, srl_count : u32) -> bool {
    if (dsp_count > 0) { return false; }
    return srl_count == 0;
}

// ============================================================================
// The sieve -- all five, and the substrate waste that follows
// ============================================================================

pub fn admissible(levels : u32, n_magnitudes : u32, base_rational : bool,
                  fanin : u32, input_bits : u32,
                  dsp_count : u32, srl_count : u32) -> bool {
    if (s1_packing(levels) == false) { return false; }
    if (s2_ceiling(levels) == false) { return false; }
    if (s3_single_lane(n_magnitudes, base_rational) == false) { return false; }
    if (s4_trit_fanin(fanin, input_bits) == false) { return false; }
    if (s5_primitive(dsp_count, srl_count) == false) { return false; }
    return true;
}

// Rows a ternary neuron of `fanin` ternary inputs actually needs: 3^fanin.
pub fn ternary_rows(fanin : u32) -> u32 {
    return levels_in_trits(fanin);
}

// Rows the binary LUT holding it provides: 2^(fanin * TERNARY_SYMBOL_BITS).
// Written out for the range that matters, as with levels_in_trits.
pub fn binary_rows(fanin : u32) -> u32 {
    if (fanin == 1) { return 4; }
    if (fanin == 2) { return 16; }
    if (fanin == 3) { return 64; }
    return 0;
}

// ============================================================================
// S6 -- NON-DOMINANCE. W778. The filter the other five could not see, and the
// one that refutes this file's own formula.
//
// PRIOR ART, W779, and it is older than the filter. A neuron whose output depends
// on one input is a 1-JUNTA, or a DICTATOR; the neuron is a LINEAR THRESHOLD
// FUNCTION (O'Donnell, Analysis of Boolean Functions). The collapse itself is the
// CRITICAL-INDEX / HEAD-TAIL DECOMPOSITION of LTFs -- Servedio, Computational
// Complexity 2007, arXiv:0902.3757 -- and the superincreasing-implies-
// lexicographic fact is formalised in Gupte, arXiv:1503.03742. The tribonacci
// constant is OEIS A058265 by definition. NOTHING in S6's mathematics is new
// (T423); what is ours is the measured attribution of low junta degree to the
// WEIGHT ALPHABET, and the consequence that TNF(k,b) has no admissible k=2
// member over Z.
//
// The metric below is JUNTA DEGREE, not "effective fan-in": that term is taken
// by ODIN (arXiv:1804.07858) for accumulator depth (T424a).
//
// The field already prices functional rather than structural input count --
// Logic Shrinkage (FPGA'22 / TRETS 2023, 10.1145/3583075) learns per-LUT input
// counts by removing low-importance inputs, for 1.54x area (T424b).
//
// At fan-in 3 (which S4 fixes) a neuron reads three weights. If ONE of them
// exceeds the sum of the others, no combination of the other two can outvote it
// and the neuron's output is a function of that ONE input. It is not constant --
// it passes every liveness check -- it simply is not a neuron.
//
// Enumerated over all 9^3 = 729 weight triples each nine-level alphabet admits,
// MEAN EFFECTIVE FAN-IN (how many inputs the output actually depends on):
//
//   alphabet                        top : rest   junta degree   full (3 of 3)
//   linear  {0,+-1,+-2,+-3,+-4}      4 <  6          2.55          66.9%
//   fib     {0,+-1,+-1,+-2,+-3}      3 <  4          2.52          63.6%
//   ladder b=2                       8 >  7          2.19          52.7%
//   ladder b=3                      27 > 13          1.49          21.9%
//   ladder b=4                      64 > 21          1.03           8.8%
//
// A base-4 neuron is, on average, a function of ONE input.
//
// THE EXACT BOUNDARY. For the ladder {b^0..b^3} the top weight exceeds the sum
// of the other three exactly when b^3 > b^2 + b + 1, whose root is the
// TRIBONACCI CONSTANT 1.8392867552. S3 demands b in Z and b >= 2. Therefore:
//
//   NO INTEGER BASE ADMITS A NINE-LEVEL LADDER FREE OF WEIGHT DOMINATION.
//
// The one formula this file states -- TNF(k,b) = {0} u {+-b^i}, k in {1,2},
// b in Z, b >= 2 -- has no member at k=2 that clears S6. The formula is widened
// below: the ladder was never the requirement, integrality was.
//
// WHAT THIS CORRECTS. T366a and T398 read base 3 as CHEAPER in table layers
// (1.05 LUT/neuron against dyadic's 1.92) and called it compression. Measured
// across six alphabets on a stand where every neuron is rejection-sampled live,
// effective fan-in predicts LUT at r = +0.991. Base 3 is cheaper because it
// COMPUTES LESS. `prefers_base(b, LAYER_TABLE) = b >= 3` was preferring
// degeneracy, and is withdrawn below.
//
// SCOPE, AND THE DIRECTION IS NOT WHAT IT LOOKS LIKE (T412). Measured on the
// sparse fan-in-3 stand where the mechanism can act, 8 seeds, both tasks:
//
//   junta degree vs accuracy   UNSW  r = -0.971   Fashion  r = +0.991
//   (W779: these r values are over 5-7 arms CONSTRUCTED to vary monotonically in
//    the predictor, with no confidence interval. Report the PAIRS and the SLOPE;
//    r here measures the design, not the world -- T424.)
//
// Near-perfect on both, WITH OPPOSITE SIGNS. On UNSW the steepest alphabet is
// significantly BETTER (base 4 at 62.01% against linear 9's 56.31%, t=+3.34) and
// six times smaller; on Fashion it is 5.28 pp worse and NOT significant. A
// neuron that reads one of three inputs is a sign detector on the strongest one,
// and whether that is a loss is a property of the TASK, exactly as T355 found
// for the sparse penalty and T288 for the saturation rung.
//
// W779, tested where it could FAIL: {1,2,4,7} and dyadic have IDENTICAL junta
// degree 2.19 and sit on opposite sides of S6 (7=7 passes, 8>7 fails). At equal
// junta degree the S6-passing alphabet is significantly better on UNSW (+0.56 pp,
// t=+2.51) and not on Fashion (+0.17, ns); pooled across the filter it is
// significant on Fashion (+1.50, t=+5.25) and not on UNSW. Each task yields ONE
// significant result and they are different results. S6 contributes at most
// 0.56 pp of its own and has never been significant on both at once (T417).
//
// So S6 marks a real and exactly-locatable structural effect. It does NOT mark a
// defect. What it forbids is a base-only ranking rule: `b >= 3` claimed a
// COMPRESSION mechanism that does not exist, and the mechanism that does exist
// has task-dependent value. S6 is the interaction between S4's fan-in bound and
// the alphabet's skew -- the combining function T402a said the sieve lacked --
// and its sign must be measured per task, never assumed.
// ============================================================================

// The largest magnitude and the sum of the others, both as integers, so the
// predicate is exact rather than a float comparison.
pub fn s6_no_domination(top : u32, rest_sum : u32) -> bool {
    return top <= rest_sum;
}

// The ladder rung sums, written out: {b^0..b^3} for the integer bases S3 allows.
pub fn ladder_top(b : u32) -> u32 {
    return b * b * b;
}

pub fn ladder_rest(b : u32) -> u32 {
    return 1 + b + b * b;
}

pub fn ladder_survives_s6(b : u32) -> bool {
    return s6_no_domination(ladder_top(b), ladder_rest(b));
}

// ============================================================================
// Layer kind -- W777. A top computed on one layer type does not survive a
// network containing two.
//
// T398 measured a trained base-3 network against a dyadic one on the same
// silicon: 83 LUT against 89 in the TABLE layers, and 203 against 103 in the
// ADDER-TREE output. Base three wins where the table absorbs the arithmetic and
// loses where the arithmetic is real, because x3, x9, x27 are additions while
// x2, x4, x8 are shifts. Total 348 against 252.
//
// So admissibility is one question and RANKING is another, and the ranking needs
// to know which kind of layer it is ranking for.
// ============================================================================

pub const LAYER_TABLE : u32 = 0;   // enumerated into a case statement, 2.00 LUT/neuron
pub const LAYER_ADDER : u32 = 1;   // a real adder tree; the weight VALUES are paid for

// Whether a base's magnitudes are all powers of two. In an ADDER layer this is
// what decides between a shift and an addition; in a TABLE layer it is
// irrelevant, because the table has already absorbed the arithmetic.
pub fn is_shift_base(b : u32) -> bool {
    if (b == 2) { return true; }
    if (b == 4) { return true; }
    if (b == 8) { return true; }
    return false;
}

// The ranking rule, stated so it cannot be quoted out of its layer.
// Returns true when base `b` is the cheaper choice for a layer of kind `kind`.
// W778: WITHDRAWN AS WRITTEN. The old body returned `b >= 3` for LAYER_TABLE,
// on T366a's reading that a faster-growing base COMPRESSES better. It does not
// compress -- it lowers the neuron's effective fan-in (S6 above, r = +0.991
// between effective fan-in and LUT). Whether that trade is good was then
// measured and is TASK-DEPENDENT (T412): significantly better on UNSW, worse and
// non-significant on Fashion. A base-only rule cannot express that, whichever
// value it returns.
//
// The table-layer preference is therefore no longer a function of the base at
// all: every integer ladder fails S6, so the ladder family has no good member
// here and the ranking must range over non-ladder integer alphabets instead.
pub fn prefers_base(b : u32, kind : u32) -> bool {
    if (kind == LAYER_ADDER) {
        return is_shift_base(b);
    }
    // LAYER_TABLE: admissible only if the ladder clears S6, which no integer
    // base does. Kept as a function so the call sites still typecheck and so the
    // FALSE is stated by the predicate rather than by a comment.
    return ladder_survives_s6(b);
}

// What the table layer should rank on instead: the alphabet's own shape.
// linear 9 = {0,+-1,+-2,+-3,+-4} has top 4 against rest 6 and the highest
// measured effective fan-in of any integer nine-level alphabet, 2.55.
// W783/T444: linear 9 is not a hand-picked example -- it is the GLOBAL MAXIMISER
// of junta degree over the entire admissible nine-level integer space. All 1156
// alphabets {0,+-1,+-b,+-c,+-d} with d <= 1+b+c and d <= 24 were enumerated over
// all 9^3 triples: rank 1 of 1156 at 2.551, runner-up 2.519. The bound is not
// load-bearing -- maximum junta degree is non-increasing in spread and plateaus
// at 2.453 beyond d/a = 8 -- so no wider alphabet can overtake it.
pub const LINEAR9_TOP  : u32 = 4;
pub const LINEAR9_REST : u32 = 6;

// The runner-up, kept so the margin is checkable rather than asserted.
pub const RUNNERUP_TOP  : u32 = 5;   // {1,3,4,5}
pub const RUNNERUP_REST : u32 = 8;

// ============================================================================
// Invariants -- L4. These are the theorems, stated so the compiler checks them.
// ============================================================================

invariant s1_rejects_non_powers {
    assert(s1_packing(5) == false);
    assert(s1_packing(7) == false);
    assert(s1_packing(11) == false);
    assert(s1_packing(17) == false);
    assert(s1_packing(3));
    assert(s1_packing(9));
    assert(s1_packing(27));
}

invariant s2_stops_at_two_trits {
    assert(s2_ceiling(3));
    assert(s2_ceiling(9));
    assert(s1_packing(27));
    assert(s2_ceiling(27) == false);
}

invariant s3_is_commensurability_not_irrationality {
    // One magnitude: single lane whatever the base. This is {0,+-phi}, and the
    // hand-supplied version got it wrong.
    assert(s3_single_lane(1, false));
    assert(s3_single_lane(1, true));
    // Mixed powers of a rational base: single lane. {0,+-1,+-2,+-4,+-8}.
    assert(s3_single_lane(4, true));
    // Mixed powers of an irrational base: two lanes. {0,+-phi^0..3}, T293.
    assert(s3_single_lane(4, false) == false);
    assert(lanes_needed(4, false) == 2);
    assert(lanes_needed(1, false) == 1);
}

invariant six_bit_rule_is_three_trit_rule {
    assert(max_fanin(1) == 6);
    assert(max_fanin(TERNARY_SYMBOL_BITS) == 3);
    assert(s4_trit_fanin(6, 1));
    assert(s4_trit_fanin(3, TERNARY_SYMBOL_BITS));
    assert(s4_trit_fanin(6, TERNARY_SYMBOL_BITS) == false);
}

invariant twenty_seven_row_neuron {
    assert(ternary_rows(3) == 27);
    assert(binary_rows(3) == 64);
}

// W782/T442: the general statement, and it is why S1 and S2 have no unique kill
// on the ladder family. For A = {0} u {+-b^i : i < k}, b integer >= 2, k >= 2:
//     top = b^(k-1),  rest = (b^(k-1) - 1)/(b - 1) <= b^(k-1) - 1 < top
// so S6 fails for EVERY such alphabet, at every k. Exhaustively checked over
// b in [2,12] and k in [2,12]: zero counterexamples, and the margin at b=2 is
// exactly +1 for every k -- the tightest possible failure, never closing.
//
// The formula this file states therefore has exactly ONE admissible shape:
// k = 1, one magnitude, {0, +-c} -- three levels, one trit, balanced ternary.
invariant s6_kills_ladders_at_every_size {
    // k = 2 magnitudes: {1, b}
    assert s6_no_domination(2, 1) == false;
    assert s6_no_domination(3, 1) == false;
    // k = 3 magnitudes: {1, b, b^2}
    assert s6_no_domination(4, 3) == false;
    assert s6_no_domination(9, 4) == false;
    // k = 4 is ladder_survives_s6, already asserted below
    // k = 1 magnitude is the one survivor, and it is vacuous rather than lucky
    assert s6_no_domination(1, 1);
}

invariant s6_kills_every_integer_ladder {
    // The exact statement, checked rather than asserted in prose: no integer
    // base clears S6 at the nine-level rung. The boundary is the tribonacci
    // constant 1.8392867552, and the smallest integer above it is 2.
    assert(ladder_survives_s6(2) == false);   //  8 > 1+2+4  = 7
    assert(ladder_survives_s6(3) == false);   // 27 > 1+3+9  = 13
    assert(ladder_survives_s6(4) == false);   // 64 > 1+4+16 = 21
    assert(ladder_survives_s6(5) == false);
    // A non-ladder integer alphabet CAN clear it. This is what the formula must
    // widen to admit.
    assert(s6_no_domination(LINEAR9_TOP, LINEAR9_REST));
    assert(s6_no_domination(3, 4));           // fib {1,1,2,3}
    // One trit is vacuously safe: a single magnitude dominates nothing.
    assert(s6_no_domination(1, 1));
}

invariant ranking_depends_on_layer_kind {
    // The same base is preferred in one layer kind and not in the other. This is
    // the whole content of T398: a top is not a property of the number alone.
    assert(prefers_base(3, LAYER_ADDER) == false);
    assert(prefers_base(2, LAYER_ADDER));
    // W778: BOTH table answers are now false, and that is the result. The old
    // invariant asserted prefers_base(3, LAYER_TABLE) -- it was encoding
    // degeneracy as a preference.
    assert(prefers_base(3, LAYER_TABLE) == false);
    assert(prefers_base(2, LAYER_TABLE) == false);
}

// ============================================================================
// Tests -- L4
// ============================================================================

test levels_and_trits_round_trip {
    assert(levels_in_trits(0) == 1);
    assert(levels_in_trits(1) == 3);
    assert(levels_in_trits(2) == 9);
    assert(levels_in_trits(3) == 27);
    assert(trits_for_levels(1) == 0);
    assert(trits_for_levels(3) == 1);
    assert(trits_for_levels(9) == 2);
    assert(trits_for_levels(27) == 3);
}

test the_sieve_admits_only_the_formula {
    assert(admissible(3, 4, true, 3, TERNARY_SYMBOL_BITS, 0, 0));
    assert(admissible(9, 4, true, 3, TERNARY_SYMBOL_BITS, 0, 0));
    assert(admissible(27, 4, true, 3, TERNARY_SYMBOL_BITS, 0, 0) == false);
    assert(admissible(7, 4, true, 3, TERNARY_SYMBOL_BITS, 0, 0) == false);
    assert(admissible(9, 4, false, 3, TERNARY_SYMBOL_BITS, 0, 0) == false);
    assert(admissible(9, 4, true, 6, TERNARY_SYMBOL_BITS, 0, 0) == false);
    assert(admissible(9, 4, true, 3, TERNARY_SYMBOL_BITS, 1, 0) == false);
    assert(admissible(9, 4, true, 3, TERNARY_SYMBOL_BITS, 0, 44) == false);
}

test substrate_waste_is_measured_not_asserted {
    assert(ternary_rows(3) == 27);
    assert(binary_rows(3) == 64);
    assert(binary_rows(3) - ternary_rows(3) == 37);
}

// ============================================================================
// Bench -- L4
// ============================================================================

bench sieve_admissibility {
    assert(admissible(3, 4, true, 3, TERNARY_SYMBOL_BITS, 0, 0));
    assert(admissible(9, 4, true, 3, TERNARY_SYMBOL_BITS, 0, 0));
    assert(admissible(27, 4, true, 3, TERNARY_SYMBOL_BITS, 0, 0) == false);
}

// ============================================================================
// W778 -- the sieve run over the repository's own catalogue, as it stood on
// 2026-08-15 (83 formats).
//
// gen/numeric/formats_catalog.json held 83 numeric formats when this run was
// taken. The catalogue count is a CI invariant that grows (109 at v3, Sep 2026;
// tools/check_catalog_count.py reads it from the SSOT), so the 83 / 12 / 71 / 70
// below are this run's numbers, not the current count. 12 carry no width
// (techniques and parametric families) or a decimal encoding and cannot be
// sieved. Of the remaining 71, ONE is admissible as a ternary weight code:
// `gfternary`. The other 70 die on S1 alone -- every one of them is a
// power-of-two code space, and 2^n is a power of three for no n >= 1.
//
// That is a CATEGORY result before it is a quality one. The catalogue is an
// ACCUMULATOR catalogue; the sieve is a WEIGHT sieve; the overlap is one entry,
// and int8 being cut says nothing against int8.
//
// The one near miss is worth a name: gf4 and mxgf4 are the only catalogued
// formats whose level count could, under a different special-value convention,
// land on nine -- their span is [8,16] and 9 lies inside it. Under the IEEE
// convention they land on SEVEN. No format in the catalogue has nine levels.
//
// AND THE OVERCLAIM THAT DOES NOT SURVIVE, recorded because it was drafted:
// "nine levels fit two trits with zero waste and a 4-bit word with 44 percent
// waste" is FALSE as a storage claim. Nine levels need ceil(log2 9) = 4 bits
// either way and waste 7 of 16 codes either way. The trit advantage is in RUNS
// (five trits, 243 levels, fit 8 bits at 5 percent waste, against 10 bits for
// five separate 2-bit trits) and in TABLE ROWS (T368b: three ternary inputs
// reach 27 of a LUT6's 64 rows). It is not in one weight's storage.
// ============================================================================

// phi^2 + 1/phi^2 = 3 | TRINITY

Open the lesson's spec in the player ↗

All lessons