J_eq_Jcost
plain-language theorem explainer
The identification lemma shows that the cost functional J defined by the formula (x + x^{-1})/2 - 1 coincides exactly with the Jcost from the Cost module. Researchers deriving Planck-scale constants or matching to observed G would cite this equality to bridge the axiomatic foundation to numerical computations. The proof is a one-line wrapper using extensionality followed by reflexivity on the matching definitions.
Claim. The cost functional defined by $J(x) = (x + x^{-1})/2 - 1$ equals the standard cost functional $Jcost$ from the Cost module.
background
The CostAxioms module formalizes the three primitive axioms of Recognition Science: Normalization (F(1) = 0), the Recognition Composition Law F(xy) + F(x/y) = 2F(x)F(y) + 2F(x) + 2F(y), and Calibration (second derivative of the log-transformed function at zero equals 1). The sibling definition J is the canonical cost functional J(x) := (x + x^{-1})/2 - 1, which satisfies the axioms via explicit instances for Normalization, Composition, and Calibration. This identification builds directly on the Cost module's Jcost and Jlog, with upstream results including the derivation of G from first principles as lambda_rec squared times c cubed over pi hbar.
proof idea
The proof applies the extensionality tactic to reduce the function equality to pointwise equality for all x, then closes with reflexivity since the local definition of J matches Cost.Jcost definitionally.
why it matters
This lemma closes the identification between the axiomatic J and Cost.Jcost, feeding directly into the PlanckScaleMatching theorem that equates them for deriving constants like G in RS-native units. It supports the T5 J-uniqueness step in the forcing chain by confirming the explicit form matches the cost definition. The downstream use in Constants.PlanckScaleMatching confirms its role in numerical matching to observed values.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.