lambda_rec_is_root
plain-language theorem explainer
The theorem confirms that the curvature functional K vanishes at the recognition length lambda_rec when the latter equals the native unit ell0. Researchers deriving constants non-circularly in Recognition Science cite this to anchor the balance condition before defining G from it. The proof is a direct algebraic reduction that unfolds the definitions of K, lambda_rec and ell0 then applies simp and ring.
Claim. $K(lambda_rec) = 0$, where $K(lambda) := lambda^2 / lambda_rec^2 - 1$ and $lambda_rec = ell_0 = 1$ in RS-native units.
background
The LambdaRecDerivation module formalizes a non-circular derivation of the recognition length lambda_rec. It uses only the normalized bit cost (=1) and the curvature cost (=2 lambda^2) from the Q3 Gauss-Bonnet normalization, without reference to Newton's constant G. G is then defined as a consequence: G := pi * lambda_rec^2 * c^3 / hbar. The curvature functional K(lambda) is the algebraic restatement of the balance condition, with K(lambda) = 0 precisely when lambda equals lambda_rec.
proof idea
The term proof unfolds K, lambda_rec and ell0, applies simp to reduce one_pow and div_one, then invokes ring to verify the resulting polynomial identity.
why it matters
This result is invoked by the downstream theorem lambda_rec_is_forced to establish existence and uniqueness of the positive root. It supplies the explicit non-circular step that lets the module define G from lambda_rec rather than the reverse, consistent with the eight-tick cycle in which lambda_rec equals ell0 in RS-native units.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.