"""v308 -- SEAM.EQUIV.01 as a machine-checked composition certificate. Attack point 1 of the TOE roadmap: the open keystone "the raw seam-Calderon boundary net IS the holomorphic c=8 (E8)_1 net". v300/v301/v302 reduced it to a single spectral input ("the quasi-free seam bulk is gapped"), and that gap is the DERIVED recovery gap 6 ln(3/2) (v302). v297 wrote the closing implication as a four-theorem literature stack. This module ASSEMBLES that stack into ONE well-typed logical chain and verifies every ARITHMETIC discriminator it rests on, so the open content is pinned to exactly one cited (not-yet-machine-proved) step. The chain (each link's out-token = the next link's in-token): G [E] carrier {c3,g_car} => derived recovery gap Delta = 6 ln(3/2) > 0 (v302) A [C] gap + quasi-free (16 Majoranas, v148) => invertible/SRE bulk (Kitaev: free fermions carry no intrinsic anyons) -> #anyons = |det K| = 1 B [E] invertible bulk => trivial Drinfeld center => holomorphic boundary (Mueger; Kawahigashi-Longo-Mueger) -> #primaries = |det Cartan| = 1 C [E] holomorphic c=8 net => even unimodular rank-8 lattice => E8 (Conway- Sloane; Dong-Xu) -> seam net = (E8)_1 DISCRIMINATORS (all exact, machine-checked here from the Cartan matrices): * |det Cartan(E8)| = 1 (one anyon / one primary / invertible / holomorphic) * |det Cartan(D8=SO(16))| = 4 (the same-c=8 rival: four primaries -> NOT holomorphic) * carrier D5(+)A3: |det| = 4*4 = 16 => the anyon-condensation tower 16 -> 4 -> 1 * c = g_car + N_fam = 5 + 3 = 8 The ONE undischarged premise is link A's spectral input read through OS: "the OS-reconstructed bulk mass gap equals the transfer gap" (Osterwalder-Schrader / quasi-free clustering, cited in v302). Everything else composes. HONEST SCOPE: [E] the arithmetic discriminators + the well-typed composition; [C] the three literature links; [O] the end-to-end machine proof (a Lean target) and the OS input. An assembly/reduction certificate (like v261/v297), NOT a closure of SEAM.EQUIV.01. Python-only (sympy linear algebra + chain check). """ import sympy as sp from tfpt_constants import check, summary, reset, g_car, N_fam, rankE8 def cartan(n, edges): A = sp.eye(n) * 2 for i, j in edges: A[i - 1, j - 1] = -1 A[j - 1, i - 1] = -1 return A # Dynkin diagrams (any valid labeling gives the same determinant) E8 = cartan(8, [(1, 3), (3, 4), (4, 5), (5, 6), (6, 7), (7, 8), (2, 4)]) D8 = cartan(8, [(1, 2), (2, 3), (3, 4), (4, 5), (5, 6), (6, 7), (6, 8)]) D5 = cartan(5, [(1, 2), (2, 3), (3, 4), (3, 5)]) A3 = cartan(3, [(1, 2), (2, 3)]) def run(): reset() print("v308 SEAM.EQUIV.01 composition certificate (Kitaev->Mueger->KLM->Conway-Sloane)") # ---- discriminators ---- dE8, dD8, dD5, dA3 = (int(M.det()) for M in (E8, D8, D5, A3)) check("discriminator: |det Cartan(E8)| = 1 (one anyon / one primary / " "invertible / holomorphic)", dE8, 1, exact=True) check("discriminator: |det Cartan(D8=SO(16))| = 4 (the same-c=8 rival has " "four primaries -> NOT holomorphic)", dD8, 4, exact=True) check("carrier tower: |det D5| * |det A3| = 4*4 = 16 = dim S^+ => " "anyon-condensation tower 16 -> 4 -> 1", dD5 * dA3, 16, exact=True) check("central charge c = g_car + N_fam = 5 + 3 = 8 (holomorphic target rank)", g_car + N_fam, 8, exact=True) check("rank E8 = 8 matches the even-unimodular hull (Conway-Sloane uniqueness)", rankE8, 8, exact=True) # ---- the derived gap (link G input is carrier-forced, not assumed) ---- gap = 6 * sp.log(sp.Rational(3, 2)) # = 2 N_fam ln(3/2) margin = gap - sp.Rational(31, 4) / sp.pi ** 2 # v76 decoupling margin check("link G [E]: the recovery gap Delta = 6 ln(3/2) = 2 N_fam ln(3/2) > 0 " "is carrier-forced (v302), and the v76 margin Delta-31/(4pi^2) > 0", bool(gap > 0) and bool(sp.N(margin) > 0)) # ---- the four-link chain: out(i) must equal in(i+1) ---- chain = [ dict(name="G", src="carrier {c3,g_car}", dst="gap_positive", kind="E", why="derived recovery gap 6 ln(3/2) (v302)"), dict(name="A", src="gap_positive", dst="invertible_bulk", kind="C", why="Kitaev: gapped quasi-free => no intrinsic anyons, |det K|=1"), dict(name="B", src="invertible_bulk", dst="holomorphic_c8", kind="C", why="Mueger/KLM: trivial center => holomorphic boundary net"), dict(name="C", src="holomorphic_c8", dst="seam_is_E8", kind="C", why="Conway-Sloane: holomorphic c=8 => unique even unimodular = E8"), ] well_typed = all(chain[i]["dst"] == chain[i + 1]["src"] for i in range(len(chain) - 1)) for lk in chain: print(f" link {lk['name']} [{lk['kind']}] {lk['src']:<16} -> " f"{lk['dst']:<16} ({lk['why']})") check("COMPOSITION [E]: the four links are well-typed (out(i) = in(i+1)); the " "final conclusion is 'seam_is_E8' = SEAM.EQUIV.01", well_typed and chain[-1]["dst"] == "seam_is_E8") # ---- the single undischarged premise (everything else composes) ---- cited_links = [lk["name"] for lk in chain if lk["kind"] == "C"] open_premise = ("OS-reconstructed bulk mass gap = transfer gap " "(Osterwalder-Schrader / quasi-free clustering, link A input)") check("REDUCTION [O]: the only undischarged TFPT-internal premise is the OS " "input '%s'; the three category-theory links (%s) are cited standard " "theorems, and the discriminators above are exact" % ( open_premise, ",".join(cited_links)), open_premise.startswith("OS-reconstructed") and len(cited_links) == 3) # ---- negative control: the rival D8 fails the holomorphy discriminator ---- check("NEG CONTROL [E]: the same-c=8 rival SO(16)_1 has |det Cartan(D8)|=4 != 1, " "so it is NON-holomorphic and excluded -- equal central charge is " "necessary, not sufficient (the load-bearing gatekeeper is holomorphy)", dD8 != 1 and dE8 == 1) return summary("v308 SEAM.EQUIV.01 composition certificate") if __name__ == "__main__": raise SystemExit(1 if run() else 0)