lambda_rec_dimensionless_id
plain-language theorem explainer
The lemma shows that for any BridgeData B with positive c, ħ and G the combination (c³ λ_rec²) / (ħ G) equals 1/π, where λ_rec is the square-root expression built from those anchors. Bridge-module users checking dimensional consistency of the recognition length cite this identity directly. The tactic proof unfolds the definition, confirms the radicand is nonnegative, replaces the squared square root by the original argument, and cancels via field_simp.
Claim. Let $B$ be a BridgeData structure with $0 < c$, $0 < ħ$ and $0 < G$. Then $c^3 λ_{rec}(B)^2 / (ħ G) = 1/π$, where $λ_{rec}(B) := √(ħ G / (π c^3))$.
background
BridgeData is a plain structure supplying the external anchors G, ħ, c, τ₀ and ℓ₀ with no axioms. The recognition length is defined inside the same module as λ_rec(B) = √(ħ G / (π c³)). The module isolates this core identity so the certified import closure remains small and excludes larger subsystems such as Core.
proof idea
Unfold lambda_rec to expose the square root. Prove the radicand is positive from the three assumptions, then nonnegative. Apply Real.sq_sqrt to obtain (√x)² = x. Finish with a calc block that substitutes the squared term and reduces the resulting rational expression to 1/π by repeated field_simp.
why it matters
The result is the direct parent of lambda_rec_dimensionless_id_physical, which re-packages the identity under the Physical hypothesis. It closes the loop with the RS-native constants (G = λ_rec² c³ / (π ħ)) and anchors the recognition wavelength inside the eight-tick cycle. No open scaffolding remains.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.