lambda_0
plain-language theorem explainer
lambda_0 supplies the explicit RS-native balance point 1/sqrt(2) at which normalized bit cost equals curvature cost. Researchers deriving the recognition length non-circularly cite it to locate the unique positive root of the balance residual. The declaration is a direct real-number assignment whose positivity and square are settled by immediate lemmas.
Claim. In RS-native dimensionless units the balance point is defined by $lambda_0 = 1 / sqrt(2)$.
background
The module derives the recognition length non-circularly from the bit cost normalized to 1 and the curvature cost 2 lambda squared that follows from the Q3 Gauss-Bonnet normalization. Newton's constant is recovered afterward by the relation G equals pi times lambda_rec squared times c cubed over hbar. The balance residual is formed as the difference between the curvature functional J_curv(lambda) and the normalized bit cost J_bit_normalized. The upstream result supplies the bare electron-phonon coupling at phi-rung 0, calibrated per material (near 1 for H3S).
proof idea
The declaration is a direct definition assigning 1 over the square root of 2. Companion lemmas lambda_0_pos and lambda_0_sq are obtained by unfolding the definition and applying Real.sqrt_pos together with norm_num arithmetic.
why it matters
The value closes the balance condition J_curv(lambda) equals J_bit_normalized and feeds balance_at_lambda_0 (residual vanishes), balance_determines_lambda (unique positive root), and lambda_rec_is_forced. It realizes the non-circular structure of the LambdaRecDerivation module, supplying the base scale before the phi-ladder and eight-tick octave enter the forcing chain.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.