lambda_rec_unique_root
plain-language theorem explainer
lambda_rec_unique_root establishes that the curvature functional K vanishes precisely when its positive argument equals the recognition length lambda_rec. Derivations of fundamental constants from curvature balance cite this equivalence. The tactic proof reduces K(lambda)=0 algebraically to lambda^2=1, factors the difference of squares, and applies case analysis via mul_eq_zero to discard the negative root.
Claim. For any positive real number $lambda$, $K(lambda)=0$ if and only if $lambda=lambda_rec$, where $K(lambda)=lambda^2/lambda_rec^2-1$ and $lambda_rec$ denotes the fundamental recognition length (equal to the voxel unit ell_0 in RS-native units).
background
The module derives the recognition length non-circularly from normalized bit cost (=1) and curvature cost (=2 lambda^2) under Q3 Gauss-Bonnet normalization, then defines G as a consequence. The curvature functional is introduced as the algebraic restatement K(lambda) := lambda^2 / lambda_rec^2 - 1, with lambda_rec set to ell0 (the fundamental length unit equal to 1 in native units).
proof idea
The proof unfolds K, lambda_rec and ell0, then simplifies powers and divisions. It splits into directions. Forward: K(lambda)=0 yields lambda^2=1 by linarith, factors via nlinarith into (lambda-1)(lambda+1)=0, applies mul_eq_zero from IntegersFromLogic, and concludes lambda=1 by linarith on each branch. Reverse: substitutes the equality and simplifies by ring.
why it matters
The result is invoked directly by the downstream theorem lambda_rec_is_forced, which proves existence and uniqueness of the positive root. It fills the uniqueness step in the non-circular curvature-extremum derivation of lambda_rec described in the module documentation. Within Recognition Science it supports identification of lambda_rec with ell0 inside the eight-tick cycle before G is recovered as pi lambda_rec^2 c^3 / hbar.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.