Jcost
plain-language theorem explainer
J-cost is the functional J(x) = (x + x^{-1})/2 - 1 on positive reals. Researchers deriving gravitational coherence collapse from recognition cost cite this when computing path integrals for action C. The definition is a direct algebraic expression that implements T5 J-uniqueness from the forcing chain.
Claim. The J-cost functional is given by $J(x) = (x + x^{-1})/2 - 1$ for $x > 0$.
background
In the Coherence Collapse module, recognition action along a path γ is defined as the integral of J-cost: C[γ] = ∫ J(r(t)) dt. This supplies the cost term that bridges gravitational collapse to the Born rule via the identity C = 2A, where A is the residual rate action -ln(sin θ_s). Upstream, ObserverForcing.cost defines the cost of any recognition event as Jcost of its state, while MultiplicativeRecognizerL4.cost derives the same functional from a comparator on positive ratios.
proof idea
Direct definition. It sets J(x) to the algebraic expression that matches the J-uniqueness landmark in UnifiedForcingChain without invoking further lemmas or tactics.
why it matters
This definition supplies the core cost functional for recognition action C[γ] in the gravity-coherence paper. It underpins the central C = 2A identity, Born rule emergence P(I) = exp(-C_I)/Σ exp(-C_J), and the mesoscopic threshold m_coh ≈ 0.2 ng. It realizes T5 J-uniqueness and feeds the eight-tick octave and D = 3 derivations in the forcing chain.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.