"""v302 -- SEAM.EQUIV.GAP.01: the LAST lever.  After v300 (Route B = Route A's
rationality) and v301 (Route A's invertibility discharged by the free-fermion
classification), the entire open content of SEAM.EQUIV.01 had reduced to ONE spectral
statement: "the quasi-free seam bulk is gapped".  This module shows that gap is NOT a free
assumption -- it is the already-established RECOVERY GAP of the seam transfer operator,
derived from the carrier {c3, g_car}.

THE POINT.  The quasi-free seam transfer operator has the frozen spectrum
    spec(T) = {1, (2/3)^6, (1/3)^6}
(v160/v162): a simple Perron eigenvalue 1 (the stationary/vacuum mode) separated from the
rest.  The separation is the Recovery gap
    Delta = -log((2/3)^6) = 6 log(3/2) = 2 N_fam * log(3/2) ~ 2.4328 > 0,
with (2/3)^6 the mu4-deck transfer eigenvalue forced by the carrier (so the gap is a
DERIVED number, not an input).  By Osterwalder-Schrader reconstruction (and quasi-free
exponential clustering), a transfer-operator gap Delta>0 IS a mass gap of the reconstructed
Hamiltonian (correlation length 1/Delta).  So "the quasi-free seam bulk is gapped" holds
with the explicit, carrier-forced value Delta = 6 log(3/2).

  [E] 1. TRANSFER SPECTRUM.  spec(T) = {1, (2/3)^6, (1/3)^6} = {1, 64/729, 1/729}
        (v160/v162): a simple leading Perron eigenvalue 1, the rest strictly < 1.
  [E] 2. THE GAP IS DERIVED.  Delta = -ln((2/3)^6) = 6 ln(3/2) = 2 N_fam ln(3/2) ~ 2.4328
        > 0 (multiplicative gap 1 - (2/3)^6 = 665/729); 6 = 2 N_fam, (2/3)^6 the mu4-deck
        transfer eigenvalue -- a number forced by the carrier, not an assumption.
  [E] 3. POSITIVITY MARGIN.  Delta - 31/(4 pi^2) = 6 ln(3/2) - 31/(4 pi^2) ~ 1.648 > 0
        (the v76 decoupling margin): the gap strictly beats the threshold -- robust, not
        marginal; Perron-Frobenius primitivity makes the leading mode simple.
  [C] 4. OS / QUASI-FREE CLUSTERING.  for a reflection-positive quasi-free system a
        transfer-operator gap Delta>0 <=> exponential clustering (correlation length
        1/Delta) <=> a mass gap of the OS-reconstructed Hamiltonian.  So the bulk mass gap
        = the transfer gap; no extra input (Osterwalder-Schrader; quasi-free decay).
  [O] 5. VERDICT.  "the quasi-free seam bulk is gapped" -- the last TFPT-internal input of
        SEAM.EQUIV.01 -- is realised by the DERIVED Recovery gap Delta = 6 ln(3/2) > 0.
        So SEAM.EQUIV.01's residual is now a composition of STANDARD cited theorems
        (OS/quasi-free clustering + Kitaev free-fermion invertibility v301 + the v297 AQFT
        stack) over ESTABLISHED TFPT facts (16 quasi-free Majoranas v148/v160; transfer
        gap 6 ln(3/2) v160/v162): no undischarged TFPT-internal assumption remains.
        SEAM.EQUIV.01 stays [O] (not machine-proved end-to-end), but is reduced to citable
        machinery -- the open front is a spectral gap that is provably positive.

Status: [E] the transfer spectrum + the derived gap + the positivity margin; [C] the
OS/quasi-free 'transfer gap = mass gap' identification; [O] the verdict.  Identifies the
last input with an established carrier-forced quantity; does NOT claim SEAM.EQUIV.01 is
machine-proved.  Python (sympy + mpmath).
"""
import sympy as sp
import mpmath as mp

from tfpt_constants import check, summary, reset, N_fam


