lambda_rec_unique_root
plain-language theorem explainer
The result shows that the curvature functional K vanishes exactly at the recognition length for any positive real argument. Researchers deriving constants from the non-circular curvature balance would cite this equivalence when confirming the unique positive root. The proof reduces the biconditional to a quadratic equation solved by factoring and linear arithmetic after unfolding the definitions.
Claim. For every real number $λ > 0$, the curvature functional satisfies $K(λ) = 0$ if and only if $λ = λ_{rec}$, where $K(λ) := λ^2 / λ_{rec}^2 - 1$ and $λ_{rec}$ is the fundamental recognition length set to the voxel unit $ℓ_0$.
background
The LambdaRecDerivation module formalizes a non-circular derivation of the recognition length from bit cost normalized to 1 and curvature cost 2λ² drawn from the Q₃ Gauss-Bonnet normalization. G is defined afterward as a consequence rather than an input. In RS-native units the module sets λ_rec := ell0 = 1, so the balance condition becomes algebraic in λ alone.
proof idea
The tactic proof unfolds K, lambda_rec and ell0, then simplifies powers and divisions. It splits the biconditional. The forward direction assumes K(λ)=0, obtains λ²=1, factors the difference of squares, applies mul_eq_zero from IntegersFromLogic, and dispatches both cases with linarith. The reverse direction substitutes the equality and closes with ring.
why it matters
This uniqueness result is invoked by the existence-uniqueness theorem lambda_rec_is_forced later in the module. It completes the algebraic step that lets G be recovered from the curvature extremum without circularity. The declaration sits after the J-uniqueness and phi fixed-point steps in the forcing chain and before the eight-tick octave and D=3 are introduced.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.