lambda_rec_is_forced
plain-language theorem explainer
The theorem asserts existence and uniqueness of a positive real root for the curvature functional K. Workers deriving Newton's constant from Q3 geometry and bit-curvature balance would cite the result to anchor the recognition length. The term-mode proof supplies lambda_rec as witness, checks its positivity and root property, then applies the uniqueness lemma to rule out other candidates.
Claim. There exists a unique positive real number $λ$ such that $K(λ)=0$, where the curvature functional satisfies $K(λ) := λ^2 / λ_rec^2 - 1$.
background
The module derives the recognition length λ_rec non-circularly from the normalized bit cost (=1) and curvature cost (=2λ²) obtained via Gauss-Bonnet normalization on the Q3 cube. The functional K encodes the balance condition whose zero set identifies λ_rec. Upstream, lambda_rec is supplied by Bridge.DataCore as the positive square root satisfying the physical bridge identity, while lambda_rec_pos and lambda_rec_unique_root supply the positivity and uniqueness facts used here.
proof idea
The term proof uses lambda_rec as the witness, applies the constructor to pair lambda_rec_pos with lambda_rec_is_root for existence, then invokes lambda_rec_unique_root on an arbitrary positive root y to obtain uniqueness.
why it matters
The result closes the chain from Q3 cube geometry through curvature quanta and balance to G = φ^5/π and κ=8φ^5. It supplies the non-circular justification for defining G from λ_rec in Constants.G and supports the full forcing sequence from T0 through the eight-tick octave to D=3.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.