lambda_0_pos
plain-language theorem explainer
The lemma establishes that the RS balance point lambda_0 is strictly positive. Researchers deriving the recognition length from bit-curvature balance cite it to guarantee a positive root exists before invoking uniqueness. The term-mode proof unfolds the explicit definition lambda_0 = 1/sqrt(2) and reduces positivity via div_pos together with the square-root positivity fact for 2.
Claim. $0 < lambda_0$, where $lambda_0 := 1/√2$ is the balance point in RS-native dimensionless units satisfying the bit-curvature equality.
background
The module derives lambda_rec non-circularly from normalized bit cost (=1) and curvature cost (=2 lambda^2) under Q3 Gauss-Bonnet normalization, without reference to G. Lambda_0 is introduced as the explicit positive real solving the balance equation J_bit_normalized = J_curv(lambda). The upstream definition in the same module states: 'The balance point in RS-native dimensionless units' and gives lambda_0 := 1 / Real.sqrt 2. The sibling definition in HydrideSCOptimization is unrelated (an identity map for material calibration).
proof idea
The term proof unfolds lambda_0 to expose 1 / sqrt(2), then applies div_pos to the facts one_pos and sqrt(2) > 0. The latter is obtained directly from Real.sqrt_pos.mpr applied to the norm_num witness 0 < 2.
why it matters
This lemma supplies the positivity hypothesis required by the downstream theorem balance_determines_lambda, which asserts existence of a unique positive lambda satisfying J_curv lambda = J_bit_normalized. It completes the non-circular step in the LambdaRecDerivation module, where G is subsequently defined as pi * lambda_rec^2 * c^3 / hbar. The result sits inside the Recognition Science forcing chain after T5 J-uniqueness and before the phi-ladder mass formula.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.