balance_determines_lambda
plain-language theorem explainer
The theorem asserts existence of a unique positive real lambda where curvature cost equals normalized bit cost. Researchers deriving Newton's constant from Q3 geometry cite this as the balance step. The proof exhibits lambda_0 as witness and applies the upstream uniqueness theorem for the residual equation after algebraic verification.
Claim. There exists a unique positive real number $lambda$ such that the curvature cost $J_{curv}(lambda) = 2 lambda^2$ equals the normalized bit cost $J_{bit normalized} = 1$.
background
The LambdaRecDerivation module formalizes a non-circular derivation of the recognition length lambda_rec. It uses only the bit cost normalized to 1 and the curvature cost 2 lambda squared obtained from Q3 Gauss-Bonnet normalization, without presupposing G. J_curv(lambda) is defined as 2 lambda squared, the curvature cost of embedding one recognition token at scale lambda, derived from 4 curvature quanta on Q3, Gauss-Bonnet on S2 with chi=2, and bounding area 4 pi lambda squared. J_bit_normalized is the bit cost of one recognition event set to 1. The upstream theorem balance_unique_positive_root establishes that lambda_0 is the unique positive root of the balance residual J_curv(lambda) minus J_bit_normalized.
proof idea
The proof is a one-line wrapper that applies balance_unique_positive_root. It uses lambda_0 as the candidate, refines the existence pair with lambda_0_pos and algebraic simplification via unfold and ring, then proves uniqueness by showing the residual vanishes and invoking the root uniqueness theorem with linarith.
why it matters
This supplies step 4 (balance_unique) in the G derivation chain certificate, which assembles Q3 combinatorics, Gauss-Bonnet total curvature 4 pi, the J_curv formula, this uniqueness result, and the G definition to reach kappa = 8 phi^5. It realizes the module's non-circular structure and feeds directly into G_derivation_chain_complete. The step aligns with T5 J-uniqueness from the forcing chain and closes the path from geometry to the gravitational constant in RS-native units.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.