n_derived

formal source

 100    For now, we define `n_derived` as unity, assuming `xi_derived` handles the
 101    main systematic bias (HSB overprediction). The LSB underprediction might
 102    require tuning `a0` or `C` rather than a separate `n(r)`. -/
 103def n_derived : ℝ := 1
 104
 105/-! ## 5. Theoretical Bounds -/
 106
 107/-- Theorem: HSB Suppression recovers Newtonian limit.
 108    As baryon acceleration goes to infinity, the ILG modification vanishes. -/
 109theorem hsb_suppression_limit (a0 : ℝ) (ha0 : a0 > 0) :
 110    Filter.Tendsto (fun g => xi_derived g a0) Filter.atTop (nhds 0) := by
 111  unfold xi_derived
 112  have h_sat_pos : a_saturation a0 > 0 := by
 113    unfold a_saturation lock_stiffness seven_beat_gap
 114    linarith
 115  -- Rewrite 1/(1+x) as (1+x)⁻¹ to match inv_tendsto_atTop
 116  rw [show (fun g => 1 / (1 + g / a_saturation a0)) = (fun g => (1 + g / a_saturation a0)⁻¹) by ext; simp]
 117  apply Filter.Tendsto.inv_tendsto_atTop
 118  apply Filter.tendsto_atTop_add_const_left
 119  apply Filter.Tendsto.atTop_mul_const (inv_pos.mpr h_sat_pos) Filter.tendsto_id
 120
 121/-- Theorem: LSB Limit is Unsuppressed.
 122    As baryon acceleration goes to zero, the suppression factor goes to 1. -/
 123theorem lsb_unsuppressed_limit (a0 : ℝ) (ha0 : a0 > 0) :
 124    Filter.Tendsto (fun g => xi_derived g a0) (nhds 0) (nhds 1) := by
 125  unfold xi_derived
 126  -- We prove 1 / (1 + g / K) -> 1
 127  -- Rewrite 1 as 1 / (1 + 0 / K)
 128  conv in (nhds 1) => rw [show (1 : ℝ) = 1 / (1 + 0 / a_saturation a0) by
 129    field_simp [a_saturation, lock_stiffness, seven_beat_gap]; linarith]
 130  apply Filter.Tendsto.div
 131  · exact tendsto_const_nhds
 132  · apply Filter.Tendsto.add
 133    · exact tendsto_const_nhds