IndisputableMonolith.TruthCore.Display

   1import Mathlib
   2import IndisputableMonolith.Constants
   3
   4namespace IndisputableMonolith
   5
   6namespace Constants
   7
   8@[simp] noncomputable def RSUnits.tau_rec_display (U : RSUnits) : ℝ := K * U.tau0
   9@[simp] noncomputable def RSUnits.lambda_kin_display (U : RSUnits) : ℝ := K * U.ell0
  10
  11@[simp] theorem RSUnits.display_speed_eq_c (U : RSUnits) :
  12  (RSUnits.lambda_kin_display U) / (RSUnits.tau_rec_display U) = U.c := by
  13  -- K * ℓ0 / (K * τ0) = ℓ0/τ0 = c
  14  have h : (K * U.ell0) / (K * U.tau0) = U.ell0 / U.tau0 := by
  15    by_cases hK : K = 0
  16    · -- If K = 0, both numerator and denominator are 0; use structural identity directly
  17      simp [RSUnits.lambda_kin_display, RSUnits.tau_rec_display, hK]
  18    · -- Cancel common nonzero factor K
  19      have hK0 : K ≠ 0 := hK
  20      have := mul_div_mul_left₀ U.ell0 U.tau0 K hK0
  21      simpa [RSUnits.lambda_kin_display, RSUnits.tau_rec_display, mul_comm, mul_left_comm, mul_assoc]
  22        using this
  23  have hstruct : U.ell0 / U.tau0 = U.c := by
  24    -- from RSUnits structure: ℓ0 = c·τ0
  25    have : U.ell0 = U.c * U.tau0 := U.c_ell0_tau0
  26    simpa [this, div_mul_eq_mul_div, mul_comm, mul_left_comm, mul_assoc] using rfl
  27  simpa [h] using hstruct
  28
  29end Constants
  30
  31namespace TruthCore
  32
  33/-- Alias: display speed identity λ_kin/τ_rec = c. -/
  34theorem display_speed_identity (U : Constants.RSUnits) :
  35  (Constants.RSUnits.lambda_kin_display U) / (Constants.RSUnits.tau_rec_display U) = U.c :=
  36  Constants.RSUnits.display_speed_eq_c U
  37
  38end TruthCore
  39
  40end IndisputableMonolith
  41