balance_unique_positive_root
plain-language theorem explainer
The result states that for any positive real scale parameter lambda the difference between the curvature cost function and the normalized bit cost vanishes if and only if lambda equals the fixed positive constant lambda_0. Researchers deriving the recognition length non-circularly from bit and curvature costs cite this uniqueness statement. The proof reduces the residual equation algebraically to lambda squared equals one half and then invokes square-root identities in both directions under the positivity hypothesis.
Claim. For every real number $lambda > 0$, the equation $J_{curv}(lambda) - J_{bit} = 0$ holds if and only if $lambda = lambda_0$, where $lambda_0$ is the unique positive root of the balance equation.
background
The module derives the recognition length lambda_rec from a non-circular balance between a normalized bit cost fixed at 1 and a curvature cost 2 lambda squared taken from the Q3 Gauss-Bonnet normalization. The balance residual is defined as the difference J_curv(lambda) minus the normalized bit cost; it vanishes precisely at the optimal scale. Upstream results supply the explicit forms of the curvature and bit-cost functions together with the definition of Newton's constant G as a derived quantity pi lambda_rec squared c cubed over hbar.
proof idea
The tactic proof first unfolds the definitions of the residual, the curvature function, the normalized bit cost, and lambda_0. It splits the biconditional. The forward direction uses linarith to obtain lambda squared equals one half, then rewrites via the square-root identity under the positivity assumption. The converse direction substitutes lambda_0, applies the square-root of one half, and simplifies the resulting expression to zero by ring normalization.
why it matters
The theorem is invoked directly by balance_determines_lambda to conclude existence and uniqueness of the positive lambda satisfying J_curv(lambda) equals the normalized bit cost. It thereby completes the central step of the LambdaRecDerivation module that fixes lambda_rec without presupposing G. In the Recognition Science chain this pins the length scale that later defines G and enters the mass ladder and alpha-band calculations.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.