From 925767961c385b00f58f5add05d20adea69a03a5 Mon Sep 17 00:00:00 2001 From: Dmitrii Vasilev Date: Sun, 18 Oct 2026 18:00:14 +0700 Subject: [PATCH] numeric: paper_claims.t27 recomputes 45 numbers printed in the GoldenFloat, Golden Ruler and TNF papers; tri papers runs it (Closes #10392) Exact u64 arithmetic only. 34 fit, 8 do not fit, 3 not checkable. 10 of 10 tests pass, 0 vacuous (t27c 0.5.2 on the Railway lab). Co-Authored-By: Claude Opus 5.5 --- scripts/tri | 4 +- specs/numeric/paper_claims.t27 | 892 +++++++++++++++++++++++++++++++++ 2 files changed, 894 insertions(+), 2 deletions(-) create mode 100644 specs/numeric/paper_claims.t27 diff --git a/scripts/tri b/scripts/tri index e82815bae0..058dce193f 100755 --- a/scripts/tri +++ b/scripts/tri @@ -41,6 +41,7 @@ tri -- the t27 front door. Compiler commands (forwarded to t27c): tri test [--json] [...] run the conformance suite (t27c suite --repo-root .) + tri papers recompute the numbers three format papers print (specs/numeric/paper_claims.t27) tri forwarded to t27c unchanged (gen, seal, fpga-build, ...) Local commands (no compiler needed): @@ -530,7 +531,7 @@ if [[ ! -x "$T27C" ]]; then exit 2 fi - +[[ "$cmd" == "papers" ]] && exec "$T27C" test-report "$REPO_ROOT/specs/numeric/paper_claims.t27" "${@:2}" # Most subcommands are implemented in the Rust `tri` binary (cli/tri), # which is a DIFFERENT binary from t27c. Everything not handled above was # forwarded to t27c, so every one of them existed and was unreachable through the @@ -602,7 +603,6 @@ fi # `t27c suite` is the only subcommand that accepts --repo-root. # Map `tri test` to the suite subcommand; pass other commands through unchanged. if [[ "$cmd" == "test" || "$cmd" == "suite" ]]; then - # Forward everything after the subcommand to t27c suite, including --json. exec "$T27C" suite --repo-root "$REPO_ROOT" "${@:2}" else exec "$T27C" "$@" diff --git a/specs/numeric/paper_claims.t27 b/specs/numeric/paper_claims.t27 new file mode 100644 index 0000000000..151cb5b15c --- /dev/null +++ b/specs/numeric/paper_claims.t27 @@ -0,0 +1,892 @@ +// SPDX-License-Identifier: Apache-2.0 +; specs/numeric/paper_claims.t27 -- which numbers printed in three papers about our formats can be recomputed, +; and which of them come out the same. Every recomputation is exact integer arithmetic in this file. +; -- +; The papers: +; P_GF arXiv:2606.05017v5, GoldenFloat: e = round((N-1)/phi^2), f = N-1-e. +; P_RULER arXiv:2606.09686v3, the Golden Ruler catalog: 109 formats, 12 clusters, six conformance packs. +; P_TNF "TNF" by Dmitrii Vasilev (2026-08-11): four families GF, GF-T, BNF, TNF; 1 + Et + M = N. +; P_REPO the format specs of this repository (specs/numeric/gft*.t27, tnf*.t27, bnf*.t27). +; -- +; The rules: +; - A claim row holds what the paper prints (CL_PRINTED, in the unit CL_UNIT with CL_DEC decimals) and a +; recomputation (CL_KIND, CL_ARG). verdict_of() is V_FITS when the recomputed value equals the printed +; one exactly, V_MISFIT when it does not, and V_UNCHECKED when no recomputation exists (CL_KIND = K_NONE): +; a testbench run, a cross-validation against another library, a measured magnitude count. +; - Count rows (U_COUNT) print how many entries of a table the paper claims and recompute how many hold. +; - Irrational constants are never written down. sqrt(5) enters only through isqrt(5 a^2); ln 2, ln 3 and e +; are summed as series at scale 10^12; a rounded decimal is compared as an integer. +; - Rounding to three significant digits is half-to-even at an exact tie: 2^-5 = 3.125e-2 prints 3.12e-2. +; - The repo widths below (GFT_*, TNF_*, BNF_*) are a snapshot of specs/numeric at eb425e6ac, taken so the +; paper tables can be compared with them; the format specs stay the source of those widths. +; - The catalog counts CATALOG_RECORDS and CATALOG_CLUSTERS are measured on specs/numeric/formats_catalog.t27 +; (`t27c catalog-gate` reports 109 records; its cluster= fields name 13 distinct clusters). +; phi^2 + 1/phi^2 = 3 | TRINITY + +module NumericPaperClaims; + +pub const P_GF : u32 = 1; +pub const P_RULER : u32 = 2; +pub const P_TNF : u32 = 3; +pub const P_REPO : u32 = 4; + +pub const PAPERS : [5]str = [ + "", + "arXiv:2606.05017v5 GoldenFloat", + "arXiv:2606.09686v3 Golden Ruler", + "TNF paper (Vasilev, 2026-08-11)", + "t27 specs/numeric" +]; + +pub const V_FITS : u32 = 1; +pub const V_MISFIT : u32 = 2; +pub const V_UNCHECKED : u32 = 3; + +pub const VERDICTS : [4]str = ["", "fits", "does not fit", "not checkable"]; + +pub const U_INT : u32 = 0; +pub const U_DEC : u32 = 1; +pub const U_PCT : u32 = 2; +pub const U_HEX : u32 = 3; +pub const U_SCI3 : u32 = 4; +pub const U_COUNT : u32 = 5; + +pub const S12 : u64 = 1000000000000; +pub const E8 : u64 = 100000000; +pub const E10 : u64 = 10000000000; +pub const E13 : u64 = 10000000000000; +pub const E16 : u64 = 10000000000000000; +pub const E18 : u64 = 1000000000000000000; +pub const M6 : u64 = 1000000; + +/// No value: a code that is special, negative or not an integer, or a value a format cannot hold. +pub const NONE : u64 = 999999999; + +pub const CATALOG_RECORDS : u64 = 109; +pub const CATALOG_CLUSTERS : u64 = 13; + +// ---------------------------------------------------------------- GoldenFloat Table 1 (17 widths) +pub const GF_ROWS : u32 = 17; +pub const GF_N : [17]u64 = [4, 8, 12, 16, 20, 24, 32, 64, 256, 6, 10, 14, 48, 96, 128, 512, 1024]; +pub const GF_E_PRINTED : [17]u64 = [1, 3, 4, 6, 7, 9, 12, 24, 97, 2, 3, 5, 18, 36, 49, 195, 391]; +pub const GF_F_PRINTED : [17]u64 = [2, 4, 7, 9, 12, 14, 19, 39, 158, 3, 6, 8, 29, 59, 78, 316, 632]; +/// (N-1)/phi^2 as printed, times 10^4. +pub const GF_RAW_PRINTED : [17]u64 = [11459, 26738, 42016, 57295, 72574, 87852, 118409, 240639, 974013, + 19098, 34377, 49656, 179524, 362868, 485097, 1951846, 3907512]; + +// ---------------------------------------------------------------- the 3.0 packs (Golden Ruler) +pub const F_BF16 : u32 = 0; +pub const F_E4M3 : u32 = 1; +pub const F_E5M2 : u32 = 2; +pub const F_E2M1 : u32 = 3; +pub const F_GF16 : u32 = 4; +pub const F_E8M0 : u32 = 5; +pub const FMT_M : [6]u64 = [7, 3, 2, 1, 9, 0]; +pub const FMT_BIAS : [6]u64 = [127, 7, 15, 1, 31, 127]; + +// ---------------------------------------------------------------- TNF paper tables +pub const T1_ROWS : u32 = 8; +pub const T1_N : [8]u64 = [8, 16, 32, 64, 128, 256, 512, 1024]; +pub const T1_M : [8]u64 = [4, 9, 25, 52, 115, 242, 497, 1006]; +/// 2^-(M+1) as printed: three digits times 1000 plus the negated decimal exponent (9.77e-4 -> 977004). +pub const T1_POW2 : [8]u64 = [312002, 977004, 149008, 111016, 120035, 707074, 122150, 729304]; + +pub const T10_ROWS : u32 = 7; +pub const T10_ET : [7]u64 = [3, 4, 5, 6, 7, 8, 10]; +pub const T10_BITS : [7]u64 = [5, 7, 8, 10, 12, 13, 16]; +/// Packing efficiency 3^Et / 2^bits as printed, in tenths of a percent. +pub const T10_EFF : [7]u64 = [844, 633, 949, 712, 534, 801, 901]; + +pub const T11_ROWS : u32 = 10; +pub const T11_N : [10]u64 = [4, 8, 16, 32, 32, 64, 128, 256, 512, 1024]; +pub const T11_ET : [10]u64 = [2, 3, 4, 6, 5, 7, 8, 9, 10, 11]; +pub const T11_M : [10]u64 = [1, 4, 9, 25, 21, 52, 115, 242, 497, 1006]; +pub const T11_K : [10]u64 = [0, 0, 2, 0, 5, 4, 4, 4, 4, 6]; +/// Reconciled M as printed; 0 is the dash of the TNF32 note row. +pub const T11_RECON : [10]u64 = [1, 4, 11, 25, 0, 56, 119, 246, 501, 1012]; + +pub const T22_ROWS : u32 = 4; +/// Within-block span in binades as printed, times 100. +pub const T22_SPAN : [4]u64 = [189, 245, 304, 375]; +pub const T22_E : [4]u64 = [1, 2, 2, 2]; + +pub const LADDER : u32 = 9; +pub const LADDER_N : [9]u64 = [4, 8, 16, 32, 64, 128, 256, 512, 1024]; +pub const T24_GFT_ET : [9]u64 = [2, 3, 4, 5, 7, 8, 9, 10, 11]; +pub const T24_GFT_M : [9]u64 = [1, 4, 9, 21, 52, 115, 242, 497, 1006]; +pub const T24_TNF_ET : [9]u64 = [2, 3, 4, 6, 7, 8, 9, 10, 11]; +pub const T24_TNF_M : [9]u64 = [1, 4, 9, 25, 52, 115, 242, 497, 1006]; + +// ---------------------------------------------------------------- repo widths at eb425e6ac +pub const GFT_ET : [9]u64 = [1, 3, 6, 12, 24, 49, 97, 195, 391]; +pub const GFT_M : [9]u64 = [2, 4, 9, 19, 39, 78, 158, 316, 632]; +pub const TNF_ET : [9]u64 = [2, 3, 4, 6, 7, 8, 9, 10, 11]; +pub const TNF_M : [9]u64 = [1, 4, 11, 25, 56, 119, 246, 501, 1012]; +pub const BNF_ROWS : u32 = 8; +pub const BNF_N : [8]u64 = [8, 16, 32, 64, 128, 256, 512, 1024]; +pub const BNF_E : [8]u64 = [5, 7, 10, 12, 13, 15, 16, 18]; +pub const BNF_M : [8]u64 = [2, 8, 21, 51, 114, 240, 495, 1005]; + +// ---------------------------------------------------------------- recomputation kinds +pub const K_NONE : u32 = 0; +pub const K_GF_EXP : u32 = 1; +pub const K_GF_TABLE1 : u32 = 2; +pub const K_GF_RAW : u32 = 3; +pub const K_GF_RAW_ONE : u32 = 4; +pub const K_LUCAS_COUNT : u32 = 5; +pub const K_LUCAS : u32 = 6; +pub const K_GF16_DECODE : u32 = 7; +pub const K_SUMSQ : u32 = 8; +pub const K_P_SCI3 : u32 = 9; +pub const K_ENC3 : u32 = 10; +pub const K_CLUSTERS : u32 = 11; +pub const K_RECORDS : u32 = 12; +pub const K_T1_POW2 : u32 = 13; +pub const K_T1_M : u32 = 14; +pub const K_HALF_LN2 : u32 = 15; +pub const K_QUARTER_INV_LN2 : u32 = 16; +pub const K_T10_BITS : u32 = 17; +pub const K_T10_EFF : u32 = 18; +pub const K_T11_K : u32 = 19; +pub const K_T11_RECON : u32 = 20; +pub const K_RADIX_BP : u32 = 21; +pub const K_KAPPA : u32 = 22; +pub const K_ONE_MINUS_LOG3_2 : u32 = 23; +pub const K_T22 : u32 = 24; +pub const K_FAMILY : u32 = 25; +pub const K_T24_GFT_GOLDEN : u32 = 26; +pub const K_T24_IDENTICAL : u32 = 27; +pub const K_T24_SUM : u32 = 28; +pub const K_TNF16_M : u32 = 29; +pub const K_TRIT_RANGE : u32 = 30; +pub const K_TRIT_STEPS : u32 = 31; +pub const K_BNF8_E : u32 = 32; +pub const K_REPO_GFT_GOLDEN : u32 = 33; +pub const K_REPO_SUMS : u32 = 34; + +// ---------------------------------------------------------------- the claims +pub const ROWS : u32 = 45; + +pub const CL_PAPER : [45]u32 = [ + 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, + 2, 2, 2, 2, 2, 2, 2, 2, 2, 2, + 3, 3, 3, 3, 3, 3, 3, 3, 3, 3, + 3, 3, 3, 3, 3, 3, 3, 3, 3, 3, + 3, 3, 3, 4, 4 +]; + +pub const CL_WHERE : [45]str = [ + "Table 1", "Table 1", "Table 1", "Table 1", "Table 1", "Abstract", "GF16 anchor", "GF16 anchor", + "Look-elsewhere", "Abstract", + "Abstract", "Abstract", "Packs", "Packs", "Packs", "Packs", "Packs", "Packs", "Anchor", "Abstract", + "Table 1", "Table 1 vs Sec. 10", "Eq. (1)", "Sec. 2", "Sec. 2", "Sec. 3", "Sec. 3", "Table 10", "Table 10", + "Table 11", "Table 11", "Sec. 17", "Sec. 17", "Cor. 18", "Sec. 17", "Cor. 26", "Table 22", "Sec. 17", + "Table 24", "Table 24", "Table 24 vs Sec. 10", "Table 23", "Table 23", + "gft*.t27", "tnf*.t27, bnf*.t27" +]; + +pub const CL_TEXT : [45]str = [ + "e = round((N-1)/phi^2), f = N-1-e gives the printed (e, f) at all 17 widths", + "(N-1)/phi^2 to four decimals, as printed, at all 17 widths", + "GF16: e = 6", + "GF1024: e = 391", + "GF16: (N-1)/phi^2 = 5.7295", + "phi^(2n) + phi^(-2n) = L_(2n) for n = 1..45 (the paper claims 1..256 at 500 digits; u64 stops at 45)", + "GF16 code 0x47C0 (e = 6, f = 9, bias 31) decodes to 30", + "30 = 1^2 + 2^2 + 3^2 + 4^2, the dot4 anchor", + "p = K / N_s = 83 / 80000 = 1.04e-3", + "35 of 35 testbench vectors at 323 MHz on an XC7A35T", + "the catalog holds 109 formats", + "the 109 formats span 12 clusters", + "3.0 in BF16 is 0x4040", + "3.0 in FP8 E4M3 is 0x44", + "3.0 in FP8 E5M2 is 0x42", + "3.0 in the MXFP4 element E2M1 is 0x5", + "3.0 in GF16 is 0x4100", + "3.0 has no E8M0 code: E8M0 holds powers of two only", + "phi^2 + phi^-2 = L_2 = 3", + "the packs are cross-validated against ml_dtypes 0.5.4", + "2^-(M+1) matches the printed M at all 8 rungs", + "the printed M equals the adopted M = N - 1 - Et at all 8 rungs (Sec. 10: all rungs satisfy 1 + Et + M = N)", + "TNF16 value = (1 + M/2^9) 2^e: a 9-bit mantissa, where 1 + 4 + M = 16 needs 11", + "four balanced trits give e in [-40, 40]", + "four balanced trits give 3^4 = 81 exponent steps", + "error constant (1/2) ln 2 = 0.3466 for a uniform significand", + "error constant 1/(4 ln 2) = 0.3607 for a logarithmic significand", + "bits = ceil(Et log2 3) at all 7 rows", + "efficiency 3^Et / 2^bits to 0.1% at all 7 rows", + "k = N - (1 + Et + M) at all 10 rows", + "reconciled M = N - 1 - Et at all 9 rows, equal to the repo tnf*.t27", + "ternary radix economy 3/ln 3 sits 0.46% above e/ln e", + "binary radix economy 2/ln 2 sits 6.15% above e/ln e", + "kappa(3)/kappa(2) = 1.683 with kappa(r) = (r-1)^2 / (r ln r)", + "kappa(3)/kappa(2) = 1.68", + "1 - log3 2 = 0.3691", + "E* = ceil(log2 b) at all 4 percentiles", + "the family F_N has N - 3 members (N = 16: 13)", + "the GF-T column follows Et = round((N-1)/phi^2) at all 9 rungs", + "GF-T and TNF give the same layout at 8 of 9 rungs (by their rules: golden GF-T against reconciled TNF)", + "the TNF column obeys 1 + Et + M = N at all 9 rungs (Sec. 10)", + "BNF8 is E = 3, M = 4 (the repo bnf8.t27 is E = 5, M = 2)", + "magnitude counts 129 / 109 / 73 for GF8, GF-T8, TNF8", + "the repo GF-T rungs follow Et = round((N-1)/phi^2) at all 9 rungs", + "every repo TNF and BNF rung obeys 1 + E + M = N (9 TNF, 8 BNF)" +]; + +pub const CL_KIND : [45]u32 = [ + 2, 3, 1, 1, 4, 5, 7, 8, 9, 0, + 12, 11, 10, 10, 10, 10, 10, 10, 6, 0, + 13, 14, 29, 30, 31, 15, 16, 17, 18, 19, + 20, 21, 21, 22, 22, 23, 24, 25, 26, 27, + 28, 32, 0, 33, 34 +]; + +pub const CL_ARG : [45]u64 = [ + 0, 0, 16, 1024, 16, 0, 18368, 4, 0, 0, + 0, 0, 0, 1, 2, 3, 4, 5, 2, 0, + 0, 0, 0, 4, 4, 0, 0, 0, 0, 0, + 0, 3, 2, 3, 2, 0, 0, 16, 0, 0, + 0, 0, 0, 0, 0 +]; + +pub const CL_PRINTED : [45]u64 = [ + 17, 17, 6, 391, 57295, 45, 30, 30, 104003, 35, + 109, 12, 16448, 68, 66, 5, 16640, 999999999, 3, 0, + 8, 8, 9, 40, 81, 3466, 3607, 7, 7, 10, + 9, 46, 615, 1683, 168, 3691, 4, 13, 9, 8, + 9, 3, 0, 9, 17 +]; + +pub const CL_UNIT : [45]u32 = [ + 5, 5, 0, 0, 1, 5, 0, 0, 4, 0, + 0, 0, 3, 3, 3, 3, 3, 0, 0, 0, + 5, 5, 0, 0, 0, 1, 1, 5, 5, 5, + 5, 2, 2, 1, 1, 1, 5, 0, 5, 5, + 5, 0, 0, 5, 5 +]; + +pub const CL_DEC : [45]u32 = [ + 0, 0, 0, 0, 4, 0, 0, 0, 0, 0, + 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, + 0, 0, 0, 0, 0, 4, 4, 0, 0, 0, + 0, 2, 2, 3, 2, 4, 0, 0, 0, 0, + 0, 0, 0, 0, 0 +]; + +// ---------------------------------------------------------------- exact integer helpers + +/// floor(sqrt(n)) for n >= 0, by bisection. +pub fn isqrt(n: u64) -> u64 { + var lo : u64 = 0; + var hi : u64 = 1; + while (hi * hi <= n) { hi = hi * 2; } + while (lo + 1 < hi) { + let mid : u64 = (lo + hi) / 2; + if (mid * mid <= n) { lo = mid; } else { hi = mid; } + } + return lo; +} + +/// GF exponent width round((N-1)/phi^2). With a = N-1, (N-1)/phi^2 = (3a - a sqrt5)/2 and a sqrt5 is +/// irrational for a > 0, so the rounded value is floor((3a - isqrt(5 a^2)) / 2). +pub fn gf_exp(n: u64) -> u64 { + let a : u64 = n - 1; + if (a <= 0) { return 0; } + return (3 * a - isqrt(5 * a * a)) / 2; +} + +/// (N-1)/phi^2 times 10^4, rounded half up, by the same argument at scale 10^4. +pub fn gf_raw_e4(n: u64) -> u64 { + let a : u64 = n - 1; + if (a <= 0) { return 0; } + return (30000 * a - isqrt(500000000 * a * a)) / 2; +} + +pub fn pow_i(b: u64, k: u64) -> u64 { + var r : u64 = 1; + var i : u64 = 0; + while (i < k) { r = r * b; i = i + 1; } + return r; +} + +pub fn fib(k: u64) -> u64 { + var a : u64 = 0; + var b : u64 = 1; + var i : u64 = 0; + while (i < k) { + let t : u64 = a + b; + a = b; + b = t; + i = i + 1; + } + return a; +} + +/// Lucas numbers by their own recurrence, L_0 = 2, L_1 = 1. +pub fn lucas(k: u64) -> u64 { + var a : u64 = 2; + var b : u64 = 1; + var i : u64 = 0; + while (i < k) { + let t : u64 = a + b; + a = b; + b = t; + i = i + 1; + } + return a; +} + +/// In Z[phi], phi^k = F_k phi + F_(k-1) and psi^k = F_k psi + F_(k-1), and phi^-1 = -psi, so +/// phi^(2n) + phi^(-2n) = F_(2n) + 2 F_(2n-1). Count the n in 1..45 where that equals L_(2n). +pub fn lucas_count() -> u64 { + var n : u64 = 1; + var c : u64 = 0; + while (n <= 45) { + if (lucas(2 * n) == fib(2 * n) + 2 * fib(2 * n - 1)) { c = c + 1; } + n = n + 1; + } + return c; +} + +/// Integer value of a positive GF16 code (1 sign, 6 exponent, 9 mantissa bits, bias 31), or NONE when +/// the code is negative or special or its value is not an integer. +pub fn gf16_int(code: u64) -> u64 { + let e : u64 = (code / 512) % 64; + let m : u64 = code % 512; + if (e == 63) { return NONE; } + if (e < 31) { return NONE; } + var v : u64 = 512 + m; + var s : u64 = e - 31; + while (s > 0) { v = v * 2; s = s - 1; } + if (v % 512 != 0) { return NONE; } + v = v / 512; + if (code >= 32768) { return NONE; } + return v; +} + +pub fn sumsq(n: u64) -> u64 { + var i : u64 = 1; + var s : u64 = 0; + while (i <= n) { s = s + i * i; i = i + 1; } + return s; +} + +/// m / unit rounded half to even. +pub fn round_even(m: u64, unit: u64) -> u64 { + var q : u64 = m / unit; + let r : u64 = m % unit; + let half : u64 = unit / 2; + if (r > half) { q = q + 1; } + if (r == half) { + if (q % 2 == 1) { q = q + 1; } + } + return q; +} + +/// 2^-k to three significant digits: digits * 1000 + the negated decimal exponent. +pub fn pow2_sci3(k: u64) -> u64 { + var m : u64 = E13; + var ex : u64 = 0; + var i : u64 = 0; + while (i < k) { + m = m / 2; + if (m < E13) { + m = m * 10; + ex = ex + 1; + } + i = i + 1; + } + var d : u64 = round_even(m, E10 * 10); + if (d == 1000) { + d = 100; + ex = ex - 1; + } + return d * 1000 + ex; +} + +/// p/q (0 < p < q) to three significant digits, in the pow2_sci3 encoding. +pub fn ratio_sci3(p0: u64, q: u64) -> u64 { + var p : u64 = p0; + var ex : u64 = 0; + while (p < q) { + p = p * 10; + ex = ex + 1; + } + let m : u64 = p * S12 / q; + var d : u64 = round_even(m, E10); + if (d == 1000) { + d = 100; + ex = ex - 1; + } + return d * 1000 + ex; +} + +/// ln 2 at scale 10^12: sum over k of 1 / (k 2^k). +pub fn ln2_s() -> u64 { + var s : u64 = 0; + var k : u64 = 1; + var p : u64 = 2; + while (k <= 40) { + s = s + S12 / (k * p); + p = p * 2; + k = k + 1; + } + return s; +} + +/// ln 3 at scale 10^12: ln 2 + ln(3/2), and ln(3/2) = 2 atanh(1/5) = 2 sum 1 / ((2j+1) 5^(2j+1)). +pub fn ln3_s() -> u64 { + var s : u64 = 0; + var j : u64 = 0; + var p : u64 = 5; + while (j <= 10) { + s = s + 2 * S12 / ((2 * j + 1) * p); + p = p * 25; + j = j + 1; + } + return ln2_s() + s; +} + +/// e at scale 10^12: sum of 1/k!. +pub fn e_s() -> u64 { + var s : u64 = 0; + var f : u64 = 1; + var k : u64 = 0; + while (k <= 17) { + if (k > 0) { f = f * k; } + s = s + S12 / f; + k = k + 1; + } + return s; +} + +/// How far the radix economy r/ln r sits above its minimum e/ln e = e, in hundredths of a percent. +pub fn radix_bp(r: u64) -> u64 { + var lnr : u64 = ln2_s(); + if (r == 3) { lnr = ln3_s(); } + let p : u64 = lnr * (e_s() / M6) / M6; + let ratio6 : u64 = r * E18 / p; + return (ratio6 - M6 + 50) / 100; +} + +/// kappa(3)/kappa(2) = (4 / (3 ln 3)) / (1 / (2 ln 2)) = 8 ln 2 / (3 ln 3), rounded to dec decimals. +pub fn kappa_ratio(dec: u64) -> u64 { + let scale : u64 = pow_i(10, dec); + let l3 : u64 = ln3_s(); + return (16 * scale * ln2_s() + 3 * l3) / (6 * l3); +} + +pub fn half_ln2_e4() -> u64 { + return (ln2_s() + E8) / (2 * E8); +} + +pub fn quarter_inv_ln2_e4() -> u64 { + let l2 : u64 = ln2_s(); + return (2 * E16 + 4 * l2) / (8 * l2); +} + +pub fn one_minus_log3_2_e4() -> u64 { + let l3 : u64 = ln3_s(); + return (20000 * (l3 - ln2_s()) + l3) / (2 * l3); +} + +/// 3.0 = 1.5 * 2^1 in a format with m mantissa bits and the given bias, or NONE when m = 0. +pub fn encode3(f: u32) -> u64 { + let m : u64 = FMT_M[f]; + if (m == 0) { return NONE; } + return (1 + FMT_BIAS[f]) * pow_i(2, m) + pow_i(2, m - 1); +} + +/// Smallest b with 2^b >= v. +pub fn ceil_log2(v: u64) -> u64 { + var b : u64 = 0; + var p : u64 = 1; + while (p < v) { + p = p * 2; + b = b + 1; + } + return b; +} + +/// Members (Et, M) of F_N: 1 + Et + M = N, Et >= 2, M >= 1. +pub fn family_size(n: u64) -> u64 { + var c : u64 = 0; + var et : u64 = 2; + while (et <= n) { + if (et + 2 <= n) { c = c + 1; } + et = et + 1; + } + return c; +} + +// ---------------------------------------------------------------- table counts + +pub fn gf_table1_count() -> u64 { + var i : u32 = 0; + var c : u64 = 0; + while (i < GF_ROWS) { + let e : u64 = gf_exp(GF_N[i]); + if (e == GF_E_PRINTED[i]) { + if (GF_N[i] - 1 - e == GF_F_PRINTED[i]) { c = c + 1; } + } + i = i + 1; + } + return c; +} + +pub fn gf_raw_count() -> u64 { + var i : u32 = 0; + var c : u64 = 0; + while (i < GF_ROWS) { + if (gf_raw_e4(GF_N[i]) == GF_RAW_PRINTED[i]) { c = c + 1; } + i = i + 1; + } + return c; +} + +pub fn t1_pow2_count() -> u64 { + var i : u32 = 0; + var c : u64 = 0; + while (i < T1_ROWS) { + if (pow2_sci3(T1_M[i] + 1) == T1_POW2[i]) { c = c + 1; } + i = i + 1; + } + return c; +} + +/// Table 1 starts at TNF8, which is rung 1 of the ladder. +pub fn t1_m_count() -> u64 { + var i : u32 = 0; + var c : u64 = 0; + while (i < T1_ROWS) { + if (T1_M[i] == T1_N[i] - 1 - TNF_ET[i + 1]) { c = c + 1; } + i = i + 1; + } + return c; +} + +pub fn t10_bits_count() -> u64 { + var i : u32 = 0; + var c : u64 = 0; + while (i < T10_ROWS) { + if (ceil_log2(pow_i(3, T10_ET[i])) == T10_BITS[i]) { c = c + 1; } + i = i + 1; + } + return c; +} + +pub fn t10_eff_count() -> u64 { + var i : u32 = 0; + var c : u64 = 0; + while (i < T10_ROWS) { + let num : u64 = pow_i(3, T10_ET[i]) * 1000; + let den : u64 = pow_i(2, T10_BITS[i]); + if ((2 * num + den) / (2 * den) == T10_EFF[i]) { c = c + 1; } + i = i + 1; + } + return c; +} + +pub fn t11_k_count() -> u64 { + var i : u32 = 0; + var c : u64 = 0; + while (i < T11_ROWS) { + if (T11_N[i] - (1 + T11_ET[i] + T11_M[i]) == T11_K[i]) { c = c + 1; } + i = i + 1; + } + return c; +} + +/// Index of width n in the ladder, or LADDER. +pub fn ladder_index(n: u64) -> u32 { + var i : u32 = 0; + while (i < LADDER) { + if (LADDER_N[i] == n) { return i; } + i = i + 1; + } + return LADDER; +} + +pub fn t11_recon_count() -> u64 { + var i : u32 = 0; + var c : u64 = 0; + while (i < T11_ROWS) { + if (T11_RECON[i] != 0) { + let j : u32 = ladder_index(T11_N[i]); + if (T11_RECON[i] == T11_N[i] - 1 - T11_ET[i]) { + if (j < LADDER) { + if (TNF_M[j] == T11_RECON[i]) { c = c + 1; } + } + } + } + i = i + 1; + } + return c; +} + +pub fn t22_count() -> u64 { + var i : u32 = 0; + var c : u64 = 0; + while (i < T22_ROWS) { + var e : u64 = 0; + var p : u64 = 100; + while (p < T22_SPAN[i]) { + p = p * 2; + e = e + 1; + } + if (e == T22_E[i]) { c = c + 1; } + i = i + 1; + } + return c; +} + +pub fn t24_gft_golden_count() -> u64 { + var i : u32 = 0; + var c : u64 = 0; + while (i < LADDER) { + let e : u64 = gf_exp(LADDER_N[i]); + if (T24_GFT_ET[i] == e) { + if (T24_GFT_M[i] == LADDER_N[i] - 1 - e) { c = c + 1; } + } + i = i + 1; + } + return c; +} + +/// Rungs where the golden rule and the reconciled width rule choose the same Et. +pub fn t24_identical_count() -> u64 { + var i : u32 = 0; + var c : u64 = 0; + while (i < LADDER) { + if (gf_exp(LADDER_N[i]) == TNF_ET[i]) { c = c + 1; } + i = i + 1; + } + return c; +} + +pub fn t24_sum_count() -> u64 { + var i : u32 = 0; + var c : u64 = 0; + while (i < LADDER) { + if (1 + T24_TNF_ET[i] + T24_TNF_M[i] == LADDER_N[i]) { c = c + 1; } + i = i + 1; + } + return c; +} + +pub fn repo_gft_golden_count() -> u64 { + var i : u32 = 0; + var c : u64 = 0; + while (i < LADDER) { + let e : u64 = gf_exp(LADDER_N[i]); + if (GFT_ET[i] == e) { + if (GFT_M[i] == LADDER_N[i] - 1 - e) { c = c + 1; } + } + i = i + 1; + } + return c; +} + +pub fn repo_sums_count() -> u64 { + var i : u32 = 0; + var c : u64 = 0; + while (i < LADDER) { + if (1 + TNF_ET[i] + TNF_M[i] == LADDER_N[i]) { c = c + 1; } + i = i + 1; + } + i = 0; + while (i < BNF_ROWS) { + if (1 + BNF_E[i] + BNF_M[i] == BNF_N[i]) { c = c + 1; } + i = i + 1; + } + return c; +} + +// ---------------------------------------------------------------- dispatch and verdicts + +pub fn recompute(kind: u32, arg: u64) -> u64 { + if (kind == K_GF_EXP) { return gf_exp(arg); } + if (kind == K_GF_TABLE1) { return gf_table1_count(); } + if (kind == K_GF_RAW) { return gf_raw_count(); } + if (kind == K_GF_RAW_ONE) { return gf_raw_e4(arg); } + if (kind == K_LUCAS_COUNT) { return lucas_count(); } + if (kind == K_LUCAS) { return lucas(arg); } + if (kind == K_GF16_DECODE) { return gf16_int(arg); } + if (kind == K_SUMSQ) { return sumsq(arg); } + if (kind == K_P_SCI3) { return ratio_sci3(83, 80000); } + if (kind == K_ENC3) { return encode3(arg as u32); } + if (kind == K_CLUSTERS) { return CATALOG_CLUSTERS; } + if (kind == K_RECORDS) { return CATALOG_RECORDS; } + if (kind == K_T1_POW2) { return t1_pow2_count(); } + if (kind == K_T1_M) { return t1_m_count(); } + if (kind == K_HALF_LN2) { return half_ln2_e4(); } + if (kind == K_QUARTER_INV_LN2) { return quarter_inv_ln2_e4(); } + if (kind == K_T10_BITS) { return t10_bits_count(); } + if (kind == K_T10_EFF) { return t10_eff_count(); } + if (kind == K_T11_K) { return t11_k_count(); } + if (kind == K_T11_RECON) { return t11_recon_count(); } + if (kind == K_RADIX_BP) { return radix_bp(arg); } + if (kind == K_KAPPA) { return kappa_ratio(arg); } + if (kind == K_ONE_MINUS_LOG3_2) { return one_minus_log3_2_e4(); } + if (kind == K_T22) { return t22_count(); } + if (kind == K_FAMILY) { return family_size(arg); } + if (kind == K_T24_GFT_GOLDEN) { return t24_gft_golden_count(); } + if (kind == K_T24_IDENTICAL) { return t24_identical_count(); } + if (kind == K_T24_SUM) { return t24_sum_count(); } + if (kind == K_TNF16_M) { return 16 - 1 - TNF_ET[2]; } + if (kind == K_TRIT_RANGE) { return (pow_i(3, arg) - 1) / 2; } + if (kind == K_TRIT_STEPS) { return pow_i(3, arg); } + if (kind == K_BNF8_E) { return BNF_E[0]; } + if (kind == K_REPO_GFT_GOLDEN) { return repo_gft_golden_count(); } + if (kind == K_REPO_SUMS) { return repo_sums_count(); } + return 0; +} + +pub fn verdict_of(kind: u32, arg: u64, printed: u64) -> u32 { + if (kind == K_NONE) { return V_UNCHECKED; } + if (recompute(kind, arg) == printed) { return V_FITS; } + return V_MISFIT; +} + +pub fn row_recomputed(i: u32) -> u64 { + return recompute(CL_KIND[i], CL_ARG[i]); +} + +pub fn row_verdict(i: u32) -> u32 { + return verdict_of(CL_KIND[i], CL_ARG[i], CL_PRINTED[i]); +} + +/// How many rows of a paper (0 = all papers) have verdict v. +pub fn count_verdict(paper: u32, v: u32) -> u32 { + var i : u32 = 0; + var c : u32 = 0; + while (i < ROWS) { + if (paper == 0 || CL_PAPER[i] == paper) { + if (row_verdict(i) == v) { c = c + 1; } + } + i = i + 1; + } + return c; +} + +// ---------------------------------------------------------------- tests + +test "golden rule: exact exponent widths across the ladder" { + assert gf_exp(4) == 1; + assert gf_exp(8) == 3; + assert gf_exp(16) == 6; + assert gf_exp(32) == 12; + assert gf_exp(256) == 97; + assert gf_exp(1024) == 391; + assert gf_exp(1) == 0; + assert isqrt(1125) == 33; + assert isqrt(1089) == 33; + assert isqrt(1088) == 32; +} + +test "golden rule: raw values at scale 10^4" { + assert gf_raw_e4(4) == 11459; + assert gf_raw_e4(16) == 57295; + assert gf_raw_e4(1024) == 3907512; + assert gf_table1_count() == 17; + assert gf_raw_count() == 17; +} + +test "Lucas and the anchors" { + assert lucas(2) == 3; + assert lucas(10) == 123; + assert fib(10) == 55; + assert lucas(90) == fib(90) + 2 * fib(89); + assert lucas_count() == 45; + assert gf16_int(18368) == 30; + assert gf16_int(16640) == 3; + assert gf16_int(16384) == 2; + assert gf16_int(32768 + 18368) == NONE; + assert gf16_int(15872) == 1; + assert gf16_int(15873) == NONE; + assert sumsq(4) == 30; +} + +test "three significant digits, half to even at a tie" { + assert pow2_sci3(5) == 312002; + assert pow2_sci3(10) == 977004; + assert pow2_sci3(53) == 111016; + assert pow2_sci3(1007) == 729304; + assert pow2_sci3(1) == 500001; + assert ratio_sci3(83, 80000) == 104003; + assert ratio_sci3(1, 8) == 125001; + assert round_even(125, 10) == 12; + assert round_even(135, 10) == 14; + assert round_even(126, 10) == 13; +} + +test "3.0 in the six packs" { + assert encode3(F_BF16) == 16448; + assert encode3(F_E4M3) == 68; + assert encode3(F_E5M2) == 66; + assert encode3(F_E2M1) == 5; + assert encode3(F_GF16) == 16640; + assert encode3(F_E8M0) == NONE; +} + +test "series constants" { + assert half_ln2_e4() == 3466; + assert quarter_inv_ln2_e4() == 3607; + assert radix_bp(3) == 46; + assert radix_bp(2) == 615; + assert kappa_ratio(3) == 1682; + assert kappa_ratio(2) == 168; + assert one_minus_log3_2_e4() == 3691; + assert ln2_s() / 1000 == 693147180; + assert e_s() / 1000 == 2718281828; +} + +test "TNF paper tables" { + assert t1_pow2_count() == 8; + assert t1_m_count() == 2; + assert t10_bits_count() == 7; + assert t10_eff_count() == 7; + assert t11_k_count() == 10; + assert t11_recon_count() == 9; + assert t22_count() == 4; + assert family_size(16) == 13; + assert t24_gft_golden_count() == 1; + assert t24_identical_count() == 1; + assert t24_sum_count() == 3; + assert repo_gft_golden_count() == 9; + assert repo_sums_count() == 17; +} + +test "the verdict of every claim" { + assert count_verdict(0, V_FITS) == 34; + assert count_verdict(0, V_MISFIT) == 8; + assert count_verdict(0, V_UNCHECKED) == 3; + assert count_verdict(P_GF, V_FITS) == 9; + assert count_verdict(P_RULER, V_MISFIT) == 1; + assert count_verdict(P_TNF, V_MISFIT) == 7; + assert count_verdict(P_TNF, V_FITS) == 15; + assert count_verdict(P_REPO, V_FITS) == 2; + assert row_verdict(11) == V_MISFIT; + assert row_recomputed(11) == 13; + assert row_verdict(21) == V_MISFIT; + assert row_recomputed(22) == 11; + assert row_recomputed(33) == 1682; + assert row_recomputed(38) == 1; + assert row_recomputed(41) == 5; + assert row_verdict(42) == V_UNCHECKED; +} + +test "negative control: a printed value off by one is a misfit, and an unchecked row stays unchecked" { + assert verdict_of(K_GF_EXP, 16, 6) == V_FITS; + assert verdict_of(K_GF_EXP, 16, 7) == V_MISFIT; + assert verdict_of(K_KAPPA, 3, 1682) == V_FITS; + assert verdict_of(K_ENC3, 1, 69) == V_MISFIT; + assert verdict_of(K_NONE, 0, 35) == V_UNCHECKED; +} + +test "the claim table is whole" { + assert PAPERS[P_TNF] == "TNF paper (Vasilev, 2026-08-11)"; + assert VERDICTS[V_MISFIT] == "does not fit"; + assert CL_PAPER[44] == P_REPO; + assert CL_KIND[42] == K_NONE; +}