ballistic_bound

formal source

  10noncomputable section
  11
  12/-- Gap 3 (algebraic core): ballistic causality bound for mode refresh frequency. -/
  13theorem ballistic_bound (k a c : ℝ) (hk : 0 < k) (ha : 0 < a) (hc : 0 < c) :
  14    let lambda_phys := 2 * Real.pi * a / k
  15    let tau_min := lambda_phys / c
  16    let omega_max := 1 / tau_min
  17    omega_max = k * c / (2 * Real.pi * a) := by
  18  intro lambda_phys tau_min omega_max
  19  dsimp [lambda_phys, tau_min, omega_max]
  20  field_simp [hk.ne', ha.ne', hc.ne', Real.pi_ne_zero]
  21
  22/-- Proposition-level interface for A7: causal + scale-free closure. -/
  23structure CausalClosureForced where
  24  /-- Exponent on mode number `k` in `ω_eff ∝ k^β`. -/
  25  beta : ℝ
  26  /-- Exponent on scale factor `a` in `ω_eff ∝ a^(-gamma)`. -/
  27  gamma : ℝ
  28  /-- Dimensional closure result (linear in `k`, inverse in `a`). -/
  29  dimensional_forcing : beta = 1 ∧ gamma = 1
  30
  31/-- Gap 3 packaging: if dimensional forcing holds, closure scaling is fixed. -/
  32theorem scale_free_causal_closure (β γ : ℝ)
  33    (h_dim : β = 1 ∧ γ = 1) :
  34    β = 1 ∧ γ = 1 :=
  35  h_dim
  36
  37/-! ## Solar System scaling bound
  38
  39The editor flagged that naive extrapolation of w(k) gives a ~0.6% correction at 1 AU,
  40far exceeding PPN bounds of ~10⁻⁵. We formalize the honest numerical estimate here
  41so the paper can cite a machine-checked bound. -/
  42
  43/-- The ratio r_solar / r_0 for 1 AU and r_0 = 12 kpc.