lambda_rec_pos
plain-language theorem explainer
Positivity of the recognition length λ_rec holds under the minimal physical assumptions that c, ħ and G are positive. Derivations of G and the uniqueness theorem for the positive root of the forcing equation cite this result. The proof is a direct term-mode reduction that unfolds the square-root definition and chains the standard positivity lemmas for multiplication and division.
Claim. Let $B$ be a BridgeData structure and let $H$ be a Physical $B$, i.e., $0 < B.c$, $0 < B.hbar$ and $0 < B.G$. Then $0 < λ_rec(B)$, where $λ_rec(B) := √(B.hbar ⋅ B.G / (π ⋅ B.c³)).
background
The Bridge.DataCore module supplies the minimal BridgeData structure holding the external anchors G, ħ, c together with display parameters tau0 and ell0. The Physical structure packages the three positivity assumptions on these anchors. The recognition length is defined directly as λ_rec(B) = √(B.hbar * B.G / (π * B.c^3)). This lemma supplies the basic positivity fact required by later constant derivations. Upstream results include the definition of lambda_rec and the Physical structure itself.
proof idea
The proof unfolds lambda_rec and applies Real.sqrt_pos.mpr to reduce to positivity of the argument. It then uses div_pos, which splits into mul_pos on hbar and G (from H) and mul_pos on π and c^3 (using Real.pi_pos and pow_pos on c_pos).
why it matters
This lemma is used by G_pos to derive positivity of G from λ_rec and by lambda_rec_is_forced to establish the unique positive root satisfying the forcing equation. It closes the bridge from Recognition Science constants to the physical length scale λ_rec, supporting the derivation of G = λ_rec² c³ / (π ħ) and the area quantization results that follow.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.