nontriviality_from_cost
plain-language theorem explainer
Non-triviality follows from the recognition cost vanishing only at unity. Workers deriving phi-ladder baselines cite this to exclude identity transitions from physical event counts. The proof assumes equality to one by contradiction and invokes the normalization J(1) = 0 to contradict the positivity hypothesis.
Claim. Let $J(x) = (x + x^{-1})/2 - 1$. If $x > 0$ and $J(x) > 0$, then $x ≠ 1$.
background
The module derives baseline rung integers and related quantities from the combinatorics of the 3-cube Q₃, upgrading prior boundary assumptions to derived status. J denotes the recognition cost functional J(x) = (1/2)(x + x^{-1}) - 1, defined for x > 0. The upstream normalization J_at_one states that the multiplicative identity carries zero cost, which is the algebraic encoding of double-entry symmetry under inversion.
proof idea
The proof is a one-line wrapper that assumes x = 1 by contradiction, substitutes into the hypothesis, and applies the normalization J_at_one to obtain J(1) = 0, contradicting J(x) > 0.
why it matters
This theorem upgrades the non-triviality assumption to derived status B-20 inside the cube-geometry derivations. It feeds the neutrino_rung result later in the same module. The result encodes the consequence of T5 J-uniqueness together with the zero-cost property at the fixed point, ensuring physical masses occupy non-vacuum rungs on the phi-ladder.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.