lambda_rec_native_voxel_convention
plain-language theorem explainer
In RS-native units the recognition length equals the voxel length and both equal one: λ_rec = ℓ₀ = 1. Anyone citing the non-circular λ_rec derivation or the Planck-gate definition of G needs this gauge fact. The proof is two reflexivity steps from the definitions λ_rec := ℓ₀ and ℓ₀ := 1.
Claim. Under the RS-native voxel convention, the recognition length equals the fundamental voxel length and both equal unity: $\lambda_{\mathrm{rec}} = \ell_0$ and $\ell_0 = 1$.
background
The module derives λ_rec from the recognition composition law and Q₃ Gauss-Bonnet with no free parameter and no fit to data. The chain forces J from the RCL, sets J_bit := 1 as the cost unit, obtains J_curv(λ) = 2λ² from polyhedral Gauss-Bonnet on ∂Q₃ ≅ S², and solves the balance J_bit = J_curv for the unique positive root λ₀ = 1/√2 in cost units.
After that root is fixed, the canonical voxel definition sets ℓ₀ := λ_rec. In the Constants layer this is recorded by the definitions λ_rec := ℓ₀ and ℓ₀ := 1, so both equal one in RS-native units. The physical content lives in the balance theorems (balance_at_lambda_0, balance_unique_positive_root, lambda0_forced_in_cost_units); the present statement only freezes the subsequent unit gauge.
G is then defined via the Planck-gate identity π ℏ G = c³ λ_rec², so identities such as K(λ_rec) = 0 become tautological once the gauge is chosen.
proof idea
Split the conjunction with constructor. The left conjunct is definitional equality λ_rec := ell0, closed by rfl. The right conjunct is definitional equality ell0 := 1, closed by rfl. No lemmas are invoked.
why it matters
This is the native-unit gauge choice that closes Step (IV) of the λ_rec derivation: after balance forces λ_rec = 1/√2 in cost units, the voxel convention ℓ₀ := λ_rec makes λ_rec = 1 in RS-native units. Downstream infrastructure (the curvature functional K, lambda_rec_is_root, and the Planck-gate form of G) assumes this normalization by name.
It sits after the forcing landmarks T5 (J-uniqueness) and T8 (D = 3), and after the RCL-driven cost balance; it does not itself force φ, the eight-tick octave, or the α band. Used_by is currently empty, so its role is definitional hygiene for the Constants layer and for verification scripts that quote λ_rec = ℓ₀ = 1.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.