Follow the source behind the result.
Search the paper sections, open their original context and follow the checks they actually cite. The knowledge atlas explains the result; this library locates its source.
v875_shell_global_lean.py
verification/v875_shell_global_lean.py
This is a registered verification module. Read its original code and the paper sections that cite it, then follow the linked claim to its present classification.
Read the publication code on this page
The registered Python source is shown as text. Displaying it does not execute the code.
#!/usr/bin/env python3
# -*- coding: utf-8 -*-
r"""v875 -- E8.SHELL.GLOBAL.01 + the GaussianShells Lean skeleton: THE GLOBAL SHELL THEOREM (15/15, SHELL-GLOBAL-THEOREM) -- the v857 census law "the nontrivial Walsh coefficient of the Gaussian E8 shell census is -1/15 of the full theta on odd shells" is UPGRADED FROM A FINITE CENSUS (n <= 16500) TO A PROOF FOR ALL SHELLS. THE THEOREM: on V = L/(1+i)L of the Gaussian E8, for EVERY shell n >= 1: Theta_v(n) = (Theta_L(n) - Theta_0(n))/15 for all v != 0 (equidistribution, division exact), Thetahat_u(n) = 16(16 1_{2|n} sigma_3(n/2) - sigma_3(n)) for every nontrivial character u, and at every ODD n: Thetahat_u(n) = -16 sigma_3(n), i.e. Thetahat_u(n)/Theta_L(n) = -1/15 EXACTLY. THE THREE INPUTS, each warded: (i) TRANSITIVITY -- the G31 class action on the 15 nonzero cosets is generated by the 60 symplectic transvections, induces Sp(4,2) (order 720), is TRANSITIVE, and is IDENTICAL to the shell-module class action (coordination verified on generators): every class has the SAME shell count at every level; (ii) DOUBLING -- (I+J)^T(I+J) = 2I and (1-J)/2 inverts (1+i) on L: Theta_0(2m) = Theta_L(m), Theta_0(odd) = 0 (the (1+i) rescaling, exact from 2 = -i(1+i)^2); (iii) THE THETA IDENTITY -- Theta_L(n) = 240 sigma_3(n) (classical Eisenstein E4; verified to n = 24 directly and via the v857 packet glue identity to n = 16500). The census range is RETAINED as the exact ward (matched everywhere, odd AND even). CONTROLS: a non-transitive subgroup <T_1> (11 orbits) admits an explicit invariant NON-uniform census with Walsh multiset {-48 x4, -16 x7, +16 x4} -- the -1/15 law breaks, transitivity is load-bearing; the even-shell formula differs correctly (7/135 at n = 2, NOT -1/15: the law is the odd-shell statement only). THE LEAN SKELETON: TfptCarrier/GaussianShells.lean kernel-checks the CONSEQUENCE CHAIN (7 theorems from the named hypothesis bundle ShellSystem: exactness of the /15 division, the shell decomposition, the Walsh formula 15 Thetahat_u = 16 Theta_0 - Theta_L, the odd-shell theorem Thetahat_u(2m+1) = -16 sigma_3(2m+1) with the exact-ratio form 15 Thetahat_u(2m+1) = -Theta_L(2m+1), and the even-shell formula) -- the house discipline: the arithmetic consequence chain is kernel-checked, the finite/structural inputs (H1) Sp(4,2)-transitivity, (H2) (1+i)-doubling, (H3) Theta_L = 240 sigma_3 stay NAMED hypotheses with their verification provenance typed on each field, so the global statement can never hide a gap between the two; every Lean statement is an exact integer identity, no division appears. ONE module from one probe (re-executed verbatim, embedded BYTE-EXACT, ~3 s) plus 4 Lean skeleton checks. This REPLACES the finite-census argument behind the v857 value theorem; the -1/15 message eigenvalue of the Gaussian code (v817/v857) now rests on a theorem for ALL odd shells. NO physics claim beyond the audit statements. Python-only per GATE.WOLFRAM.02 (integer arithmetic; the Wolfram mirror carries the census-level identities via v857).
PROVENANCE: probe frozen + SHA-hashed before first run (FROZEN_SPEC SHA-256
gated below); executed 2026-08-08 evening, re-executed verbatim at this
promotion in an isolated namespace with the byte-equality provenance ward.
Lean: lake build green (3418 jobs), no sorry, no native_decide, axioms
propext/Classical.choice/Quot.sound on all 7 GaussianShells theorems,
lean_manifest at 90 files. NO RH claim.
"""
import contextlib
import io
import os
import re
import sys
import time
import types
_HERE = os.path.dirname(os.path.abspath(__file__))
if _HERE not in sys.path:
sys.path.insert(0, _HERE)
EXPECT_SHA_SHELL = ("a4b2f6d953af356f3989b61d5e3f213b7612f559"
"1bbec8b37a939b040399ab0b")
# ------------- frozen probe source (embedded BYTE-EXACT, raw string)
_SRC_SHELL = r'''
#!/usr/bin/env python3
# -*- coding: utf-8 -*-
r"""gaussian_shell_global_probe -- E8.GAUSSIAN.SHELL.GLOBAL.01 (phase 1
of the 2026-08-08 evening plan): the GLOBAL GAUSSIAN SHELL THEOREM --
the finite census (v833/v844/v857: equidistribution measured to level
16, the -1/15 value theorem measured to 16500) is upgraded to ALL
shells by three verified structural inputs: (i) the deployed
G31 -> Sp(4,2) class action is by symplectic TRANSVECTIONS and is
transitive on the 15 nonzero classes of V = L/(1+i)L, and it is the
SAME class action used in the shell modules; (ii) multiplication by
(1+i) doubles the norm (J antisymmetry), so Theta_0(2m) = Theta_L(m)
and Theta_0(odd) = 0; (iii) Theta_L(n) = 240 sigma_3(n) (classical E8
theta = 240 E4-coefficients; CITED + verified on the computed range).
Consequence, for ALL n: Theta_v(n) = (Theta_L(n) - Theta_0(n))/15 for
every v != 0 and Thetahat_u(n) = (16 Theta_0(n) - Theta_L(n))/15 =
16 (16 1_{2|n} sigma_3(n/2) - sigma_3(n)); for ODD n: Thetahat_u(n) =
-16 sigma_3(n) and Thetahat_u/Theta_L = -1/15 EXACTLY -- a theorem for
all odd n, replacing the n <= 16500 census.
FROZEN CLAIMS (2026-08-08 evening, frozen + SHA-hashed before first run):
S1 STRUCTURAL INPUT (i) -- THE ACTION (exact integer arithmetic):
S1.1 rebuild: 240 doubled std-model E8 roots (norm 8); the J
matrix satisfies J^T = -J, J^2 = -I, (I-J)(I+J) = 2I and
det(I+J) = 16 = |L/(1+i)L| EXACTLY.
S1.2 THE LATTICE IS THE ROOT SPAN: the HNF of the 240 roots has
|det| = 256; the mod-4 membership residues of L number 256, so
[L : 4Z^8] = 256 and det(L) = 4^8/256 = 256; every root passes
the membership test => root span = L EXACTLY; and 4 e_k in
(1+i)L for all 8 unit directions => classes are mod-4 data (the
DP ground).
S1.3 THE CLASSES, TWO LABELINGS (the coordination check, part 1):
the shell-module labeling (mod-4 residue reps, DP path) and the
G31-module labeling (greedy on the roots, v858 path) give the
SAME partition of the 240 roots: 15 nonzero classes x 16, zero
class EMPTY.
S1.4 THE SYMPLECTIC FORM: b(x,y) = ((x.y)/4 + (x.Jy)/4) mod 2 is
well-defined on V x V (class-constant over all 240 roots vs all
16 reps), F2-bilinear (all 16^3 additivity triples), alternating
(b(x,x) = 0, forced by |x|^2 in 8Z), symmetric, and NONDEGENERATE
(rank 4 over F2).
S1.5 THE 60 GENERATORS ARE SYMPLECTIC TRANSVECTIONS (the
coordination check, part 2): each v858 reflection R_v satisfies
(4M)^T (4M) = 16 I (isometry) and (4M) J = J (4M) (complex-
linear), permutes the 240 roots (hence preserves L = root span),
and its induced class map IS the symplectic transvection
T_{vbar}: x -> x + b(x, vbar) vbar for vbar = class(v) -- and the
two action paths (root-permutation transport vs matrix-on-reps
transport) COINCIDE on every generator.
S1.6 TRANSITIVITY: the closure of the 60 induced transvections
has order 720 = |Sp(4,2)|, every generator preserves b, the
action on the 15 nonzero classes is TRANSITIVE (one orbit of
size 15), and the 60 root lines cover all 15 classes at 4 lines
per class (v858 S2.3 reproduced).
S2 STRUCTURAL INPUT (ii) -- NORM DOUBLING (exact):
S2.1 (I+J)^T (I+J) = 2I EXACTLY (x.Jx = 0 from antisymmetry), so
|(1+i)x|^2 = 2|x|^2 for EVERY x; the deployed membership test is
the inverse bijection ((1-J)/2)(1+i) = I from (I-J)(I+J) = 2I;
level-2 witness: the 240 vectors (1+i)r (r a root) are distinct,
norm 16, ALL in the zero class.
S2.2 RAMIFICATION on the DP range: Theta_0(n) = 0 for EVERY odd
n <= 24 (one-line proof: x = (1+i)y => |x|^2 = 2|y|^2 with
|y|^2 in 8Z => level even) and Theta_0(2m) = 240 sigma_3(m) =
Theta_L(m) for every 2m <= 24 (the doubling bijection), with
Theta_0(2) = 240 matching the witness.
S3 STRUCTURAL INPUT (iii) -- THE THETA IDENTITY (exact int DP over
the 256 mod-4 residues, levels |x|^2 = 8n, n <= NCAP = 24):
S3.1 DP gates: residue fibers all 256; level-1 class census
equals the root census (0; 16 x15).
S3.2 Theta_L(n) = sum_v Theta_v(n) = 240 sigma_3(n) for EVERY
n <= 24 against an independent sigma_3 sieve (the classical E8
theta formula, CITED as Eisenstein E4 and verified here on the
computed range).
S4 THE DERIVED GLOBAL FORMULAS + THE WARD:
S4.1 Theta_v(n) = (Theta_L(n) - Theta_0(n))/15 EXACTLY for every
v != 0 and every n <= 24 (equidistribution is now a COROLLARY:
the shell counting function is invariant under the induced
Sp-action -- each generator is a norm-preserving lattice
bijection transporting class v to gbar(v) -- and the action is
transitive on the 15 nonzero classes; 15-divisibility exact).
S4.2 Thetahat_u(n) = (16 Theta_0(n) - Theta_L(n))/15 =
16 (16 1_{2|n} sigma_3(n/2) - sigma_3(n)) EXACTLY for every
u != 0 and every n <= 24.
S4.3 THE GLOBAL WARD to 16500 (v817/v857 packet machinery rebuilt
read-only, int64 with the deployed exactness certificates):
heads (Th0..Th3)(1) = (52,64,60,64); glue identity
Th0+Th1+Th2+Th3 = 240 sigma_3(n) for ALL n <= 16500; Th1 = Th3;
the packet numerator (Th0-Th1+Th2-Th3)(n) EQUALS the derived
closed form 16 (16 1_{2|n} sigma_3(n/2) - sigma_3(n)) for EVERY
n <= 16500 (odd AND even -- the deployed census range matches
the theorem everywhere), and equals the DP Thetahat_u(n) on
n <= 24; hence for ODD n: Thetahat_u(n) = -16 sigma_3(n) and
Thetahat_u/Theta_L = -1/15 EXACTLY -- now a THEOREM for ALL odd
n, the n <= 16500 census replaced by proof.
C CONTROLS (each must fire; exact):
C1 A WRONG ACTION BREAKS EQUIDISTRIBUTION: the non-transitive
subgroup H = <T_1> (one transvection) has 11 orbits on the 15
nonzero classes (7 fixed + 4 swaps); an explicit H-invariant
NON-uniform census (move 16 roots between two H-fixed
classes: values 32 and 0) is constructed -- its Walsh values
on u != 0 are the multiset {-48: 4, -16: 7, +16: 4}, NOT
uniform, and the -1/15 law breaks; a full-group generator
moves that census (measured) -- transitivity is the
load-bearing input, H-invariance alone does not force
uniformity.
C2 THE EVEN-SHELL FORMULA DIFFERS CORRECTLY: Thetahat_u(2m) =
16 (16 sigma_3(m) - sigma_3(2m)) (verified in BOTH
machineries via S4.2/S4.3); at n = 2: Thetahat = 112,
Theta_L = 2160, ratio 112/2160 = 7/135 != -1/15 (typed:
the -1/15 law is the ODD-shell statement only).
KILLS (any one fires => typed failure):
K1 rebuild / lattice / J identities break -> LATTICE-BROKEN
K2 action / coordination / transitivity break -> ACTION-MISMATCH
K3 doubling / ramification breaks -> DOUBLING-BROKEN
K4 DP gates / theta identity break -> THETA-MISMATCH
K5 a derived global formula / ward breaks -> FORMULA-BROKEN
K6 a control does not fire -> CONTROL-DEAD
VERDICT (frozen enum): SHELL-GLOBAL-THEOREM / LATTICE-BROKEN /
ACTION-MISMATCH / DOUBLING-BROKEN / THETA-MISMATCH / FORMULA-BROKEN /
CONTROL-DEAD.
FIREWALL: experiments/ probe; EXPLORATION ONLY -- writes nothing but
stdout; no verification/, paper, ledger, changelog or website surface;
no .md, no commits. Exact integer/Fraction arithmetic in every
decision (numpy int64 packet layer uses the deployed divisibility
certificates); no floats, no RNG, no fits. NO physics claim, NO RH
claim. Runtime cap: minutes.
Sources (read-only, machinery rebuilt inline): verification/
v833_gaussian_ramification_ladder.py + v844_message_doily_rank.py
(census, class machinery), v857_simplex_fourier_winding.py (Walsh law,
theta DP, packet thetas, equidistribution to 16, value theorem to
16500), v858_g31_clock_alphabet.py (60 reflections, lines per class),
v634_st31_structure.py (G31 = (Z4 o 2^{1+4}).Sp4(2)), v817 (packet
machinery), Eisenstein E4 / classical E8 theta (Theta_L = 240 sigma_3,
citation).
Run:
experiments/tfpt-discovery/.venv/bin/python \
experiments/tfpt-discovery/gaussian_shell_global_probe.py
"""
import hashlib
import itertools
import time
from collections import Counter
from fractions import Fraction as Fr
import numpy as np
T0 = time.time()
CHECKS = []
KILLS = []
NCAP = 24 # DP shell levels (|x|^2 = 8n), exact python ints
N_THETA = 16500 # packet reach (v817/v857 value)
def check(name, ok, detail="", kill=None):
CHECKS.append((name, bool(ok)))
if kill and not ok:
KILLS.append(kill)
print(" [%s] %s%s" % ("PASS" if ok else "FAIL", name,
(" -- " + detail) if detail else ""), flush=True)
return bool(ok)
def section(title):
print("\n== %s == (t=%.1fs)" % (title, time.time() - T0), flush=True)
print("=" * 74)
print("E8.GAUSSIAN.SHELL.GLOBAL.01 -- transitivity + doubling + theta")
print("identity => Theta_v(n) = (Theta_L - Theta_0)/15 for ALL shells;")
print("Thetahat_u(odd)/Theta_L = -1/15 as a THEOREM (census replaced)")
print("=" * 74)
print("FROZEN_SPEC SHA-256: %s"
% hashlib.sha256(__doc__.encode("utf-8")).hexdigest())
# ======================================================================
section("S1: structural input (i) -- the G31 -> Sp(4,2) class action")
# ======================================================================
STD = []
for v in itertools.product(range(-1, 2), repeat=8):
if sum(a * a for a in v) == 2 and sum(v) % 2 == 0:
STD.append(tuple(2 * a for a in v))
for yb in itertools.product((0, -1), repeat=8):
v = tuple(2 * a + 1 for a in yb)
if sum(a * a for a in v) == 8 and sum(v) % 4 == 0:
STD.append(v)
STD = sorted(STD)
J = np.zeros((8, 8), dtype=np.int64)
for k in range(4):
J[2 * k, 2 * k + 1] = -1
J[2 * k + 1, 2 * k] = 1
I8 = np.eye(8, dtype=np.int64)
check("S1.1 240 roots (norm 8); J^T = -J; J^2 = -I; (I-J)(I+J) = 2I; "
"det(I+J) = %d == 16 = |L/(1+i)L|"
% round(np.linalg.det((I8 + J).astype(float))),
len(STD) == 240 and len(set(STD)) == 240
and all(sum(x * x for x in r) == 8 for r in STD)
and np.array_equal(J.T, -J)
and np.array_equal(J @ J, -I8)
and np.array_equal((I8 - J) @ (I8 + J), 2 * I8)
and round(np.linalg.det((I8 + J).astype(float))) == 16, kill="K1")
def in_L_std(v):
if all(x % 2 == 0 for x in v):
return sum(x // 2 for x in v) % 2 == 0
if all(x % 2 == 1 for x in v):
return sum(v) % 4 == 0
return False
def in_pi2L_std(v):
w = [0] * 8
for k in range(4):
w[2 * k] = v[2 * k] + v[2 * k + 1]
w[2 * k + 1] = v[2 * k + 1] - v[2 * k]
if any(x % 2 for x in w):
return False
return in_L_std([x // 2 for x in w])
def ext_gcd(a, b):
old_r, r = a, b
old_s, s = 1, 0
old_t, t = 0, 1
while r:
qt = old_r // r
old_r, r = r, old_r - qt * r
old_s, s = s, old_s - qt * s
old_t, t = t, old_t - qt * t
return old_r, old_s, old_t
def hnf_det(rows):
"""|det| of the lattice generated by integer rows (greedy upper-
triangular HNF fold; exact)."""
H = [[0] * 8 for _ in range(8)]
for r in rows:
v = list(r)
for i in range(8):
if v is None or v[i] == 0:
continue
if H[i][i] == 0:
if v[i] < 0:
v = [-x for x in v]
H[i] = v
v = None
else:
g, x0, y0 = ext_gcd(H[i][i], v[i])
new = [x0 * H[i][j] + y0 * v[j] for j in range(8)]
v = [(H[i][i] // g) * v[j] - (v[i] // g) * H[i][j]
for j in range(8)]
H[i] = new
det = 1
for i in range(8):
det *= H[i][i]
return abs(det)
det_root_span = hnf_det(STD)
residues = []
for par in ((0, 2), (1, 3)):
for rho in itertools.product(par, repeat=8):
if sum(rho) % 4 == 0:
residues.append(rho)
four_ek = all(in_pi2L_std(tuple(4 if j == k else 0 for j in range(8)))
for k in range(8))
check("S1.2 lattice = root span: HNF |det| = %d == 256; membership "
"residues mod 4: %d == 256 => det(L) = 4^8/256 = 256; every "
"root in L: %s; 4 e_k in (1+i)L for all k: %s (classes are "
"mod-4 data)"
% (det_root_span, len(residues),
all(in_L_std(r) for r in STD), four_ek),
det_root_span == 256 and len(residues) == 256
and all(in_L_std(r) for r in STD) and four_ek, kill="K1")
# ---- two labelings: shell path (mod-4 residue reps) vs G31 path (roots)
res_reps = []
res_label = {}
for rho in sorted(residues):
for li, rep in enumerate(res_reps):
if in_pi2L_std(tuple(a - b for a, b in zip(rho, rep))):
res_label[rho] = li
break
else:
res_label[rho] = len(res_reps)
res_reps.append(rho)
def label_shell(x):
return res_label[tuple(a % 4 for a in x)]
root_reps = []
root_label = {}
for r in STD:
for li, rep in enumerate(root_reps):
if in_pi2L_std(tuple(a - b for a, b in zip(r, rep))):
root_label[r] = li
break
else:
root_label[r] = len(root_reps)
root_reps.append(r)
part_shell = {}
part_g31 = {}
for r in STD:
part_shell.setdefault(label_shell(r), set()).add(r)
part_g31.setdefault(root_label[r], set()).add(r)
same_partition = ({frozenset(s) for s in part_shell.values()}
== {frozenset(s) for s in part_g31.values()})
zero_shell = res_label[(0,) * 8]
census_g31 = sorted(Counter(root_label.values()).values())
check("S1.3 coordination part 1: shell-module labeling (16 residue "
"classes, zero class = residue 0) and G31-module labeling (%d "
"root classes) give the SAME partition: %s; census 15 x 16, "
"zero class EMPTY (no root labels as residue-zero: %s)"
% (len(root_reps), same_partition,
all(label_shell(r) != zero_shell for r in STD)),
len(res_reps) == 16 and len(root_reps) == 15 and same_partition
and census_g31 == [16] * 15
and all(label_shell(r) != zero_shell for r in STD), kill="K2")
# canonical 16-class indexing: 0 = zero class, 1..15 = root classes
ZERO = (0,) * 8
REPS16 = [ZERO] + list(root_reps)
def lab16(x):
hits = [k for k in range(16)
if in_pi2L_std(tuple(a - b for a, b in zip(x, REPS16[k])))]
assert len(hits) == 1
return hits[0]
def b_raw(x, yv):
d = sum(a * c for a, c in zip(x, yv))
jy = []
for k in range(4):
jy.append(-yv[2 * k + 1])
jy.append(yv[2 * k])
dj = sum(a * c for a, c in zip(x, jy))
assert d % 4 == 0 and dj % 4 == 0
return (d // 4 + dj // 4) % 2
B = [[b_raw(REPS16[a], REPS16[c]) for c in range(16)] for a in range(16)]
ADD = [[None] * 16 for _ in range(16)]
for a in range(16):
for c in range(16):
ADD[a][c] = lab16(tuple(x + z
for x, z in zip(REPS16[a], REPS16[c])))
well_def = all(b_raw(r, REPS16[c]) == B[lab16(r)][c]
for r in STD for c in range(16))
bilinear = all(B[ADD[a][c]][d] == (B[a][d] + B[c][d]) % 2
for a in range(16) for c in range(16) for d in range(16))
alt = all(B[a][a] == 0 for a in range(16))
sym = all(B[a][c] == B[c][a] for a in range(16) for c in range(16))
rows_bits = [sum(B[a][c] << c for c in range(16)) for a in range(16)]
rank = 0
pivots = []
for rb in rows_bits:
cur = rb
for p in pivots:
cur = min(cur, cur ^ p)
if cur:
pivots.append(cur)
rank += 1
check("S1.4 symplectic form b = ((x.y)/4 + (x.Jy)/4) mod 2: well-"
"defined on classes (240 x 16): %s; F2-bilinear (16^3): %s; "
"alternating: %s; symmetric: %s; rank over F2 = %d == 4 "
"(nondegenerate)" % (well_def, bilinear, alt, sym, rank),
well_def and bilinear and alt and sym and rank == 4, kill="K2")
# ---- the 60 reflections (v858 machinery) and their induced class maps
ridx = {r: i for i, r in enumerate(STD)}
Jvec = {}
for r in STD + [ZERO]:
out = []
for k in range(4):
out.append(-r[2 * k + 1])
out.append(r[2 * k])
Jvec[r] = tuple(out)
line_of = {}
line_reps = []
for r in STD:
if r in line_of:
continue
orb = [r]
cur = r
for _ in range(3):
cur = Jvec[cur]
orb.append(cur)
for x in orb:
line_of[x] = len(line_reps)
line_reps.append(r)
def refl_apply(vroot, x):
"""complex reflection in the Gaussian line of vroot, exact ints."""
w = Jvec[vroot]
d = sum(a * c for a, c in zip(x, vroot))
dj = sum(a * c for a, c in zip(x, w))
assert d % 4 == 0 and dj % 4 == 0
re, im = d // 4, dj // 4
return tuple(x[i] - re * vroot[i] - im * w[i] for i in range(8))
ok_matrix = True
ok_perm = True
ok_transvec = True
ok_coincide = True
induced_maps = []
for a in range(60):
vroot = line_reps[a]
varr = np.array(vroot, dtype=np.int64)
warr = J @ varr
M4 = 4 * I8 - np.outer(varr, varr) - np.outer(warr, warr)
if not np.array_equal(M4.T @ M4, 16 * I8):
ok_matrix = False
if not np.array_equal(M4 @ J, J @ M4):
ok_matrix = False
imgs = [refl_apply(vroot, r) for r in STD]
if sorted(imgs) != STD:
ok_perm = False
vbar = lab16(vroot)
gbar = tuple(lab16(refl_apply(vroot, REPS16[k])) for k in range(16))
pred = tuple(ADD[k][vbar] if B[k][vbar] == 1 else k
for k in range(16))
if gbar != pred:
ok_transvec = False
# coincidence of the two action paths on every root
for r, im_r in zip(STD, imgs):
if lab16(im_r) != gbar[lab16(r)]:
ok_coincide = False
break
induced_maps.append(gbar)
check("S1.5 coordination part 2 (60 generators): (4M)^T(4M) = 16I and "
"(4M)J = J(4M): %s; each permutes the 240 roots (preserves L = "
"root span): %s; induced class map == symplectic transvection "
"T_vbar: %s; root-permutation path == matrix-on-reps path on "
"every generator: %s"
% (ok_matrix, ok_perm, ok_transvec, ok_coincide),
ok_matrix and ok_perm and ok_transvec and ok_coincide, kill="K2")
IDMAP = tuple(range(16))
pool = {IDMAP}
frontier = [IDMAP]
while frontier:
nxt = []
for p in frontier:
for g in induced_maps:
qm = tuple(g[p[k]] for k in range(16))
if qm not in pool:
pool.add(qm)
nxt.append(qm)
frontier = nxt
orbit = {1}
frontier = [1]
while frontier:
x = frontier.pop()
for g in induced_maps:
if g[x] not in orbit:
orbit.add(g[x])
frontier.append(g[x])
gens_symp = all(B[g[a]][g[c]] == B[a][c]
for g in induced_maps
for a in range(16) for c in range(16))
lines_per_class = Counter(lab16(line_reps[a]) for a in range(60))
check("S1.6 TRANSITIVITY: closure order %d == 720 = |Sp(4,2)|; all 60 "
"induced generators preserve b: %s; orbit of a nonzero class "
"has size %d == 15 (ONE orbit); 60 lines cover all 15 classes "
"at %s per class"
% (len(pool), gens_symp, len(orbit),
sorted(set(lines_per_class.values()))),
len(pool) == 720 and gens_symp and len(orbit) == 15
and sorted(lines_per_class.values()) == [4] * 15, kill="K2")
# ======================================================================
section("S2: structural input (ii) -- norm doubling by (1+i)")
# ======================================================================
doubling_matrix = np.array_equal((I8 + J).T @ (I8 + J), 2 * I8)
pi_roots = [tuple(r[i] + Jvec[r][i] for i in range(8)) for r in STD]
witness = (len(set(pi_roots)) == 240
and all(sum(x * x for x in p) == 16 for p in pi_roots)
and all(lab16(p) == 0 for p in pi_roots))
check("S2.1 (I+J)^T(I+J) = 2I EXACT => |(1+i)x|^2 = 2|x|^2 for every "
"x; inverse bijection ((1-J)/2)(1+i) = I (S1.1 identity); level-"
"2 witness: 240 distinct vectors (1+i)r, norm 16, ALL class 0: "
"%s" % witness,
doubling_matrix and witness, kill="K3")
# ======================================================================
section("S3: structural input (iii) -- theta identity via mod-4 DP")
# ======================================================================
EMAX = 8 * NCAP
DIGIT = {}
for d in range(4):
poly = {}
for zz in range(-16, 17):
e = (d + 4 * zz) ** 2
if e <= EMAX:
poly[e] = poly.get(e, 0) + 1
DIGIT[d] = poly
def poly_mul(a, b):
out = {}
for ea, ca in a.items():
for eb, cb in b.items():
e = ea + eb
if e <= EMAX:
out[e] = out.get(e, 0) + ca * cb
return out
THETA = [[0] * (NCAP + 1) for _ in range(16)]
fibers = [0] * 16
for rho in residues:
k = lab16(rho)
fibers[k] += 1
poly = {0: 1}
for i in range(8):
poly = poly_mul(poly, DIGIT[rho[i]])
for n in range(NCAP + 1):
THETA[k][n] += poly.get(8 * n, 0)
sigma3 = [0] * (NCAP + 1)
for d in range(1, NCAP + 1):
for m in range(d, NCAP + 1, d):
sigma3[m] += d ** 3
lvl1 = [THETA[k][1] for k in range(16)]
check("S3.1 DP gates: residue fibers %s == {16 x16}; level-1 class "
"census = (0; 16 x15): %s"
% (sorted(set(fibers)), lvl1[0] == 0
and sorted(lvl1[1:]) == [16] * 15),
sorted(set(fibers)) == [16] and lvl1[0] == 0
and sorted(lvl1[1:]) == [16] * 15, kill="K4")
theta_L = [sum(THETA[k][n] for k in range(16)) for n in range(NCAP + 1)]
check("S3.2 Theta_L(n) = 240 sigma_3(n) for EVERY n <= %d against the "
"independent sieve (classical E8 theta = E4, CITED + verified "
"on the computed range)" % NCAP,
all(theta_L[n] == 240 * sigma3[n] for n in range(1, NCAP + 1)),
kill="K4")
odd_zero = all(THETA[0][n] == 0 for n in range(1, NCAP + 1, 2))
even_dbl = all(THETA[0][2 * m] == 240 * sigma3[m]
for m in range(1, NCAP // 2 + 1))
check("S2.2/S3 RAMIFICATION on the DP range: Theta_0(odd n) = 0 for "
"all odd n <= %d (proof: |x|^2 = 2|y|^2, |y|^2 in 8Z => level "
"even); Theta_0(2m) = 240 sigma_3(m) = Theta_L(m) for 2m <= %d; "
"Theta_0(2) = %d == 240 (witness)"
% (NCAP, NCAP, THETA[0][2]),
odd_zero and even_dbl and THETA[0][2] == 240, kill="K3")
# ======================================================================
section("S4: the derived global formulas + the ward")
# ======================================================================
equi_formula = True
for n in range(1, NCAP + 1):
num = theta_L[n] - THETA[0][n]
if num % 15 != 0:
equi_formula = False
break
val = num // 15
if any(THETA[k][n] != val for k in range(1, 16)):
equi_formula = False
break
check("S4.1 Theta_v(n) = (Theta_L(n) - Theta_0(n))/15 EXACTLY for "
"every v != 0 and every n <= %d (15-divisibility exact; "
"equidistribution = COROLLARY of S1 transitivity + isometry "
"transport)" % NCAP, equi_formula, kill="K5")
# coordinatize V for the Walsh transform
basis = []
for k in range(1, 16):
closure = {0}
fr = [0]
while fr:
x = fr.pop()
for g in basis:
z = ADD[x][g]
if z not in closure:
closure.add(z)
fr.append(z)
if k not in closure:
basis.append(k)
COORD = {}
for bits in itertools.product((0, 1), repeat=4):
c = 0
for i, bt in enumerate(bits):
if bt:
c = ADD[c][basis[i]]
COORD[c] = bits
U0 = (0, 0, 0, 0)
THAT = {}
for u in itertools.product((0, 1), repeat=4):
THAT[u] = [sum((-1) ** (sum(a * b for a, b in zip(u, COORD[k])) % 2)
* THETA[k][n] for k in range(16))
for n in range(NCAP + 1)]
def closed_form(n, sig):
even_part = 16 * sig[n // 2] if n % 2 == 0 else 0
return 16 * (even_part - sig[n])
hat_ok = all(15 * THAT[u][n] == 16 * THETA[0][n] - theta_L[n]
and THAT[u][n] == closed_form(n, sigma3)
for u in THAT if u != U0 for n in range(1, NCAP + 1))
check("S4.2 Thetahat_u(n) = (16 Theta_0 - Theta_L)/15 = "
"16 (16 1_{2|n} sigma_3(n/2) - sigma_3(n)) EXACTLY for every "
"u != 0 and n <= %d" % NCAP,
len(COORD) == 16 and len(basis) == 4 and hat_ok, kill="K5")
def sparse_theta_terms(kind, cap):
out = []
if kind in ("th3", "th4"):
out.append((0, 1))
n = 1
while n * n <= cap:
out.append((n * n, 2 if kind == "th3" else 2 * ((-1) ** n)))
n += 1
else:
o = 1
while o * o <= cap:
out.append((o * o, 2))
o += 2
return out
def sparse_mul(dense, terms):
out = np.zeros_like(dense)
for e, c in terms:
if e == 0:
out += c * dense
else:
out[e:] += c * dense[:-e]
return out
def build_thetas():
"""exact class thetas Th_j, sigma3 to N_THETA (v817/v857
build_thetas, rebuilt verbatim)."""
sig3 = np.zeros(N_THETA + 1, dtype=np.int64)
for d in range(1, N_THETA + 1):
sig3[d::d] += d ** 3
scap = 2 * N_THETA
t3 = sparse_theta_terms("th3", scap)
t4 = sparse_theta_terms("th4", scap)
one = np.zeros(scap + 1, dtype=np.int64)
one[0] = 1
p3 = one.copy()
p4 = one.copy()
for _ in range(8):
p3 = sparse_mul(p3, t3)
p4 = sparse_mul(p4, t4)
m53 = one.copy()
for _ in range(5):
m53 = sparse_mul(m53, t3)
for _ in range(3):
m53 = sparse_mul(m53, t4)
m35 = one.copy()
for _ in range(5):
m35 = sparse_mul(m35, t4)
for _ in range(3):
m35 = sparse_mul(m35, t3)
num0 = p3 + m53 + m35 + p4
num2 = p3 - m53 - m35 + p4
ok_div = bool(np.all(num0 % 4 == 0) and np.all(num2 % 4 == 0))
Th0 = (num0 // 4)[::2][:N_THETA + 1].copy()
Th2 = (num2 // 4)[::2][:N_THETA + 1].copy()
tcap = 8 * N_THETA
t2 = sparse_theta_terms("th2", tcap)
acc = np.zeros(tcap + 1, dtype=np.int64)
acc[0] = 1
for _ in range(8):
acc = sparse_mul(acc, t2)
ok_div &= bool(np.all(acc[::8][:N_THETA + 1] % 4 == 0))
Th1 = (acc[::8][:N_THETA + 1] // 4).copy()
return dict(sig3=sig3, Th=(Th0, Th1, Th2, Th1), ok_div=ok_div)
TH = build_thetas()
Th0, Th1, Th2, Th3 = TH["Th"]
sig3p = TH["sig3"]
heads = (int(Th0[1]), int(Th1[1]), int(Th2[1]), int(Th3[1]))
glue = bool(np.all((Th0 + Th1 + Th2 + Th3)[1:] == 240 * sig3p[1:]))
num2c = Th0 - Th1 + Th2 - Th3
F = -16 * sig3p.copy()
F[2::2] += 256 * sig3p[1:N_THETA // 2 + 1]
ward_all = bool(np.all(num2c[1:] == F[1:]))
odd_idx = np.arange(1, N_THETA + 1, 2)
odd_thm = bool(np.all(15 * num2c[odd_idx] == -240 * sig3p[odd_idx]))
dp_bridge = all(int(num2c[n]) == THAT[u][n]
for u in THAT if u != U0 for n in range(1, NCAP + 1))
sieve_agree = all(int(sig3p[n]) == sigma3[n] for n in range(1, NCAP + 1))
check("S4.3 GLOBAL WARD to %d: heads %s == (52,64,60,64); divisibility "
"certificates: %s; glue Th0+..+Th3 = 240 sigma_3 ALL n: %s; "
"packet numerator == closed form 16(16 1_{2|n} sigma_3(n/2) - "
"sigma_3(n)) for EVERY n (odd AND even): %s; == DP Thetahat_u on "
"n <= %d: %s; odd theorem 15 num = -240 sigma_3: %s => "
"Thetahat_u/Theta_L = %s at every odd n"
% (N_THETA, heads, TH["ok_div"], glue, ward_all, NCAP, dp_bridge,
odd_thm, Fr(-16, 240)),
heads == (52, 64, 60, 64) and TH["ok_div"] and glue and ward_all
and dp_bridge and odd_thm and sieve_agree
and Fr(-16, 240) == Fr(-1, 15), kill="K5")
print("\n THE STRUCTURAL ARGUMENT (the promotable proof sketch, "
"step by step):")
print(" LEMMA 1 (invariance + transitivity): every g in G31 is a")
print(" norm-preserving bijection of L ((4M)^T(4M) = 16I; roots ->")
print(" roots; L = root span, S1.2/S1.5) that transports class v")
print(" to gbar(v) (complex-linearity (4M)J = J(4M) makes gbar")
print(" well-defined on V = L/(1+i)L); hence Theta_{gbar(v)}(n) =")
print(" Theta_v(n) for ALL n. The induced group is Sp(4,2) (order")
print(" 720, generated by the 60 transvections T_vbar, S1.5/S1.6),")
print(" TRANSITIVE on the 15 nonzero classes => Theta_v(n) is ONE")
print(" value over v != 0 at every shell n.")
print(" LEMMA 2 (doubling): (I+J)^T(I+J) = 2I => |(1+i)x|^2 =")
print(" 2|x|^2, and (1-J)/2 inverts (1+i) on L => Theta_0(2m) =")
print(" Theta_L(m), Theta_0(odd) = 0 (|y|^2 in 8Z forces even")
print(" level).")
print(" LEMMA 3 (theta identity): Theta_L(n) = 240 sigma_3(n)")
print(" (classical: Theta_{E8} = E4; verified here to n = 24 and")
print(" via the packet glue identity to n = 16500).")
print(" CONCLUSION: 15 Theta_v(n) = Theta_L(n) - Theta_0(n) for")
print(" v != 0; Thetahat_u(n) = (16 Theta_0(n) - Theta_L(n))/15 =")
print(" 16(16 1_{2|n} sigma_3(n/2) - sigma_3(n)); at odd n:")
print(" Thetahat_u(n) = -16 sigma_3(n), Thetahat_u/Theta_L = -1/15")
print(" EXACTLY -- for ALL odd n, no census cap.")
print(" LEAN NOTES (report): needs (a) the Sp-transitivity as a")
print(" FINITE fact (decidable orbit computation on F_2^4 from the")
print(" 60 transvections -- all data in this probe), (b) the")
print(" doubling as the two matrix identities above, (c) the theta")
print(" identity as citation (Eisenstein E4) or finite")
print(" verification; the conclusion is linear algebra over Q.")
# ======================================================================
section("C: controls (each must fire)")
# ======================================================================
T1 = induced_maps[0]
fixed = [k for k in range(1, 16) if T1[k] == k]
moved = [k for k in range(1, 16) if T1[k] != k]
n_orbits = len(fixed) + len(moved) // 2
a_cl, b_cl = fixed[0], fixed[1]
r_prime = [0] + [16] * 15
r_prime[a_cl] = 32
r_prime[b_cl] = 0
h_invariant = all(r_prime[T1[k]] == r_prime[k] for k in range(16))
WP = {}
for u in itertools.product((0, 1), repeat=4):
WP[u] = sum((-1) ** (sum(x * z for x, z in zip(u, COORD[k])) % 2)
* r_prime[k] for k in range(16))
mult = Counter(WP[u] for u in WP if u != U0)
full_group_moves = any(any(r_prime[g[k]] != r_prime[k]
for k in range(16)) for g in induced_maps)
check("C1 FIRES: non-transitive H = <T_1>: %d orbits on the 15 nonzero "
"classes (%d fixed + %d swaps) != 1; explicit H-invariant NON-"
"uniform census (32/0 on two H-fixed classes): invariant %s; "
"Walsh multiset on u != 0 = %s == {-48: 4, -16: 7, 16: 4} NOT "
"uniform => the -1/15 law breaks; a full-group generator moves "
"it: %s (transitivity is load-bearing)"
% (n_orbits, len(fixed), len(moved) // 2, h_invariant,
dict(sorted(mult.items())), full_group_moves),
n_orbits == 11 and len(fixed) == 7 and h_invariant
and dict(mult) == {-48: 4, -16: 7, 16: 4}
and len(set(mult)) > 1 and full_group_moves, kill="K6")
even_vals_ok = all(int(num2c[2 * m]) == 16 * (16 * int(sig3p[m])
- int(sig3p[2 * m]))
for m in range(1, N_THETA // 2 + 1))
ratio2 = Fr(int(num2c[2]), int(240 * sig3p[2]))
check("C2 FIRES: even-shell formula Thetahat_u(2m) = 16(16 sigma_3(m) "
"- sigma_3(2m)) for ALL 2m <= %d: %s; at n = 2: Thetahat = %d "
"== 112, Theta_L = %d == 2160, ratio %s == 7/135 != -1/15 "
"(the -1/15 law is the ODD-shell statement only)"
% (N_THETA, even_vals_ok, int(num2c[2]), int(240 * sig3p[2]),
ratio2),
even_vals_ok and int(num2c[2]) == 112
and int(240 * sig3p[2]) == 2160 and ratio2 == Fr(7, 135)
and ratio2 != Fr(-1, 15), kill="K6")
# ======================================================================
section("VERDICT")
# ======================================================================
n_pass = sum(1 for _, ok in CHECKS if ok)
n_tot = len(CHECKS)
if KILLS:
VERDICT = {"K1": "LATTICE-BROKEN", "K2": "ACTION-MISMATCH",
"K3": "DOUBLING-BROKEN", "K4": "THETA-MISMATCH",
"K5": "FORMULA-BROKEN", "K6": "CONTROL-DEAD"}[KILLS[0]]
else:
VERDICT = "SHELL-GLOBAL-THEOREM"
print("%d/%d checks passed" % (n_pass, n_tot))
print("VERDICT: %s" % VERDICT)
print("\nPROMOTION-READY STATEMENT (report only -- no promotion, no edits):")
print(" THEOREM (global Gaussian shell law): on V = L/(1+i)L of the")
print(" Gaussian E8, for EVERY shell n >= 1: Theta_v(n) = (Theta_L(n)")
print(" - Theta_0(n))/15 for all v != 0, Thetahat_u(n) = 16(16 1_{2|n}")
print(" sigma_3(n/2) - sigma_3(n)) for all u != 0, and at every ODD n:")
print(" Thetahat_u(n) = -16 sigma_3(n), Thetahat_u(n)/Theta_L(n) =")
print(" -1/15 EXACTLY. Inputs: (i) the G31 class action = the 60")
print(" symplectic transvections generating Sp(4,2), transitive on the")
print(" 15 nonzero classes -- and IDENTICAL to the shell-module class")
print(" action (coordination verified on generators); (ii) norm")
print(" doubling by (1+i); (iii) Theta_L = 240 sigma_3 (classical).")
print(" This REPLACES the n <= 16500 census (v857 value theorem) by a")
print(" proof; the census range is retained as the exact ward (matched")
print(" everywhere, odd AND even). Controls: a non-transitive")
print(" subgroup admits a non-uniform invariant census (the law")
print(" breaks); the even-shell formula differs correctly (7/135 at")
print(" n = 2).")
print("Runtime: %.1f s" % (time.time() - T0))
print("ALL CHECKS PASSED" if n_pass == n_tot
else "CHECKS FAILED: %d" % (n_tot - n_pass))
raise SystemExit(0 if (n_pass == n_tot) else 1)
'''
# --------------------------------------------------------------- harness
_PF_RE = re.compile(r"^\s*\[(PASS|FAIL)\]\s+(\S+)", re.M)
_VD_RE = re.compile(r"VERDICT[:\]]")
_SHA_RE = re.compile(r"FROZEN_SPEC SHA-256[ :=]+([0-9a-f]{64})")
def _probe_file(name):
cand = os.path.abspath(os.path.join(
_HERE, os.pardir, "experiments", "tfpt-discovery", name + ".py"))
return cand if os.path.isfile(cand) else None
def _census(out):
marks = _PF_RE.findall(out)
fails = sorted({tok for st, tok in marks if st == "FAIL"})
verdict = ""
for line in out.splitlines():
if _VD_RE.search(line):
verdict = line.strip()
return len(marks), fails, verdict
def _exec_probe(name, src):
if src[:1] == "\n":
src = src[1:]
path = _probe_file(name)
same = None
if path is not None:
with open(path, encoding="utf-8") as fh:
same = (fh.read() == src)
fname = path or os.path.abspath(__file__)
mod = types.ModuleType(name)
mod.__file__ = fname
sys.modules[name] = mod
buf = io.StringIO()
code = 0
with contextlib.redirect_stdout(buf):
try:
exec(compile(src, fname, "exec"), mod.__dict__)
except SystemExit as exc:
code = 0 if exc.code is None else int(exc.code)
except Exception:
import traceback
traceback.print_exc(file=sys.stdout)
code = 99
out = buf.getvalue()
sys.stdout.write(out)
sys.stdout.flush()
return out, code, same
# ====== PART B -- the Lean skeleton (GaussianShells.lean; the consequence
# chain kernel-checked from named hypotheses; integer witnesses here)
_B_CHECKS = []
def _bcheck(name, ok, detail=""):
_B_CHECKS.append(bool(ok))
print(" [%s] %s%s" % ("PASS" if ok else "FAIL", name,
(" -- " + detail) if detail else ""),
flush=True)
return bool(ok)
_LEAN_THEOREMS = (
"dvd_diff", "decomposition", "walsh_formula", "theta_v_odd",
"walsh_odd", "walsh_odd_ratio", "walsh_even",
)
def part_b():
from sympy import divisor_sigma
print("\n" + "-" * 74)
print("v875 PART B -- the Lean skeleton: TfptCarrier/GaussianShells."
"lean (the consequence")
print("chain kernel-checked from the named ShellSystem hypotheses; "
"integer witnesses here)")
print("-" * 74, flush=True)
N = 2000
sig3 = [0] + [int(divisor_sigma(n, 3)) for n in range(1, N + 1)]
ThL = [0] + [240 * sig3[n] for n in range(1, N + 1)]
Th0 = [0] * (N + 1)
for m in range(1, N // 2 + 1):
Th0[2 * m] = ThL[m] # (H2): the (1+i) doubling
# B1: (H1) exactness -- 15 | ThL(n) - Th0(n) for every n (an actual
# arithmetic fact of the instantiated system, NOT imposed)
ok_dvd = all((ThL[n] - Th0[n]) % 15 == 0 for n in range(1, N + 1))
Thv = [0] + [(ThL[n] - Th0[n]) // 15 for n in range(1, N + 1)]
ok_dec = all(ThL[n] == Th0[n] + 15 * Thv[n] for n in range(1, N + 1))
_bcheck("B1 EXACTNESS + DECOMPOSITION (dvd_diff / decomposition, "
"kernel-checked): on the instantiated system (Theta_L = 240 "
"sigma_3, Theta_0 = the (1+i) doubling) the division "
"Theta_v = (Theta_L - Theta_0)/15 is EXACT at every n <= %d "
"and Theta_L = Theta_0 + 15 Theta_v identically" % N,
ok_dvd and ok_dec)
# B2: the Walsh formula 15 Thhat = 16 Th0 - ThL
Thhat = [Th0[n] - Thv[n] for n in range(N + 1)]
ok_wf = all(15 * Thhat[n] == 16 * Th0[n] - ThL[n]
for n in range(1, N + 1))
_bcheck("B2 THE WALSH FORMULA (walsh_formula, kernel-checked): "
"15 Thetahat_u(n) = 16 Theta_0(n) - Theta_L(n) at every "
"n <= %d (pure algebra from (H1))" % N, ok_wf)
# B3: the odd-shell theorem + the exact-ratio form
ok_odd = all(Thhat[n] == -16 * sig3[n]
and 15 * Thhat[n] == -ThL[n]
for n in range(1, N + 1, 2))
_bcheck("B3 THE ODD-SHELL THEOREM (walsh_odd / walsh_odd_ratio, "
"kernel-checked): Thetahat_u(2m+1) = -16 sigma_3(2m+1) and "
"15 Thetahat_u(2m+1) = -Theta_L(2m+1) -- the -1/15 law as "
"an integer identity, every odd n <= %d" % N, ok_odd)
# B4: the even-shell formula + the Lean file inventory
ok_even = all(Thhat[2 * m] == 16 * (16 * sig3[m] - sig3[2 * m])
for m in range(1, N // 2 + 1))
lean_path = os.path.abspath(os.path.join(
_HERE, os.pardir, "experiments", "lean4-carrier-rigidity",
"TfptCarrier", "GaussianShells.lean"))
ok_file = os.path.isfile(lean_path)
missing, has_sorry, ok_struct = list(_LEAN_THEOREMS), False, False
if ok_file:
txt = open(lean_path, encoding="utf-8").read()
body = txt.split("-/", 1)[1] if "-/" in txt else txt
missing = [nm for nm in _LEAN_THEOREMS
if ("theorem %s " % nm) not in body
and ("theorem %s\n" % nm) not in body]
has_sorry = (re.search(r"^\s*sorry\b", body, re.M) is not None
or "native_decide" in body)
ok_struct = "structure ShellSystem" in body
_bcheck("B4 THE EVEN-SHELL FORMULA + INVENTORY (walsh_even, "
"kernel-checked): Thetahat_u(2m) = 16(16 sigma_3(m) - "
"sigma_3(2m)) at every even n <= %d; TfptCarrier/"
"GaussianShells.lean present with the ShellSystem hypothesis "
"bundle + all %d theorems, no sorry / native_decide"
% (N, len(_LEAN_THEOREMS)),
ok_even and ok_file and ok_struct and not missing
and not has_sorry,
"missing: %s" % missing if missing else "")
print(" (kernel-checked statements: experiments/"
"lean4-carrier-rigidity/TfptCarrier/GaussianShells.lean -- "
"the ShellSystem hypothesis bundle (H1 transitivity, H2 "
"doubling, H3 theta identity; provenance typed on each field, "
"named NOT proven) + 7 consequence theorems, lake build green "
"3418 jobs, no sorry, no native_decide, axioms propext/"
"Classical.choice/Quot.sound only; import wired in "
"TfptCarrier.lean; lean_manifest.sha256 at 90 files)")
def run():
t0 = time.time()
_B_CHECKS.clear()
print("=" * 74)
print("v875 -- E8.SHELL.GLOBAL.01 + the GaussianShells Lean skeleton")
print("(the census -> theorem upgrade: Thetahat_u/Theta_L = -1/15 on "
"ALL odd shells,")
print("from Sp(4,2) transitivity + (1+i) doubling + Theta_L = 240 "
"sigma_3; the")
print("consequence chain kernel-checked, the inputs named; NO physics "
"claim)")
print("=" * 74, flush=True)
gates = []
print("\n" + "-" * 74)
print("EMBEDDED FROZEN PROBE: gaussian_shell_global_probe")
print("-" * 74, flush=True)
out, code, same = _exec_probe("gaussian_shell_global_probe",
_SRC_SHELL)
n, fails, verdict = _census(out)
m = _SHA_RE.search(out)
sha_ok = m is not None and m.group(1) == EXPECT_SHA_SHELL
ok_gate = (n == 15 and not fails and "SHELL-GLOBAL-THEOREM" in verdict
and code == 0 and same is not False and sha_ok)
gates.append(ok_gate)
prov = ("byte-exact vs experiments source" if same is True else
"embedded copy (source file not present)" if same is None
else "SOURCE MISMATCH")
print("\n[%s] PATTERN GATE gaussian_shell_global_probe: %d checks "
"(exp 15) | FAILs %s (exp none) | exit %d (exp 0) | spec SHA "
"%s | %s\n verdict line: %s"
% ("PASS" if ok_gate else "FAIL", n,
",".join(fails) if fails else "none", code,
"ok" if sha_ok else "MISMATCH", prov, verdict[:120]),
flush=True)
part_b()
ok_b = all(_B_CHECKS) and len(_B_CHECKS) == 4
gates.append(ok_b)
ok = all(gates)
print("\n" + "=" * 74)
print("v875: %d/%d gates passed (1 probe pattern gate + %d/4 Lean "
"skeleton checks) | runtime %.1f s"
% (sum(gates), len(gates), sum(_B_CHECKS), time.time() - t0))
print("The -1/15 census law is now a theorem for ALL odd shells; the "
"finite census")
print("stays as the exact ward; the Lean skeleton separates the "
"kernel-checked")
print("consequence chain from the three named inputs.")
print("[%s] v875 VERDICT GATE: SHELL-GLOBAL-THEOREM + the Lean "
"skeleton" % ("PASS" if ok else "FAIL"))
return 0 if ok else 1
if __name__ == "__main__":
raise SystemExit(run())
Recorded source fingerprint
65beb96eb31c770dd1ead1347e4cb3bd5a303278dba1d0c4aefeae081f3e28b8
Paper sections that cite this module
What this source index covers
The public registry includes 116 document views, 6,693 section records and 985 physical LaTeX sources. Active publication documents, research material and archives retain their recorded roles. This is source navigation, not a new semantic review or proof run.