lambda0_forced_in_cost_units
plain-language theorem explainer
Under unit bit-cost normalization, the curvature–bit balance residual has a unique positive root in recognition-cost units, equal to 1/√2. Cite this when packaging the forced recognition length before the native voxel gauge. The proof is a short existence-uniqueness term: exhibit λ₀ with positivity and residual zero, then invoke the residual's unique-positive-root lemma.
Claim. There exists a unique $\lambda > 0$ such that the balance residual vanishes: $J_{\mathrm{curv}}(\lambda) - J_{\mathrm{bit}} = 0$, where $J_{\mathrm{curv}}(\lambda) = 2\lambda^2$ and $J_{\mathrm{bit}} = 1$. Equivalently, $2\lambda^2 = 1$ has unique positive solution $\lambda_0 = 1/\sqrt{2}$ in recognition-cost units.
background
This module formalizes the four-step, parameter-free derivation of the recognition length from the recognition composition law and polyhedral Gauss–Bonnet on the elementary cell $Q_3$. Step (I) forces the cost $J(x) = \tfrac12(x+x^{-1})-1$. Step (II) forces $D=3$ and the cube cell. Step (III) fixes curvature cost from $|\kappa|=4$ quanta on $\partial Q_3\cong S^2$ with area $A=4\pi\lambda^2$, yielding $J_{\mathrm{curv}}(\lambda)=2\lambda^2$.
Step (II) of the cost axis sets the bit cost of one recognition event to the unit $J_{\mathrm{bit}}=1$ (the calibration already fixed by $J''(0)=1$ in cost uniqueness). The balance residual is then $J_{\mathrm{curv}}(\lambda)-1$. Vanishing of that residual is the equilibrium condition whose unique positive root is the recognition length in cost units.
Upstream, residual zero at the explicit root and the iff-characterization of that root among positive reals are already proved; this declaration only packages them as a single $\exists!$ statement.
proof idea
Term-mode $\exists!$ package via refine. Existence witness is the explicit positive root $\lambda_0=1/\sqrt{2}$: positivity and residual vanishing come from the prior lemmas that $\lambda_0>0$ and that the residual is zero there (by unfolding $2\lambda^2-1$ and the identity $\lambda_0^2=1/2$).
Uniqueness: for any positive $\lambda$ with residual zero, the unique-positive-root lemma converts residual vanishing into equality with $\lambda_0$ (algebraically $2\lambda^2=1\Rightarrow\lambda=1/\sqrt{2}$ on $\lambda>0$). No further analysis is needed.
why it matters
This is Step (IV) of the non-circular $\lambda_{\mathrm{rec}}$ chain in the module and in papers/RS_Lambda_Rec_Derivation: after RCL forces $J$ (T5), dimension forcing gives $D=3$ and $Q_3$ (T8), and Gauss–Bonnet gives $J_{\mathrm{curv}}=2\lambda^2$, balance against unit bit cost forces a unique positive cost-unit scale. The next sibling records the RS-native gauge $\lambda_{\mathrm{rec}}=\ell_0=1$ once the voxel length is identified with that root.
The doc-comment caveat is essential for citation: the numeric cost-unit root depends on $J_{\mathrm{bit}}:=1$. Planck-scale matching uses $J_{\mathrm{bit}}=J(\varphi)$ instead and obtains a different cost-unit root; the normalization-independent physics is the SI ratio $\lambda_{\mathrm{rec}}/\ell_P=1/\sqrt{\pi}$ (Planck-gate identity). No downstream theorems currently depend on this package, but it is the derived content the native-unit convention theorem points back to.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.