J
plain-language theorem explainer
The recognition cost functional is defined by J(x) = (x + x^{-1})/2 - 1 for real x. Researchers deriving baseline rung integers and particle masses from 3-cube combinatorics cite this to quantify deviations from unity. It enters as a direct definition that matches the closed-form expression without intermediate lemmas.
Claim. The recognition cost functional is defined by $J(x) = (x + x^{-1})/2 - 1$ for $x > 0$.
background
The Baseline Rung Derivations module upgrades prior boundary assumptions to derived status by tracing every integer to D = 3 and the combinatorics of the 3-cube Q3. Quantities such as octave offset (-8), neutrino baseline (-54), lepton baseline (2), and quark baseline (4) are obtained from vertex, edge, face, and wallpaper counts at this dimension. The recognition cost J measures deviation from the fixed point x = 1, where J(1) = 0 renders the case unobservable, consistent with the J-uniqueness step in the forcing chain.
proof idea
This declaration is the direct definition of the functional using the closed-form expression (1/2)(x + x^{-1}) - 1.
why it matters
This definition supplies the cost measure required for all subsequent baseline derivations in the module, including non-triviality, generation ordering, and completeness statements that feed the phi-ladder mass formula. It realizes the T5 J-uniqueness landmark of the unified forcing chain and enables the eight-tick octave structure with period 2^3. The result closes the transition from assumed to derived status for the rung integers listed in the module table.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.