lambda_0
plain-language theorem explainer
The declaration supplies the numerical value 1/sqrt(2) for the dimensionless balance point where normalized bit cost equals curvature cost 2λ². Researchers deriving the recognition length and then G in the non-circular framework would cite this constant. The definition is a direct assignment with supporting lemmas establishing its square equals 1/2.
Claim. $λ_0 := 1/√2$ denotes the unique positive real satisfying the balance equation between normalized bit cost and curvature cost $2λ²$.
background
The LambdaRecDerivation module obtains the recognition length by equating bit cost (normalized to 1) with curvature cost from Q₃ Gauss-Bonnet normalization. balanceResidual is the difference between J_curv(λ) and J_bit_normalized; the module states that G is then defined as π · λ_rec² · c³ / ℏ without prior reference to Newton's constant. The upstream hydride module supplies a placeholder lambda_0 for e-ph coupling at rung 0, defined simply as the identity on its argument.
proof idea
The declaration is a direct definition assigning 1/Real.sqrt 2. Downstream lemmas lambda_0_sq and lambda_0_pos establish the algebraic properties needed for the ring tactic in balance_at_lambda_0.
why it matters
This definition anchors the non-circular derivation of lambda_rec, which feeds balance_determines_lambda and lambda_rec_is_forced to prove uniqueness of the positive root. It supplies the starting value for the curvature-extremum argument that later yields G, consistent with the Recognition Composition Law and the module's emphasis on logical direction from costs to constants.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.