lambda_0_sq
plain-language theorem explainer
lambda_0 squared equals one half in RS-native dimensionless units. Workers deriving the non-circular lambda_rec from equating bit cost to curvature cost cite this identity to simplify residuals. The proof reduces directly from the explicit definition via unfolding, division-power rewrite, and norm_num after invoking the square-root square identity.
Claim. $lambda_0^2 = 1/2$, where $lambda_0$ is the positive real balance point at which normalized bit cost equals curvature cost $2 lambda^2$.
background
The LambdaRecDerivation module derives the recognition length non-circularly by equating the normalized bit cost (set to 1) with the curvature cost $2 lambda^2$ from Q3 Gauss-Bonnet normalization. The balance point is introduced explicitly as the positive real solving this equality. Upstream definition states lambda_0 : ℝ := 1 / Real.sqrt 2, which supplies the algebraic starting point for all subsequent balance statements.
proof idea
Unfold lambda_0 to expose the division by square root of two. Rewrite via div_pow. Introduce the non-negativity fact (0 : ℝ) ≤ 2. Apply Real.sq_sqrt to replace the squared root with the original argument. Finish with norm_num to obtain the numerical identity 1/2.
why it matters
balance_at_lambda_0 invokes this identity to prove the residual vanishes at lambda_0; balance_determines_lambda uses it to establish uniqueness of the positive root. The step completes the algebraic core of the non-circular lambda_rec derivation, from which G is defined as pi lambda_rec^2 c^3 / hbar. It anchors the curvature functional used throughout the constants layer of the Recognition Science framework.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.