import PhysicsLogic.Framework.LowEnergyEffectiveRangeReduction

open Filter PhysicsLogic.Framework.EffectiveRangeExpansion
open scoped Topology

example : ∀ (phase : Real -> Real) (constant quadratic : Real),
    HasFirstTwoCoefficients phase constant quadratic ->
      Tendsto phase (nhdsWithin 0 (Set.Ioi 0)) (𝓝 constant) :=
  @PhysicsLogic.Framework.EffectiveRangeExpansion.HasFirstTwoCoefficients.constant_limit

example : ∀ (phase : Real -> Real) (constant quadratic : Real),
    HasFirstTwoCoefficients phase constant quadratic ↔
      Tendsto phase (nhdsWithin 0 (Set.Ioi 0)) (𝓝 constant) ∧
        Tendsto (fun momentum => (phase momentum - constant) / momentum ^ 2)
          (nhdsWithin 0 (Set.Ioi 0)) (𝓝 quadratic) :=
  PhysicsLogic.Framework.EffectiveRangeExpansion.first_two_coefficients_iff_explicit_limits

-- All former outputs remain consequences of the reduced specification.
example : ∀ (phase : Real -> Real) (inverseLength effectiveRange : Real),
    NonvacuousEffectiveRangeExpansionAt phase inverseLength effectiveRange ↔
      HasQuarticError phase (twoParameterPhaseFunction inverseLength effectiveRange) ∧
        HasFirstTwoCoefficients phase (-inverseLength) (effectiveRange / 2) :=
  PhysicsLogic.Framework.EffectiveRangeExpansion.nonvacuous_expansion_iff_control_and_actual_coefficients

example : ∀ (phase : Real -> Real) (inverseLength effectiveRange : Real),
    NonvacuousEffectiveRangeExpansionAt phase inverseLength effectiveRange ↔
      (∃ radius coefficient : Real, 0 < radius ∧ 0 ≤ coefficient ∧
        ∀ momentum : Real, 0 < momentum -> momentum < radius ->
          |phase momentum - (-inverseLength + effectiveRange / 2 * momentum ^ 2)| ≤
            coefficient * momentum ^ 4) ∧
      Tendsto phase (nhdsWithin 0 (Set.Ioi 0)) (𝓝 (-inverseLength)) ∧
      Tendsto (fun momentum => (phase momentum - (-inverseLength)) / momentum ^ 2)
        (nhdsWithin 0 (Set.Ioi 0)) (𝓝 (effectiveRange / 2)) :=
  fun phase inverseLength effectiveRange =>
    (nonvacuous_expansion_iff_control_and_actual_coefficients
      phase inverseLength effectiveRange).trans
        (and_congr Iff.rfl
          (first_two_coefficients_iff_explicit_limits phase (-inverseLength) (effectiveRange / 2)))

-- Only positive momenta approach threshold; the value at zero stays free.
example :
    let phase : Real -> Real := fun momentum =>
      if 0 < momentum then -3 + 2 * momentum ^ 2 else 42
    HasFirstTwoCoefficients phase (-3) 2 ∧ phase 0 ≠ -3 := by
  dsimp only
  refine ⟨?_, by norm_num⟩
  have positive : ∀ᶠ momentum in approach, 0 < momentum := self_mem_nhdsWithin
  have quotient : (fun momentum : Real =>
      ((if 0 < momentum then -3 + 2 * momentum ^ 2 else 42) - (-3)) / momentum ^ 2)
        =ᶠ[approach] (fun _ => 2) := by
    filter_upwards [positive] with momentum h
    simp only [if_pos h]
    field_simp [ne_of_gt h]
    ring
  exact tendsto_const_nhds.congr' quotient.symm

example : ∀ (phase : Real -> Real) (firstInverse secondInverse firstRange secondRange : Real),
    NonvacuousEffectiveRangeExpansionAt phase firstInverse firstRange ->
    NonvacuousEffectiveRangeExpansionAt phase secondInverse secondRange ->
    firstInverse = secondInverse ∧ firstRange = secondRange :=
  PhysicsLogic.Framework.EffectiveRangeExpansion.the_actual_effective_range_coefficients_are_unique

-- The converse shortcut is still false: matching two coefficients alone
-- does not bound an actual higher-order remainder.
example : HasFirstTwoCoefficients Countermodels.cubicPhase (-3) 2 ∧
    ¬HasQuarticError Countermodels.cubicPhase (twoParameterPhaseFunction 3 4) :=
  PhysicsLogic.Framework.EffectiveRangeExpansion.Countermodels.exact_first_coefficients_do_not_give_quartic_control

#print axioms PhysicsLogic.Framework.EffectiveRangeExpansion.nonvacuous_expansion_iff_control_and_actual_coefficients
#print axioms PhysicsLogic.Framework.EffectiveRangeExpansion.the_actual_effective_range_coefficients_are_unique
#print axioms PhysicsLogic.Framework.EffectiveRangeExpansion.HasFirstTwoCoefficients.constant_limit
#print axioms PhysicsLogic.Framework.EffectiveRangeExpansion.first_two_coefficients_iff_explicit_limits