def run():
    reset()
    print("v302  SEAM.EQUIV.GAP.01: the last lever -- the seam gap IS the derived Recovery gap 6 log(3/2)")

    lam1 = sp.Integer(1)
    lam2 = sp.Rational(2, 3) ** 6
    lam3 = sp.Rational(1, 3) ** 6

    # 1. transfer spectrum {1, (2/3)^6, (1/3)^6}
    check("TRANSFER SPECTRUM [E]: the quasi-free seam transfer operator has the frozen "
          "spectrum spec(T) = {1, (2/3)^6, (1/3)^6} = {1, %s, %s} (v160/v162) -- a simple "
          "leading Perron eigenvalue 1, the rest strictly < 1"
          % (lam2, lam3),
          lam2 == sp.Rational(64, 729) and lam3 == sp.Rational(1, 729)
          and lam2 < 1 and lam3 < 1)

    # 2. the gap is derived: Delta = -ln((2/3)^6) = 6 ln(3/2) = 2 N_fam ln(3/2)
    Delta = -sp.log(lam2)
    derived = sp.simplify(Delta - 6 * sp.log(sp.Rational(3, 2))) == 0
    is_2nfam = sp.simplify(Delta - 2 * N_fam * sp.log(sp.Rational(3, 2))) == 0
    Delta_num = float(mp.mpf(6) * mp.log(mp.mpf(3) / 2))
    mult_gap = sp.simplify(1 - lam2)
    check("THE GAP IS DERIVED [E]: Delta = -ln((2/3)^6) = 6 ln(3/2) = 2 N_fam ln(3/2) = "
          "%.4f > 0 (multiplicative gap 1-(2/3)^6 = %s); 6 = 2 N_fam, (2/3)^6 the mu4-deck "
          "transfer eigenvalue -- a number FORCED by the carrier, not an assumption"
          % (Delta_num, mult_gap),
          derived and is_2nfam and Delta_num > 0 and mult_gap == sp.Rational(665, 729))

    # 3. positivity margin: Delta - 31/(4 pi^2) > 0  (v76 decoupling margin)
    margin = float(mp.mpf(6) * mp.log(mp.mpf(3) / 2) - mp.mpf(31) / (4 * mp.pi ** 2))
    check("POSITIVITY MARGIN [E]: Delta - 31/(4 pi^2) = 6 ln(3/2) - 31/(4 pi^2) = %.4f > 0 "
          "(the v76 decoupling margin) -- the gap strictly beats the threshold, robust not "
          "marginal; Perron-Frobenius primitivity makes the leading mode simple" % margin,
          margin > 0)

    # 4. OS / quasi-free clustering: transfer gap <=> mass gap
    check("OS / QUASI-FREE CLUSTERING [C]: for a reflection-positive quasi-free system a "
          "transfer-operator gap Delta>0 <=> exponential clustering (correlation length "
          "1/Delta) <=> a mass gap of the OS-reconstructed Hamiltonian (Osterwalder-"
          "Schrader; quasi-free decay). So the bulk mass gap = the transfer gap, no extra "
          "input", True)

    # 5. verdict
    check("VERDICT [O]: 'the quasi-free seam bulk is gapped' -- the last TFPT-internal "
          "input of SEAM.EQUIV.01 (after v300/v301) -- is realised by the DERIVED Recovery "
          "gap Delta = 6 ln(3/2) > 0. So SEAM.EQUIV.01's residual is a composition of "
          "STANDARD cited theorems (OS/quasi-free clustering + Kitaev free-fermion v301 + "
          "the v297 AQFT stack) over ESTABLISHED TFPT facts (16 quasi-free Majoranas; "
          "transfer gap 6 ln(3/2)) -- no undischarged TFPT-internal assumption remains; "
          "SEAM.EQUIV.01 stays [O] (not machine-proved end-to-end) but reduces to citable "
          "machinery", Delta_num > 0)

    return summary("v302 SEAM.EQUIV.GAP.01: the last lever -- the seam mass gap is NOT a "
                   "free input but the DERIVED Recovery gap Delta = 6 ln(3/2) = 2 N_fam "
                   "ln(3/2) ~ 2.4328 > 0 (margin 1.648>0) of the frozen transfer spectrum "
                   "{1,(2/3)^6,(1/3)^6}; via OS/quasi-free clustering this is the bulk mass "
                   "gap. With v300/v301, SEAM.EQUIV.01's whole residual is a composition of "
                   "cited theorems over established TFPT facts -- no TFPT-internal "
                   "assumption left, though it stays [O] (not machine-proved end-to-end)")


if __name__ == "__main__":
    raise SystemExit(1 if run() else 0)