costFamily_one_eq_J
plain-language theorem explainer
The theorem shows that the cost family at parameter 1 recovers the J-cost exactly for positive reals. Algebraists normalizing initial objects in the Recognition Category cite this step when specializing the general family. The proof is a direct algebraic reduction that unfolds the definitions and applies real exponent rules.
Claim. For every real $x > 0$, $F_1(x) = J(x)$, where $F_κ(x) := (x^κ + x^{-κ})/2 - 1$ is the one-parameter cost family.
background
The costFamily definition supplies the explicit one-parameter family $F_κ(x) = (x^κ + x^{-κ})/2 - 1$ on positive reals, the continuous solutions to the calibrated d'Alembert law prior to fixing κ. The J-cost is the special case at κ = 1, drawn from the CostAlgebra module. This theorem lives in the RecognitionCategory module, which assembles the algebraic structure for costs under the Recognition framework.
proof idea
The term proof unfolds costFamily together with the J definition from CostAlgebra, rewrites via the rules x^1 = x and x^{-1} under the positivity hypothesis, then simplifies directly against the Jcost definition.
why it matters
This normalization is invoked by the two downstream theorems that establish costAlgKappaInitial.cost x = J x and costAlgPlusInitial.cost x = J x. It supplies the concrete link from the general family to the canonical J-cost, consistent with J-uniqueness in the forcing chain. No open scaffolding remains at this step.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.