#!/usr/bin/env python3 """v785 -- HECKE.CARRIER_CHECK32.01: the mod-32 carrier congruence of the TFPT cusp channel -- f8 = eta(2 tau)^4 eta(4 tau)^4 == E_odd = sum_{n odd} sigma3(n) q^n (mod 32), verified coefficient-wise to q^100000 = 25000x the Sturm bound, Sturm-certified: the Sturm step is the ONE cited classical theorem (Sturm 1987), bound (4/12)*[SL2(Z):Gamma_0(8)] = (4/12)*12 = 4 (20/20 checks, ~41 s, verdict CHECK32-THEOREM; discovery probe hecke_check32_probe.py, 2026-08-05). COROLLARY CENSUS: a_p == 1 + p^3 (mod 32) for ALL 9591/9591 odd primes p < 10^5 (zero failures), with the explicit decoder p == (a_p - 1)^3 (mod 32) exact on every tested prime because the cube map r -> r^3 is a BIJECTION on the 16 odd residues mod 32 (finite census). MAXIMALITY: the congruence does NOT lift to mod 64 -- it fails already at q^3 (a_3 - (1 + 27) = -4 - 28 = -32, zero mod 32 but NOT mod 64), and the mod-64 census on the first 1000 odd primes has 252/1000 failures (mod 32: 0/1000); structural observation (typed as observation, NOT derivation): 32 = 2^g_car (g_car = 5, axiom P2) = dim(S+ + S-) = 16 + 16 of the D5 spinor layer (v774) = 28 - (-4) = the pi_cusp denominator (v535 N4a). HECKE GRAMMAR clean on the computed coefficients: multiplicativity a_(mn) = a_m a_n on all 289291 coprime pairs with mn <= 10^5, good-prime recurrence on all 93 odd prime powers <= 10^5, ramified U_2 law a_(2^k) = a_2^k = 0 (2 | level 8), derived mod-32 prime-power law a_(p^k) == sigma3(p^k) (mod 32); the eta build is cross-checked against an independent pure-dict rebuild to q^2000 and the v535 corpus anchors (a_3 = -4, a_5 = -2, a_7 = 24, a_11 = -44, a_13 = 22). CONTROLS FIRE: the mutant eta(2t)^4 eta(4t)^3 breaks the census immediately -- first failing prime p = 5 (p = 3 passes by a single 1/32-type coincidence), failure fraction 1126/1228 = 91.7%; random growth-matched integer sequences (seed 20260805, 100 trials x 1228 primes) are detected at ~31/32 (measured mean per-prime pass rate 0.0324 ~ 1/32 = 0.0312). Lean layer: experiments/lean4-carrier-rigidity/TfptCarrier/Check32.lean (13 theorems, Lean tree 80 modules, built green) formalizes the mod-32 congruence kernel. No marker move, NO RH claim. Python-only per GATE.WOLFRAM.02. PROVENANCE: discovery probe hecke_check32_probe.py (2026-08-05, 20/20, ~41 s, CHECK32-THEOREM; the two disclosed harness amendments carried verbatim in the original docstring below -- S5 first draft applied the good-prime T_p recurrence at the ramified p = 2, fixed to good primes + explicit U_2 check; S6/C1 first draft predeclared "first failing prime = 3", the mutant passes p = 3 by a single mod-32 coincidence and first fails at p = 5, assertion relaxed to first-fail within the first two odd primes + fraction > 1/2; data unchanged in both); re-run identically at promotion. Promoted verbatim (all execution already inside main(), constants and helpers definition-only at module level, nothing executes at import; numbers unchanged). run() encodes the all-pass pattern (v757 precedent). Original hecke_check32_probe.py docstring (verbatim): hecke_check32_probe -- HECKE.CARRIER_CHECK32.01: the mod-32 carrier congruence of the TFPT cusp channel. THE THEOREM CANDIDATE (frozen before running): f8(q) = eta(2 tau)^4 eta(4 tau)^4 = sum a_n q^n (the TFPT cusp channel; corpus anchor v535_hecke_from_geometry.py / HECKE.GEOM.01: a_3 = -4, a_5 = -2, a_7 = 24, a_11 = -44, a_13 = 22; exact cusp projector pi_cusp = (28 - T_3)/32) satisfies f8 == E_odd (mod 32), where E_odd(q) = sum_{n odd} sigma3(n) q^n = (E4(tau) - 9 E4(2tau) + 8 E4(4tau)) / 240. COROLLARY: a_p == 1 + p^3 (mod 32) for EVERY odd prime p, with the explicit decoder p == (a_p - 1)^3 (mod 32) (the cube map is a bijection on the 16 odd residues mod 32 -- finite census below). MODULARITY INPUT TYPING (honest, frozen): * f8 is weight-4 level-8 cuspidal: CORPUS-ANCHORED (v535 HECKE.GEOM.01, FENCE check "f8 = eta(2)^4 eta(4)^4, level 8"; eigenform with T_3 f8 = -4 f8 verified there and re-verified here via the Hecke grammar gate S5). * E_odd is the stated Eisenstein combination: the q-expansion identity against sigma3 is MACHINE-VERIFIED here directly to 10000 terms (S2). * The Sturm step itself ("two integral forms of weight k on Gamma_0(N) congruent mod m beyond k/12 * [SL2(Z):Gamma_0(N)] terms are congruent") is the ONE CITED classical ingredient (Sturm 1987); bound (4/12) * [SL2(Z):Gamma_0(8)] = (4/12) * 12 = 4. We verify the congruence to q^100000 -- 25000x the bound -- so the theorem-grade reading needs exactly this one cited theorem, everything else is machine-verified integer arithmetic. SECTIONS (predeclared): S0 eta-product build, EXACT integer arithmetic (pentagonal sparse series, P^4 via Kronecker-substitution big-int multiplication) to q^100000; integrality by construction; cross-check against an independent pure-dict O(n*sqrt n) build to q^2000 and against the corpus a_p table (v535). S1 E_odd identity: (E4 - 9 E4(2t) + 8 E4(4t))/240 == sum_{n odd} sigma3(n) q^n coefficient-wise to n = 10000 (exact). S2 STURM-PLUS: a_n == [E_odd]_n (mod 32) for ALL n <= 100000 (both series supported on odd n; even side is 0 == 0). S3 CENSUS: a_p == 1 + p^3 (mod 32) for ALL odd primes p < 10^5, zero failures required; decoder p == (a_p - 1)^3 (mod 32) for all tested primes; cube-map bijection census on the 16 odd residues. S4 MAXIMALITY / MUTATION: predeclared must-fail mod 64 at q^3: a_3 - (1 + 27) = -4 - 28 = -32, which is 0 mod 32 but NOT 0 mod 64 -- so 32 is the maximal 2-power. STRUCTURAL OBSERVATION (typed as observation, NOT derivation): 32 = 2^g_car (g_car = 5, axiom P2) = dim(S+ + S-) = 16 + 16 of the D5 spinor layer (v774 ARF.SPINORCOMPILER.01: S+_{D5} = Lambda^even C^5 = 1+5bar+10, 16-dim), and 32 = 28 - (-4) is the cusp projector denominator in pi_cusp = (28 - T_3)/32 (v535 N4a). S5 GRAMMAR: Hecke wellformedness on the computed coefficients -- a_{mn} = a_m a_n for all coprime pairs with mn <= 100000; a_{p^k} = a_p a_{p^{k-1}} - p^3 a_{p^{k-2}} for all p^k <= 100000; spot values a_9 = -11, a_15 = 8, a_25 = -121; derived mod-32 prime-power law a_{p^k} == sigma3(p^k) == sum_{j<=k} p^{3j} (mod 32), verified for all prime powers in range. S6 CONTROLS (must fire): C1 perturbed eta exponent g = q * prod(1-q^{2n})^4 (1-q^{4n})^3 (fractional eta prefactor dropped -- stated honestly): the census a'_p == 1 + p^3 (mod 32) must break immediately (first failing prime and failure fraction reported). C2 random integer sequences with matching growth |b_p| ~ p^{3/2}: per-prime pass probability must be ~ 1/32, i.e. detection (failure) rate ~ 31/32 = 96.875% -- quantified empirically as the checksum reading (seeded, 100 trials x 1228 primes). HARNESS AMENDMENTS AFTER FIRST RUN (data unchanged, recorded honestly): * S5 first draft applied the good-prime T_p recurrence at p = 2; but 2 | level 8, where the correct law is the ramified U_2 one, a_(2^k) = a_2^k = 0. Fixed to good primes + explicit U_2 check. * S6/C1 first draft predeclared "first failing prime = 3"; the mutant passes at p = 3 by a single mod-32 coincidence and first fails at p = 5, with failure fraction 0.917. The control requirement ("breaks immediately") is met; assertion relaxed to first-fail within the first two odd primes + fraction > 1/2. VERDICT ENUM (frozen): CHECK32-THEOREM : congruence verified far beyond Sturm + census clean (zero failures) + mutation fires + grammar clean + controls fire -- promotion-grade with the one cited Sturm ingredient typed. CHECK32-PARTIAL : some component degraded but no counterexample. CHECK32-FALSE : a counterexample -- reported exactly. Exploration only (experiments/tfpt-discovery/): no verification/, no ledger, no papers, no website surfaces touched. Lean companion: experiments/lean4-carrier-rigidity/TfptCarrier/Check32.lean (finite core kernel-checked: cube bijection, first-coefficient congruences as exact integer statements, mod-64 failure witness). """ from __future__ import annotations import random import time N_MAIN = 100_000 # q-range of the main build (a_n for n <= N_MAIN) N_EODD = 10_000 # range of the direct E_odd identity check (S1) N_XCHECK = 2_000 # range of the independent pure-dict rebuild (S0) N_MUTANT = 10_000 # q-range of the C1 mutant build MOD = 32 STURM_BOUND = 4 # (4/12) * [SL2(Z):Gamma_0(8)] = (4/12)*12 = 4 A_P_CORPUS = {3: -4, 5: -2, 7: 24, 11: -44, 13: 22} # v535 HECKE.GEOM.01 RNG_SEED = 20260805 N_RANDOM_TRIALS = 100 CHECKS = [] def check(label: str, ok: bool) -> bool: CHECKS.append((label, bool(ok))) print(f" [{'PASS' if ok else 'FAIL'}] {label}") return bool(ok) # ------------------------------------------------------------------ exact # polynomial arithmetic over Z via Kronecker substitution: evaluate at # x = 2^K, one big-int multiply, balanced-digit decode. Exact for # |product coefficients| < 2^(K-1) (asserted from Cauchy bounds). def _encode_nonneg(v, K): nb = K // 8 return int.from_bytes( b"".join(int(x).to_bytes(nb, "little") for x in v), "little") def kron_mul(a, b, n_out): """Exact product of integer coefficient lists a, b truncated to degree n_out (inclusive). Single big-int multiplication.""" ca = max((abs(x) for x in a), default=0) cb = max((abs(x) for x in b), default=0) bound = ca * cb * min(len(a), len(b)) K = 64 while bound >= (1 << (K - 1)): K += 64 ap = _encode_nonneg([x if x > 0 else 0 for x in a], K) an = _encode_nonneg([-x if x < 0 else 0 for x in a], K) bp = _encode_nonneg([x if x > 0 else 0 for x in b], K) bn = _encode_nonneg([-x if x < 0 else 0 for x in b], K) prod = (ap - an) * (bp - bn) neg = prod < 0 if neg: prod = -prod mask = (1 << K) - 1 half = 1 << (K - 1) out = [0] * (n_out + 1) for i in range(n_out + 1): if prod == 0: break d = prod & mask prod >>= K if d >= half: # balanced digit: negative coeff d -= (1 << K) prod += 1 out[i] = -d if neg else d return out def pentagonal_series(n_max): """prod_{n>=1} (1 - x^n) = sum_k (-1)^k x^{k(3k-1)/2}, truncated.""" out = [0] * (n_max + 1) out[0] = 1 k = 1 while True: g1 = k * (3 * k - 1) // 2 g2 = k * (3 * k + 1) // 2 if g1 > n_max and g2 > n_max: break s = -1 if k % 2 == 1 else 1 if g1 <= n_max: out[g1] += s if g2 <= n_max: out[g2] += s k += 1 return out def euler_pow(e, n_max): """prod (1 - x^n)^e exactly, e in {3, 4} here.""" P = pentagonal_series(n_max) P2 = kron_mul(P, P, n_max) if e == 2: return P2 if e == 3: return kron_mul(P2, P, n_max) if e == 4: return kron_mul(P2, P2, n_max) raise ValueError(e) def embed(series, d, n_max): """series(x) -> series(q^d) as a q-coefficient list.""" out = [0] * (n_max + 1) for i, c in enumerate(series): if i * d > n_max: break out[i * d] = c return out def build_f8(n_max, exp4=4): """q * prod(1-q^{2n})^4 * prod(1-q^{4n})^exp4 (exp4 = 3 is the C1 mutant; the dropped fractional eta prefactor is stated in the docstring).""" A = embed(euler_pow(4, n_max // 2), 2, n_max - 1) B = embed(euler_pow(exp4, n_max // 4), 4, n_max - 1) core = kron_mul(A, B, n_max - 1) return [0] + core # multiply by q def build_f8_dict_xcheck(n_max): """Independent slow exact rebuild (dict of sparse pentagonal factors multiplied pairwise, no Kronecker), for the S0 cross-check.""" def pent(d): out = {0: 1} k = 1 while d * k * (3 * k - 1) // 2 <= n_max: s = -1 if k % 2 == 1 else 1 for g in (k * (3 * k - 1) // 2, k * (3 * k + 1) // 2): if d * g <= n_max: out[d * g] = out.get(d * g, 0) + s k += 1 return out def dmul(a, b): out = {} for i, ci in a.items(): if ci == 0: continue for j, cj in b.items(): if i + j <= n_max: out[i + j] = out.get(i + j, 0) + ci * cj return out p2, p4 = pent(2), pent(4) acc = {0: 1} for _ in range(4): acc = dmul(acc, p2) for _ in range(4): acc = dmul(acc, p4) return [0] + [acc.get(n, 0) for n in range(n_max)] def sieve_primes(n_max): is_c = bytearray(n_max + 1) primes = [] for p in range(2, n_max + 1): if not is_c[p]: primes.append(p) for m in range(p * p, n_max + 1, p): is_c[m] = 1 return primes def sieve_sigma3(n_max): s = [0] * (n_max + 1) for d in range(1, n_max + 1): d3 = d * d * d for m in range(d, n_max + 1, d): s[m] += d3 return s # ================================================================== run def main(): t0 = time.time() print("hecke_check32_probe -- HECKE.CARRIER_CHECK32.01") print(f" range N = {N_MAIN}, modulus {MOD}, Sturm bound {STURM_BOUND}") # ------------------------------------------------------------- S0 print("S0 -- exact eta-product build") a = build_f8(N_MAIN) check("integrality: coefficients are Python ints by construction " "(pentagonal series, big-int Kronecker products, no floats)", all(isinstance(x, int) for x in a[:100])) check(f"corpus anchor (v535): a_p = {A_P_CORPUS} reproduced", all(a[p] == v for p, v in A_P_CORPUS.items())) check("normalisation: a_0 = 0, a_1 = 1; support on ODD n only " f"(checked all n <= {N_MAIN})", a[0] == 0 and a[1] == 1 and all(a[n] == 0 for n in range(0, N_MAIN + 1, 2))) xc = build_f8_dict_xcheck(N_XCHECK) check(f"independent pure-dict rebuild agrees to q^{N_XCHECK}", a[:N_XCHECK + 1] == xc[:N_XCHECK + 1]) print(f" a_3={a[3]}, a_5={a[5]}, a_7={a[7]}, a_9={a[9]}, " f"a_11={a[11]}, a_13={a[13]}, a_15={a[15]}, a_25={a[25]}") # ------------------------------------------------------------- S1 print("S1 -- E_odd Eisenstein identity (direct, exact)") sig3 = sieve_sigma3(N_MAIN) # E4(t) - 9 E4(2t) + 8 E4(4t), coefficient-wise over Z, then /240. ok_e = True first_bad = None for n in range(N_EODD + 1): c = (1 if n == 0 else 240 * sig3[n]) c += -9 * (1 if n == 0 else (240 * sig3[n // 2] if n % 2 == 0 else 0)) c += 8 * (1 if n == 0 else (240 * sig3[n // 4] if n % 4 == 0 else 0)) if c % 240 != 0: ok_e = False first_bad = n break e_odd_n = c // 240 want = sig3[n] if (n % 2 == 1) else 0 if e_odd_n != want: ok_e = False first_bad = n break check(f"(E4 - 9 E4(2t) + 8 E4(4t))/240 == sum_(n odd) sigma3(n) q^n " f"coefficient-wise for ALL n <= {N_EODD}" + ("" if ok_e else f" (FIRST BAD n = {first_bad})"), ok_e) # ------------------------------------------------------------- S2 print("S2 -- Sturm-plus congruence f8 == E_odd (mod 32)") bad = [n for n in range(1, N_MAIN + 1) if (a[n] - (sig3[n] if n % 2 == 1 else 0)) % MOD != 0] check(f"a_n == [E_odd]_n (mod 32) for ALL n <= {N_MAIN} " f"(= {N_MAIN // STURM_BOUND}x the Sturm bound {STURM_BOUND}; " f"failures: {len(bad)}" + (f", first at n = {bad[0]}" if bad else "") + ")", len(bad) == 0) check("typing: Sturm step = ONE cited classical theorem (Sturm 1987, " "bound (4/12)*[SL2:Gamma_0(8)] = (4/12)*12 = 4); f8 wt-4 lvl-8 " "cuspidal = corpus anchor v535; E_odd combination = machine-" "verified S1", STURM_BOUND == (4 * 12) // 12) # ------------------------------------------------------------- S3 print("S3 -- prime census + decoder bijection") primes = sieve_primes(N_MAIN - 1) odd_primes = [p for p in primes if p % 2 == 1] fails = [(p, a[p], (1 + p ** 3) % MOD) for p in odd_primes if (a[p] - (1 + p ** 3)) % MOD != 0] check(f"census: a_p == 1 + p^3 (mod 32) for ALL {len(odd_primes)} odd " f"primes p < 10^5 (failures: {len(fails)}" + (f", first: {fails[0]}" if fails else "") + ")", len(fails) == 0) odd_res = [r for r in range(MOD) if r % 2 == 1] cube = {r: pow(r, 3, MOD) for r in odd_res} check("cube map census: r -> r^3 is a BIJECTION on the 16 odd " "residues mod 32 (image = all 16, no collision)", sorted(cube.values()) == odd_res) dec_fails = [p for p in odd_primes if pow((a[p] - 1) % MOD, 3, MOD) != p % MOD] check("decoder: p == (a_p - 1)^3 (mod 32) for ALL tested primes " f"(failures: {len(dec_fails)})", len(dec_fails) == 0) # ------------------------------------------------------------- S4 print("S4 -- maximality / mutation (predeclared must-fail mod 64)") d3 = a[3] - (1 + 3 ** 3) check(f"mod-64 failure AT q^3: a_3 - (1+27) = {a[3]} - 28 = {d3}; " "== 0 (mod 32) but != 0 (mod 64) -- 32 is the maximal 2-power", d3 == -32 and d3 % 32 == 0 and d3 % 64 != 0) n64 = sum(1 for p in odd_primes[:1000] if (a[p] - (1 + p ** 3)) % 64 != 0) print(f" mod-64 census on first 1000 odd primes: " f"{n64}/1000 fail (mod 32: 0/1000)") check("mod-64 census: failures exist (first at p = 3) so the " "congruence does NOT lift to 64", n64 > 0) check("STRUCTURAL OBSERVATION (typed as observation, not derivation): " "32 = 2^g_car (g_car = 5, P2) = dim(S+ + S-) = 16+16 (v774) " "= 28 - (-4) = pi_cusp denominator (v535 N4a)", 2 ** 5 == 32 and 16 + 16 == 32 and 28 - (-4) == 32) # ------------------------------------------------------------- S5 print("S5 -- Hecke grammar wellformedness gate") check("spot values: a_9 = -11, a_15 = 8, a_25 = -121", a[9] == -11 and a[15] == 8 and a[25] == -121) mult_bad = 0 n_mult = 0 for m in range(2, 317): for n in range(m + 1, N_MAIN // m + 1): from math import gcd if gcd(m, n) == 1: n_mult += 1 if a[m * n] != a[m] * a[n]: mult_bad += 1 check(f"multiplicativity a_(mn) = a_m a_n on ALL {n_mult} coprime " f"pairs with 2 <= m < n, mn <= {N_MAIN} (failures: {mult_bad})", mult_bad == 0) # p = 2 divides the level 8: the good-prime T_p recurrence does NOT # apply there; the correct law is the U_2 (ramified) one, # a_(2^k) = a_2^k = 0 -- trivially consistent with odd support. check("ramified prime p = 2 (2 | level 8): U_2 law a_(2^k) = a_2^k " "= 0 for all 2^k <= N (odd support)", all(a[1 << k] == 0 for k in range(1, 17))) pp_bad = 0 n_pp = 0 pp32_bad = 0 for p in primes: if p == 2: continue # good primes only (p coprime to 8) pk, prev, prev2 = p * p, a[p], 1 while pk <= N_MAIN: n_pp += 1 want = a[p] * prev - p ** 3 * prev2 if a[pk] != want: pp_bad += 1 if (a[pk] - sig3[pk]) % MOD != 0: pp32_bad += 1 prev2, prev = prev, a[pk] pk *= p check(f"good-prime recurrence a_(p^k) = a_p a_(p^(k-1)) - p^3 " f"a_(p^(k-2)) on all {n_pp} odd prime powers <= {N_MAIN} " f"(failures: {pp_bad})", pp_bad == 0) check("derived mod-32 prime-power law: a_(p^k) == sigma3(p^k) " "= sum_(j<=k) p^(3j) (mod 32) for all odd prime powers in " f"range (failures: {pp32_bad})", pp32_bad == 0) # ------------------------------------------------------------- S6 print("S6 -- controls (must fire)") g = build_f8(N_MUTANT, exp4=3) mut_primes = [p for p in sieve_primes(N_MUTANT - 1) if p % 2 == 1] mut_fails = [p for p in mut_primes if (g[p] - (1 + p ** 3)) % MOD != 0] first_mut = mut_fails[0] if mut_fails else None frac = len(mut_fails) / len(mut_primes) # Honest note: at p = 3 the mutant passes BY CHANCE (a single mod-32 # coincidence, prob ~ 1/32 per prime); the census as a whole breaks # immediately -- first failure within the first two odd primes and # an overwhelming failure fraction. check(f"C1 mutant eta(2t)^4 eta(4t)^3: census breaks immediately -- " f"first failing prime p = {first_mut} (p = 3 passes by a " f"1/32-type coincidence), failure fraction " f"{len(mut_fails)}/{len(mut_primes)} = {frac:.3f}", first_mut is not None and first_mut <= 5 and frac > 0.5) rng = random.Random(RNG_SEED) hit_rates = [] for _ in range(N_RANDOM_TRIALS): hits = 0 for p in mut_primes: m = int(p ** 1.5) * 2 + 32 b_p = rng.randint(-m, m) if (b_p - (1 + p ** 3)) % MOD == 0: hits += 1 hit_rates.append(hits / len(mut_primes)) mean_hit = sum(hit_rates) / len(hit_rates) check(f"C2 random growth-matched sequences (seed {RNG_SEED}, " f"{N_RANDOM_TRIALS} trials x {len(mut_primes)} primes): mean " f"per-prime pass rate {mean_hit:.4f} ~ 1/32 = {1/32:.4f}; " f"detection rate {1 - mean_hit:.4f} ~ 31/32 = {31/32:.4f}", abs(mean_hit - 1 / 32) < 0.01) # ---------------------------------------------------------- verdict n_pass = sum(1 for _, ok in CHECKS if ok) n_all = len(CHECKS) if n_pass == n_all: verdict = "CHECK32-THEOREM" elif any((a[n] - (sig3[n] if n % 2 else 0)) % MOD != 0 for n in range(1, N_MAIN + 1)): verdict = "CHECK32-FALSE" else: verdict = "CHECK32-PARTIAL" dt = time.time() - t0 print(f"CHECKS: {n_pass}/{n_all} passed; walltime {dt:.1f}s") print(f"VERDICT: {verdict}") # coefficient table for the Lean companion (provenance) odd_head = [(n, a[n], sig3[n]) for n in range(1, 64, 2)] print("LEAN TABLE (n, a_n, sigma3(n)) for odd n <= 63:") print(" " + repr(odd_head)) return 0 if verdict == "CHECK32-THEOREM" else 1 def run(): """run_all entry point (v757 precedent): expected pattern 20/20 with verdict CHECK32-THEOREM (main() returns 0 only on that verdict; any PARTIAL or FALSE outcome breaks the suite).""" rc = main() fails = [n for (n, ok) in CHECKS if not ok] n_pass = len(CHECKS) - len(fails) ok = (rc == 0 and not fails and len(CHECKS) == 20) print("\n[%s] PATTERN GATE: expected 20/20 CHECK32-THEOREM; got " "%d/%d, rc = %d -- fails: %s" % ("PASS" if ok else "FAIL", n_pass, len(CHECKS), rc, fails or "none")) print("\nADJUDICATION: %s -- CHECK32-THEOREM: f8 == E_odd (mod 32) to " "q^100000 (25000x the Sturm bound 4; Sturm 1987 is the one cited " "classical ingredient); a_p == 1 + p^3 (mod 32) on all 9591 odd " "primes p < 10^5 with the cube-map decoder bijective on the 16 " "odd residues; mod-64 fails at q^3 (252/1000 prime census); " "controls fire (mutant 1126/1228 = 91.7%%, random detection " "~31/32). Lean kernel companion Check32.lean. No marker move, " "NO RH claim." % ("PASS" if ok else "FAIL")) return 0 if ok else 1 if __name__ == "__main__": raise SystemExit(run())