costLambdaTwo
plain-language theorem explainer
Defines the λ=2 cost F₂(x)=(x²+x⁻²)/2−1 on the positive reals, the second member of the hyperbolic cost family whose unit curvature is 4 rather than 1. Anyone arguing that the Recognition Composition Law alone forces the canonical J-cost cites this as the continuum countermodel. The body is a one-line arithmetic formula; no proof content.
Claim. Define $F_2:\mathbb{R}\to\mathbb{R}$ by $F_2(x)=\frac{x^2+x^{-2}}{2}-1$. This is the $\lambda=2$ member of the cost family $F_\lambda(x)=\frac{x^\lambda+x^{-\lambda}}{2}-1$; its log-coordinate second derivative at the unit equals $4$, not $1$.
background
In Recognition Science the canonical cost is $J(x)=(x+x^{-1})/2-1$ (also written $\cosh(\log x)-1$), forced at T5 of the unified forcing chain once calibration is imposed. The same algebraic skeleton admits a one-parameter family $F_\lambda(x)=(x^\lambda+x^{-\lambda})/2-1$. Each $F_\lambda$ is reciprocal, normalized at $1$, continuous on $(0,\infty)$, and satisfies the Recognition Composition Law $J(xy)+J(x/y)=2J(x)J(y)+2J(x)+2J(y)$ with $J$ replaced by $F_\lambda$.
The module studies native-cost uniqueness on both the rational carrier and its real completion. On the completion the free parameter is the curvature scale $\lambda^2$ at the unit; calibration (the hypothesis IsCalibrated) is what pins $\lambda=1$. The present definition supplies the concrete $\lambda=2$ witness used throughout the non-forcing arguments.
proof idea
Pure definition: expand $(x^2+(x^2)^{-1})/2-1$. No tactics, no lemmas. Downstream proofs treat the resulting function as a closed-form countermodel and discharge reciprocal symmetry, normalization, the composition law, and continuity by direct calculation on this formula.
why it matters
This is the continuum countermodel that makes calibration load-bearing. The parent theorem composition_law_without_calibration_does_not_force_jcost exhibits $F_2$ as a function satisfying every hypothesis of the law-of-logic forcing statement except calibration, yet unequal to canonical $J$. The structural-ledger side uses the same idea: evenPowerGeneratedNativeCost is documented as the carrier analogue of this continuum countermodel, and PRCStructuralSansAnchorUniquenessTarget_refuted shows the anchor-free ledger does not force the canonical cost.
Framework reading (T5 / RCL): algebra alone forces only the family $(x^\lambda+x^{-\lambda})/2-1$; a separate unit calibration selects $\lambda=1$. Whether the recognition defect $\delta$ supplies that unit calibration is the open joint on live track T1. This definition proves the joint is genuine: the composition law does not already imply the unit.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.