isNonTrivial
plain-language theorem explainer
A gauge bond configuration on the twelve-edge cube is non-trivial precisely when at least one bond carries a nonzero rung index on the phi-ladder. Researchers resolving the Yang-Mills mass gap in Recognition Science cite this predicate to separate the vacuum from all excitations before applying the J-cost lower bound. The definition is a direct existential quantifier over the Fin 12 indices with no auxiliary lemmas.
Claim. A gauge bond configuration $cfg$ is non-trivial if there exists an edge $e$ among the twelve edges of the cube such that the integer rung index assigned to that bond is nonzero.
background
In the Recognition Science treatment of the Yang-Mills mass gap, GaugeBondConfig is the structure that assigns to each of the twelve edges of the three-dimensional cube an integer rung index on the phi-ladder. The vacuum sets every rung to zero, so the multiplier is identically one. The J-cost functional J(x) = ½(x + x⁻¹) − 1 then vanishes only on the vacuum and is strictly positive on every nonzero rung, as derived from the Recognition Composition Law and the T5 uniqueness condition.
proof idea
The definition is a one-line existential predicate: there exists e : Fin 12 such that cfg.bonds e ≠ 0. No lemmas or tactics are invoked; the predicate simply negates the vacuum condition that all bonds equal zero.
why it matters
This predicate supplies the hypothesis for both gauge_mass_gap and gauge_cost_ge_gap. It isolates the non-vacuum sector whose total J-cost is bounded below by the spectral gap Δ = J(φ) = (√5 − 2)/2. The construction thereby closes the step from the phi-ladder excitations forced by T5 and T6 to the strict positivity required by the Millennium problem statement in the RS framework.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.