extremum_unique
plain-language theorem explainer
The theorem shows that the positive real solving the curvature-bit cost equality must be the explicit square-root expression derived from J_bit. Researchers deriving Planck-scale wavelengths in Recognition Science cite it to lock down uniqueness of the recognition length scale. The proof is a short tactic sequence that unfolds the two cost definitions, applies linear arithmetic to isolate the square, and extracts the positive root via the square-root lemma.
Claim. Let $J_ {curv}(λ) = 2λ^2$ be the curvature cost and $J_{bit} = J(φ)$ the bit cost. If $λ > 0$ and $J_{curv}(λ) = J_{bit}$, then $λ = √(J_{bit}/2)$.
background
In the Planck-Scale Matching module the derivation chain begins with the bit cost $J_{bit} := J(φ) = cosh(ln φ) - 1$, the fundamental ledger transition cost at the self-similar scale. The curvature cost is defined by the physical hypothesis that a ±4 curvature packet distributed over the eight vertices of the Q₃ hypercube yields total cost $J_{curv}(λ) = 2λ^2$. The extremum equation $J_{bit} = J_{curv}(λ)$ is solved explicitly by the definition $λ_{rec} := √(J_{bit}/2)$. The module imports the general J_curv from LambdaRecDerivation and the J functional from PhiForcing to ground these expressions.
proof idea
The tactic proof first unfolds J_curv and lambda_rec_from_Jbit to expose the algebraic relation. Linear arithmetic isolates $λ^2 = J_{bit}/2$. The square-root lemma (sqrt_sq applied to the positive hypothesis) supplies $λ = √(λ^2)$, after which rewriting and exact finish the identification.
why it matters
This uniqueness result closes the extremum step in the Conjecture C8 derivation of λ_rec ≈ 0.564 ℓ_P. It sits inside the larger chain that converts the Recognition Composition Law and the phi fixed point into a concrete Planck ratio via face averaging and the 1/π factor. Because the used-by list is currently empty, the lemma functions as a reusable interface for any later proof that needs to substitute the explicit root back into dimensionful expressions.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.