balanceResidual
plain-language theorem explainer
The balance residual subtracts the normalized bit cost from the quadratic curvature cost at scale lambda. Derivations of the recognition length lambda_rec as the curvature extremum cite this definition to locate the zero. It is introduced as the direct difference of the two cost functions without further computation.
Claim. $R(lambda) := 2 lambda^2 - 1$, where the curvature cost is $J_{curv}(lambda) = 2 lambda^2$ and the bit cost is the constant 1.
background
The module derives the recognition length lambda_rec non-circularly from the unit bit cost and the curvature cost 2 lambda squared. J_bit_normalized is defined as the bit cost of one recognition event normalized to 1. J_curv(lambda) is the curvature cost of embedding one recognition token at scale lambda, obtained from four curvature quanta on Q3, Gauss-Bonnet normalization on S2 with Euler characteristic 2, and bounding area 4 pi lambda squared, yielding exactly 2 lambda squared.
proof idea
One-line definition that subtracts J_bit_normalized from J_curv lambda.
why it matters
This definition supplies the residual whose zero is established by the downstream theorems balance_at_lambda_0 and balance_unique_positive_root. It completes the non-circular step in the LambdaRecDerivation module, where G is later recovered as pi lambda_rec squared times c cubed over hbar. The construction aligns with the J-cost framework and the curvature-extremum route to lambda_rec.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.