E_coh_rs_eq_E_coh
plain-language theorem explainer
Researchers formalizing Recognition Science native units cite this lemma to equate the rung-based coherence energy to its locked counterpart. It confirms that phi to the power of negative five is unambiguous whether the exponent is integer or real. The tactic proof simplifies definitions then bridges the exponent types with rpow_intCast and norm_cast.
Claim. $E_{coh,rs} = E_{coh}$ where both equal the coherence quantum $phi^{-5}$ in RS-native units.
background
The RSNativeUnits module defines a native measurement system with base units tick (discrete time quantum) and voxel (spatial step at c=1), from which the coherence quantum is derived as E_coh = phi^{-5}. The phi-ladder organizes all scalings as phi^n for integer n; phiRung implements this ladder via phi ^ n. cLagLock supplies the canonical locked constant C_lock = phi^{-5} as the reference E_coh. MODULE_DOC states that all dimensionless ratios are fixed by phi alone and that SI conversion remains optional via ExternalCalibration.
proof idea
simp only [E_coh_rs, phiRung, E_coh, cLagLock] reduces both sides to phi raised to -5. A local have establishes phi ^ (-5 : ℤ) = phi ^ (-5 : ℝ) by rw [← Real.rpow_intCast phi (-5)]. Then rw [h], congr 1, and norm_cast finish the goal.
why it matters
The lemma closes the integer-versus-real exponent gap for the coherence quantum that sets hbar = phi^{-5} in RS units. It supports the phi-ladder scaling used throughout the framework (T5 J-uniqueness through T8 D=3) before any external calibration. No downstream uses are recorded, but the equality ensures internal consistency of the native constants module.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.