lambda_rec_dimensionless_id
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.
claimLet $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 in Recognition Science
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.
scope and limits
- Does not prove positivity of λ_rec without the three supplied assumptions.
- Does not evaluate the numerical size of any constant.
- Does not extend the identity to negative or complex values.
- Does not derive the square-root form of λ_rec from deeper axioms.
formal statement (Lean)
39lemma lambda_rec_dimensionless_id (B : BridgeData)
40 (hc : 0 < B.c) (hh : 0 < B.hbar) (hG : 0 < B.G) :
41 (B.c ^ 3) * (lambda_rec B) ^ 2 / (B.hbar * B.G) = 1 / Real.pi := by
proof body
Tactic-mode proof.
42 -- Expand λ_rec and simplify using sqrt and algebra
43 unfold lambda_rec
44 have h_pos : 0 < B.hbar * B.G / (Real.pi * B.c ^ 3) := by
45 apply div_pos (mul_pos hh hG)
46 exact mul_pos Real.pi_pos (pow_pos hc 3)
47 -- Use (sqrt x)^2 = x for x ≥ 0
48 have h_nonneg : 0 ≤ B.hbar * B.G / (Real.pi * B.c ^ 3) := le_of_lt h_pos
49 have hsq : (Real.sqrt (B.hbar * B.G / (Real.pi * B.c ^ 3))) ^ 2 =
50 B.hbar * B.G / (Real.pi * B.c ^ 3) := by
51 simpa using Real.sq_sqrt h_nonneg
52 -- Now simplify the target expression
53 calc
54 (B.c ^ 3) * (Real.sqrt (B.hbar * B.G / (Real.pi * B.c ^ 3))) ^ 2 / (B.hbar * B.G)
55 = (B.c ^ 3) * (B.hbar * B.G / (Real.pi * B.c ^ 3)) / (B.hbar * B.G) := by
56 simp [hsq]
57 _ = ((B.c ^ 3) * (B.hbar * B.G)) / ((Real.pi * B.c ^ 3) * (B.hbar * B.G)) := by
58 field_simp
59 _ = 1 / Real.pi := by
60 field_simp [mul_comm, mul_left_comm, mul_assoc, pow_succ, pow_mul]
61
62/-- Dimensionless identity packaged with a physical-assumptions helper. -/