274lemma E_coh_rs_eq_E_coh : E_coh_rs = E_coh := by
proof body
Tactic-mode proof.
275 simp only [E_coh_rs, phiRung, E_coh, cLagLock] 276 -- Both are phi^(-5), but one uses zpow and the other uses rpow 277 -- φ^(-5 : ℤ) = φ^(-5 : ℝ) for φ > 0 278 have h : phi ^ (-5 : ℤ) = phi ^ ((-5 : ℤ) : ℝ) := by 279 rw [← Real.rpow_intCast phi (-5)] 280 rw [h] 281 congr 1 282 norm_cast 283 284/-! ## External Calibration (SI Bridge) 285 286If you want "seconds" and "meters", you must provide an explicit calibration 287mapping RS primitives to an external unit system. This keeps the empirical 288seam explicit and auditable. 289-/ 290 291/-- External calibration structure for mapping RS units to SI/other systems. -/
depends on (15)
Lean names referenced from this declaration's body.