CausalClosureForced

formal source

  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.
  44    1 AU ≈ 4.85 × 10⁻⁹ kpc, so r_solar/r_0 ≈ 4 × 10⁻¹⁰.
  45    We use the conservative bound r_solar/r_0 < 5 × 10⁻¹⁰. -/
  46def solar_ratio_bound : ℝ := 5e-10
  47
  48/-- The kernel correction at Solar System scales exceeds PPN bounds
  49    when naively extrapolated. This theorem states that the correction
  50    w - 1 = C · (r/r₀)^α is positive for any positive r/r₀ and
  51    positive C, α. No UV cutoff is assumed.
  52
  53    This formalizes the Solar System tension identified in the paper: