SU(7): verifiable certificates and formula attribution

The model transcription uses the equation numbers in the Komori–Maru PDF: parities (11–13), gauge potential (68), fermionic potentials (72–76), and Table 1. Some HTML equation numbers are shifted by six. The fixed inputs and the precise potential, rather than an unspecified physical model, are what these certificates cover.

Phases and exclusion of the printed rounding intervals

For signed coefficients m, parity signs s ∈ {+1,−1}, and positive integer charges c, define

Each printed phase is expanded to its rounding interval of half-width 0.0005. Each computed minimum is isolated in an interval of half-width 10⁻⁶. The nine decimal places below are numerical approximations, not nine certified decimal places.

F′ is strictly negative throughout all five printed intervals. Thus none contains a stationary point of the transcribed potential. A nonzero overall normalization cannot move a stationary point. Neither a common positive integer Fourier cutoff nor a common multiplicative fermion normalization restores stationarity in all five intervals. The admissible normalization interval for row 1 ends below 0.863, whereas that for row 2 starts above 0.952. The exclusions concern the printed gauge contribution and the stated matter contents.

Reconstruction from representations

Q = 2T⁴⁴ = E₅₇ + E₇₅ commutes with P₆ and B = P₅P′₅. Their common eigenbasis has weights (q,P₆,B): three copies of (0,+,+), one (0,−,−), one (0,−,+), and (±1,−,−). Direct enumeration of Sym², Sym³ and 7⊗7̄−1 gives dimensions 28, 84 and 48, respectively; Newton identities independently check both symmetric powers.

In Sym³, the antiperiodic c = 1 coefficient is 12. It includes the lower charges of the quartet, whose charges are ±3 and ±1. Removing that contribution is not justified by the representation. Reversing the product of intrinsic parities sends s to −s and reproduces the other four tables. The representation content belongs to Komori–Maru; the earlier SU(7) reconstruction is documented in Marín’s Part VI. [KM25] [Marín VI]

The last two terms in the 84 formula have subscripts 48 in PDF equation (76), HTML equation (82). This appears to be an index typo. The reconstruction assigns each field the parities of its own representation; the typo has not been established as the cause of the numerical discrepancy.

The gauge question and its assumptions

On a flat background F_MN = 0, with background gauge fixing and compatible Faddeev–Popov ghost parities, A_μ contributes four components, A₅ one, and the complex ghost subtracts two in the positive P₆ sector: 4 + 1 − 2 = 3. A₆ contributes one in the other sector. For charged pairs, reversing both fifth-direction parities gives an equivalent spectrum because Q exchanges the reflection eigenspaces.

Under these assumptions the candidate gauge triples (m,s,c) are (−3/4,+,2), (−3/2,+,1), (−3,−,1). The printed triples are (−1,+,2), (−2,+,1), (−7/2,−,1). The 3+1 candidate predates this certification and is recorded in Part VII. It also fails to reproduce the printed phases. Choosing the physical determinant still requires a complete gauge and boundary analysis. The familiar five-dimensional gauge–ghost factor −3 in Haba–Yamashita does not by itself settle that six-dimensional question. [Marín VII] [HY04]

Why the minimum certificate is global

Periodicity F(α+2) = F(α) and reflection F(−α) = F(α) reduce the domain to [0,1]. Opposite signs of F′ isolate a root in a strictly convex neighborhood. Outside that neighborhood, an exhaustive interval partition proves that F exceeds its value at a reference point inside the neighborhood. The partition has no gaps. Rational endpoints and positive margins are included in the certificate JSON.

This standard integral bound controls the Fourier tail. The bound ∑ |m|(πc)³ζ(2) controls the variation of F″. Native arithmetic encloses π with Machin’s formula and rational alternating series, reduces phases exactly, and uses Taylor expansions with explicit remainders for sine and cosine. Integer division rounds outward. Sage/Arb independently evaluates each interval without reusing that trigonometric implementation.

For k = R₅/R₆ ≥ 10, restored sixth-direction terms are bounded using

The remainder g−1 decays exponentially. The rational bound uses π > 3 and e⁶ > 400; its contribution to F′ is too small to reconcile any printed phase interval. This result assumes the stated massless determinant and matter contents. Part VI already discussed finite-k suppression; this dossier supplies an explicit uniform bound.

Certified propagation to masses

At fixed m_W = 80.4 GeV and g₄ = 0.63, the root and curvature intervals propagate through the following positive mass formulas. They are conditional consequences of these inputs and potentials. Here F″ denotes differentiation with respect to α. [KM25, mass relations]

The separate 21 moment ceilings assume the quartic-logarithmic truncation and the Higgs-mass window 123–127 GeV, at the stated m_W and g₄. Their interval replay does not turn them into full-Fourier bounds and does not establish attainment. See the conditional-bound verification.

Formula-by-formula comparison and attribution

The comparison matches mathematical expressions after making normalization and variable changes explicit. An antecedent for an identity does not imply that two physical models are equivalent. The references identify checked sources for the formulas and their applications.

1. Periodic and antiperiodic expansions

Write S_±(x) = ∑_n≥1(±1)ⁿcos(nx)/n⁵. Haba, Takenaga and Toshifumi Yamashita give the following expansions in equations (10–11), including higher terms. For x > 0, their ln(x²) equals 2 ln x. [HTY05]

The even extension uses ln|x|. These kernels and their logarithmic term are established formulas.

2. The three-coefficient potential has a direct antecedent

With x = πα > 0 and the constant term removed, define A_j = ∑_s=+1 mc^j, B_j = ∑_s=−1 mc^j, and

For the finite charge list, F(x/π)−F(0) = f(x)+O(x⁶) as x→0. Sakamoto and Takenaga’s equation (15) has exactly this functional form, with the coefficient map

Their equations (16–18) specify discrete coefficients from matter multiplicities in an SU(3) model. The SU(7) representation dictionary and allowed coefficient values differ. This is a match of analytic structure, not an identification of the models. Credit for this antecedent belongs to Makoto Sakamoto and Kazunori Takenaga, in addition to the earlier kernel expansions. [ST07]

3. Stationary curvature and the fixed-mass reduction

Differentiating the displayed f and imposing f′(x_*) = 0 at x_* > 0 gives the algebraic consequences

The last two expressions require nonzero denominators. They are exact for f; the full Fourier potential has higher-order corrections. Part VII develops their SU(7) fixed-mass application. The general identities are algebraic consequences of the established potential. Sakamoto–Takenaga’s equation (37) already eliminates the logarithm in the special case C⁽²⁾ = 0; it is not the general formula printed above. [Marín VII] [ST07]

Set K = √3 m_Wg₄/(2π³). Since F″(α) = π²f″(x) within the truncation, μ = m_h²/(Kπ²)². The full-potential diagnostic m_hα/√F″ = K follows directly from the mass formula; Part VI uses it as a consistency check, not an independent mass law. [KM25] [Marín VI]

4. Lambert W and its branches

For D > 0 and A₄ > 0, set y = x², d = 12ζ(3)D/A₄ and b = (4G−A₄)/(2A₄). The stationarity equation becomes

W(z)e^W(z) = z defines the classical Lambert function; Corless, Gonnet, Hare, Jeffrey and Knuth provide the standard modern reference for its branches. When b−1−ln d > 0, W₋₁ yields a local minimum and W₀ a local maximum of f. At equality the stationary points merge and the curvature vanishes. These branch assignments use the stated signs, and neither root is guaranteed to lie in the small-angle regime. Part VII applies this standard inversion. A full-Fourier global minimum requires a separate proof. [Corless96] [Marín VII]

5. Duplication, endpoint factors and the finite function basis

The elementary separation into even and odd n gives the exact relation

Cacciapaglia, Cornell, Deandrea, Isnard, Pasechnik, Preda and Wang explicitly use this identity and its endpoint values in equations (2.11–2.13) of their PDF, (11–13) in HTML. Their functions are ℱ^±(a) = (3/2)S_±(2πa). This is a relevant published antecedent, not a claim that they originated the mathematical identity. [CCD24]

For the lab’s charges c = 1,2,3, substitution reduces the six signed kernels to five periodic frequencies 1,2,3,4,6. The endpoint factor 31/16 is 1+15/16. In Part VII notation,

These are direct deductions from the established kernel identity. The SU(7) integer classification and nonnegative generator relations in Part VII are more specific statements and retain that attribution. W_end is the quantity called W in the seed-shift theorem; it is distinct from the Lambert function.

6. SU(7) congruences and their scope

Part VII obtains this model-specific law from the eight allowed matter generators and either stated gauge contribution, using the elementary identity c⁴ ≡ c² (mod 3). Every matter generator shifts 8D−2A₄ by a multiple of six, while the gauge contribution has residue three. The congruence holds for both gauge choices; the parity of 8D differs. The Lean proof certifies this application. [Marín VII]

Likewise, D = (S+7Δ)/8 with S = A₂+B₂ and Δ = A₂−B₂ is a rearrangement of the periodic/antiperiodic curvature weights. A trace formulation must also specify whether opposite charges are counted separately. Higher derivatives at the origin cannot be obtained by treating ζ(1) as finite: the quartic term contains the logarithm displayed above.

