planck_gate_normalized
plain-language theorem explainer
The normalized Planck gate identity states that c³ λ_rec² equals π ħ G exactly under the Recognition Science definitions. Researchers closing the C8 matching loop between recognition wavelength and gravitational constant would cite this result. The proof is a short tactic sequence that applies the underlying gate identity, confirms the denominator is nonzero via positivity lemmas, and rewrites the division to obtain equality.
Claim. $c^3 λ_rec^2 / (π ħ G) = 1$
background
This theorem lives in the Planck-Scale Matching module, which formalizes Conjecture C8 by equating bit cost J_bit = J(φ) to curvature cost on the Q3 hypercube. The module defines λ_rec via the square root expression sqrt(ħ G / (π c³)) and G via λ_rec² c³ / (π ħ), so the normalized gate is the consistency check that recovers the original relation after substitution. Upstream results include the lambda_rec definition from Bridge.DataCore and the positivity lemmas G_pos, hbar_pos that guarantee the denominator is nonzero.
proof idea
The tactic proof first obtains the un-normalized equality via planck_gate_identity. It then constructs a non-zero proof for π ħ G by successive applications of mul_ne_zero using Real.pi_pos.ne', hbar_pos.ne', and G_pos.ne'. The final steps apply div_eq_one_iff_eq on that non-zero fact and conclude by symmetry of the resulting equality.
why it matters
The declaration closes the Planck-scale matching certificate C8 in the module summary, confirming that the face-averaging factor 1/π is consistently recovered once G is expressed in terms of λ_rec. It anchors the constants block that supplies RS-native values ħ = φ^{-5} and G = φ^5 / π to the forcing chain (T5 J-uniqueness through T8 D=3). The module summary flags the remaining open step: a fully rigorous derivation of the curvature packet J_curv(λ) = 2λ² from the ±4 curvature on Q3 vertices.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.