balance_at_lambda_0
plain-language theorem explainer
The theorem shows the balance residual, defined as curvature cost minus normalized bit cost, vanishes exactly at the scale lambda_0 = 1/sqrt(2). Researchers deriving the recognition length lambda_rec from curvature-extremum conditions without invoking G would cite this algebraic identity. The proof is a direct term-mode reduction that substitutes the square of lambda_0 and simplifies the resulting quadratic expression.
Claim. Let the balance residual be the function $R(lambda) = 2 lambda^2 - 1$. Then $R(lambda_0) = 0$ where $lambda_0 = 1 / sqrt(2)$.
background
The module derives the recognition length lambda_rec non-circularly from bit cost (=1) and curvature cost (=2 lambda^2) obtained via Q3 Gauss-Bonnet normalization. The balance residual is defined as J_curv(lambda) - J_bit_normalized, where J_bit_normalized is the constant 1 and J_curv(lambda) = 2 lambda^2. The point lambda_0 is introduced as 1/sqrt(2) and shown to satisfy lambda_0^2 = 1/2 by the upstream lemma lambda_0_sq. This setting isolates the curvature-extremum condition before G is recovered as a derived quantity.
proof idea
The term proof unfolds balanceResidual, J_curv, and J_bit_normalized, rewrites the resulting expression with the lemma lambda_0_sq, and finishes with the ring tactic to confirm the quadratic vanishes.
why it matters
The result verifies that lambda_0 solves the balance equation inside the non-circular lambda_rec derivation. It supplies the explicit root used downstream to define G := pi lambda_rec^2 c^3 / hbar and to place lambda_rec on the phi-ladder. The declaration closes the algebraic step that separates curvature cost from bit cost before any gravitational constant enters.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.