Attribution ledger

The machine-readable comparison is available as formula_attribution.json. Its symbolic checks verify the displayed changes of variables and algebraic consequences. Physical equivalence requires additional assumptions.

Earlier analysis and the verification recorded here

Carles Marín’s Part VI records the five discrepant minima, the representation reconstruction, the apparent 84 index typo, finite-k suppression and the different fitted fermion factors. Part VII contains the moment identities, lattice laws and the 3+1 candidate. The manuscripts acknowledge Claude (Anthropic) as an AI research assistant; the present certification and literature audit were prepared with Codex (OpenAI) assistance. Mathematical sources retain the authorship listed above.

This dossier records intervals covering the complete rounding ranges, controlled infinite tails, and ten full-domain global-minimum certificates checked by two arithmetic implementations. It also proves the exclusion of a common Fourier cutoff for every positive integer N under the stated assumptions. The 26 Lean declarations formalize the model algebra. These verification artifacts do not establish scientific priority for the underlying results.

Bibliographic finding: the inspected Part VII source does not cite Sakamoto–Takenaga, although its three-coefficient potential has the antecedent identified above. This dossier adds that credit. Presentations of that reduction should carry the reference; the SU(7) arithmetic and conditional optimization must be assessed separately.

The earlier review checked the Komori–Maru version history and the two citing articles returned by INSPIRE: spherical compactification and gauge coupling unification. No correction of the five benchmark rows was identified there. The snapshot and its limits are recorded in literature_audit.json. Formula searches additionally used the kernel expansions, three-coefficient form, Lambert equation, endpoint identity and SU(7) congruence, including equivalent notation.

The earlier allegation of a missing absolute value in Haba–Yamashita remains withdrawn. It is not one of the discrepancies supported here. No author correspondence or external expert review has been performed, and the absence of a search result does not establish absence from all papers.

Statement and proof register

• SU7-T1 The 7, Sym2(7), adjoint and Sym3(7) characters imply the eight implemented fermionic coefficient tables.
  Proof: Lean exact weights plus independent matrix diagonalization and Newton identities. Status: formal-algebra.
• SU7-T2 Changing periodic gauge weight 4 to 3 with the odd-sector weight fixed at 1 changes 8D by 9 and A4 by 9/2, preserving W_end and 8D-2A4, for every fixed matter content.
  Proof: Lean, including universal integer matter shifts. Status: formal-algebra.
• SU7-T3 Each of the five Table 1 rounding boxes contains no stationary point for the explicitly transcribed infinite potential.
  Proof: Integer interval arithmetic, analytic Fourier remainder and independent Arb replay. Status: computer-assisted-theorem.
• SU7-T4 No common positive integer winding cutoff or common multiplicative fermionic normalization restores stationarity in all five rounding boxes.
  Proof: Finite exact interval exclusions, uniform infinite-tail bound and disjoint normalization intervals. Status: computer-assisted-theorem.
• SU7-T5 For each of five listed matter contents and each of two fixed gauge seeds, the enclosed positive small-phase root is the unique global minimum on [0,1].
  Proof: Exhaustive continuum cover, strict convexity at the root, positive exterior energy gaps; independently checked with Arb. Status: computer-assisted-theorem.
• SU7-T6 Within the printed massless determinant, restoring the sixth-direction terms at k=R5/R6>=10 cannot reconcile the printed phases.
  Proof: Exact exponential bound and a uniform derivative-error enclosure. Status: computer-assisted-theorem.
• GHU-L1 The printed KLY harmonic differentiates to curvature coefficient 18-4Nf. KLY denotes Kubo, Lim and Hiroyuki Yamashita; see the attribution ledger.
  Proof: Exact symbolic differentiation in Sage. Status: symbolic-identity.
• GHU-L2 At a stationary point of the stated small-angle expansion, f_xx=2*zeta(3)*D-A4*x^2/6.
  Proof: Exact symbolic substitution in Sage. Status: conditional-symbolic-identity.
• SU7-T7 For every nonnegative integer combination of the eight matter generators, 8D-2A4 is congruent to 3 modulo 6 for either gauge seed; 8D is odd for the printed seed and even for the 3+1 seed.
  Proof: Lean: exact generator moments followed by universal integer congruence proofs. Status: formal-algebra.
• SU7-T8 The ten certified roots give enclosed Higgs masses and compactification scales at fixed mW=80.4 GeV and g4=0.63.
  Proof: Arb propagation of root and curvature intervals through the stated positive mass formulas. Status: conditional-computer-assisted-result.

What remains open

