J_eq_Jcost
plain-language theorem explainer
The pointwise equality J(x) = Jcost(x) for every real x is established by definition matching. Researchers deriving the recognition wavelength from bit-curvature equilibrium in the Planck-scale conjecture cite this to interchange the canonical cost with the axiomatic form without adjustment. The proof is a single reflexivity step on the shared expression (x + x^{-1})/2 - 1.
Claim. For all real $x$, $J(x) = Jcost(x)$, where $J(x) := (x + x^{-1})/2 - 1$.
background
In the Planck-Scale Matching module the derivation of λ_rec proceeds by equating bit cost to curvature cost on the Q3 hypercube. The cost functional is introduced locally as J(x) = (x + x^{-1})/2 - 1, the form fixed by J-uniqueness in the forcing chain. This theorem equates the local J to the Jcost imported from the Cost module, which satisfies the Recognition Composition Law and the normalization axiom.
proof idea
The proof is a term-mode reflexivity that matches the body of the local J definition directly to the body of Jcost.
why it matters
This equality interfaces the local definition in PlanckScaleMatching with the axiomatic Cost.Jcost, allowing the J_bit computation to feed the extremum condition J_bit = J_curv(λ_rec) and the subsequent face-averaging step that produces the factor 1/π. It supports the parent lemma in CostAxioms that verifies J satisfies the full set of cost axioms. The result closes the interface needed for the conjecture C8 derivation of λ_rec ≈ 0.564 ℓ_P.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.