K
plain-language theorem explainer
The curvature functional K(λ) is defined by the algebraic expression λ²/λ_rec² - 1. Researchers working on the non-circular derivation of the recognition length from bit cost and curvature cost would cite this restatement. It is a direct one-line definition with no lemmas or reductions.
Claim. The curvature functional is defined by $K(λ) = λ² / λ_rec² - 1$.
background
This module derives λ_rec non-circularly from the normalized bit cost (=1) and curvature cost (=2λ²) under Q₃ Gauss-Bonnet normalization, without presupposing Newton's G. G is then defined as the consequence G := π · λ_rec² · c³ / ℏ. The functional K(λ) algebraically restates the balance condition K(λ)=0 iff λ=λ_rec. Upstream, lambda_rec from Bridge.DataCore supplies the physical expression √(ħG/c³), while Constants.lambda_rec sets it to ell0 in RS-native units and RGTransport.lambda supplies λ = ln(φ).
proof idea
This is a direct definition of K as the expression lambda ^ 2 / lambda_rec ^ 2 - 1. No lemmas are applied.
why it matters
This definition supports the non-circular λ_rec derivation that yields G as a consequence, feeding into downstream results such as defectDist_no_global_quasi_triangle in CostAlgebra and ballP constructions in Causality. The module doc states it is retained for backward compatibility with verification infrastructure. It aligns with the T5 J-uniqueness and T6 phi fixed-point steps in the forcing chain.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.