• Physical gauge determinant: Complete written gauge-fixed boundary problem and literature/author comparison; algebraic 3+1 counting alone does not settle every physical assumption.
• Other model contents and multiple Wilson phases: An individual continuum certificate; ten benchmarks do not certify arbitrary scans.
• Moment upper bounds: Keep small-angle hypotheses. A certified full-Fourier benchmark does not promote the moment ceiling into a full-potential theorem.
• Neutrinos and collider comparisons: Algebraic identities may be formalized; numerical diagonalization, experimental inputs and phenomenological viability require their own checks.
• Thermal bounce and cosmological history: Validated differential-equation solutions and full error propagation before claiming interval-certified transition predictions.
• Real analysis in Lean: Formalize convergence, derivative interchange, tail estimates, convexity and the certificate checker. Present analytic proofs are computer-assisted, not Lean-certified.

Reproduction and files

The recorded proof engines are Lean 4.27.0 (core library; replayed 13 October 2026). The original 4.10.0 source and receipt are retained under proof/su7; only List.bind was renamed to List.flatMap, with theorem statements unchanged. See the complete certificate catalogue. The numerical engine is and SageMath 10.9, with Arb at 192-bit precision for the interval replays. Repository attributes preserve the exact bytes of the certificate inputs and proof sources so their SHA-256 checks remain reproducible across platforms.

From the lab source repository, with SymPy and mpmath available:

python proof/su7/reconstruct.py
python proof/su7/global_certificates.py
sage -python proof/su7/verify_sage.py results/ghu_su7_reconstruction_20261008
lean proof/su7/SU7Certificates.lean

The Python scripts write to results/ghu_su7_reconstruction_20261008. The Sage command checks the continuous certificates; Lean checks the exact algebra. To replay the conditional moment ceilings, copy data/su7_certification/candidate_bounds.input.json into that results directory and run sage -python proof/su7/verify_bounds_sage.py results/ghu_su7_reconstruction_20261008.

The results, partitions, checksums, theorem register and logs are preserved in data/su7_certification/. Download the certificate bundle or use Screen a table → Certified SU(7) benchmarks in the application. A change of matter content, potential or physical assumptions requires a new certificate.

References and authors

1. Yuzuho Komori and Nobuhito Maru. SU(7) Grand Gauge-Higgs Unification (2025). PDF equations (11–13), (68), (72–76), (80–82), and Table 1.
2. Naoyuki Haba and Toshifumi Yamashita. A general formula of the effective potential in 5D SU(N) gauge theory on orbifold (2004). Section 5, especially equations (5.9–5.10); JHEP 02 (2004) 059.
3. Naoyuki Haba, Kazunori Takenaga and Toshifumi Yamashita. Higgs mass in the gauge-Higgs unification (2004 preprint; 2005 publication). Equations (10–11); Physics Letters B 615 (2005), 247–256.
4. Makoto Sakamoto and Kazunori Takenaga. Large Gauge Hierarchy in Gauge-Higgs Unification (2006 preprint; 2007 publication). Equations (13–18) and (37); Physical Review D 75 (2007), 045015.
5. Giacomo Cacciapaglia, Alan S. Cornell, Aldo Deandrea, Wanda Isnard, Roman Pasechnik, Anca Preda and Zhi-Wei Wang. General vacuum stability of orbifold gauge breaking and application to asymptotic grand unification (2024). PDF equations (2.11–2.13), HTML equations (11–13).
6. R. M. Corless, G. H. Gonnet, D. E. G. Hare, D. J. Jeffrey and D. E. Knuth. On the Lambert W function (1996). Advances in Computational Mathematics 5, 329–359. Modern reference for the classical function and its branches.
7. Masahiro Kubo, C. S. Lim and Hiroyuki Yamashita. The Hosotani Mechanism in Bulk Gauge Theories with an Orbifold Extra Space S¹/Z₂ (2001 preprint; 2002 publication). Equations (33) and (35). Hiroyuki Yamashita is distinct from Toshifumi Yamashita in HY04 and HTY05.
8. Carles Marín. Part VI: Proton decay in SU(7) grand gauge-Higgs unification (local source reviewed 8 October 2026). The section “The instrument, and where it fails” documents the numerical diagnostics.
9. Carles Marín. Part VII: An Upper Bound on the Compactification Scale of SU(7) Grand Gauge-Higgs Unification, and the Dijet Angular Distribution That Tests It (local source reviewed 8 October 2026). Source for the SU(7) moment reduction, congruences, generator classification and conditional bounds.

Attribution distinguishes the source of a formula, an application to a specific model, and the production of verification artifacts.