J_eq_zero_imp_one
plain-language theorem explainer
The result shows that the recognition cost J vanishes only at the identity ratio x=1 when x is positive. Researchers deriving mass rungs or ledger factors from the phi-ladder cite it to exclude trivial transitions from event counts. The proof unfolds the definition of J and applies linear and nonlinear arithmetic to obtain a contradiction unless x equals 1.
Claim. If $x > 0$ and $J(x) = 0$, then $x = 1$, where the recognition cost is given by $J(x) = (x + x^{-1})/2 - 1$.
background
The functional J is the recognition cost J(x) = (1/2)(x + x^{-1}) - 1 defined on positive reals. In the module, every integer baseline traces to the single input D = 3 via cube combinatorics on Q_3. Item B-20 upgrades non-triviality to derived status: any transition with x = 1 has zero cost and leaves no ledger record, so identity transitions are excluded from the physical event count. Upstream results supply the cost interpretation of recognition events and the identity event at the J minimum.
proof idea
The tactic proof unfolds the definition of J to obtain the equation x + x^{-1} = 2. Linear arithmetic isolates the inverse as x^{-1} = 2 - x. Multiplication by x and substitution of the known product x * x^{-1} = 1 then yields a quadratic relation that nonlinear arithmetic shows holds only when x = 1.
why it matters
This declaration upgrades the non-triviality assumption B-20 to derived status from T1 plus T5 J-uniqueness. It guarantees that only non-unit ratios contribute to ledger records, supporting the mass formula yardstick * phi^(rung - 8 + gap(Z)) and the exclusion of zero-cost events. The result sits inside the baseline rung derivations that feed octave offset and neutrino baseline calculations from D = 3.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.