import PhysicsLogic.Papers.KaplanSavageWise1998

set_option autoImplicit false
set_option backward.isDefEq.respectTransparency false
open Filter PhysicsLogic.Papers.KaplanSavageWise1998
open PhysicsLogic.Framework.EffectiveRangeExpansion
open scoped Topology

noncomputable section

-- Shared data for isolated calibration, coefficient and local RG diagnostics.
-- Unused fit and interpretation routes remain unasserted.
private def data {Momentum : Type} (coordinate : Momentum -> Real)
    (phase : Momentum -> Real) :
    NuclearScatteringFramework Unit Real Momentum (Fin 3) (Fin 4) Int Unit Unit where
  singletChannel := ()
  coupledChannel := ()
  c0 := 0
  c2 := 1
  d2 := 2
  leadingContact := 0
  firstCorrection := 1
  quarkMassContact := 2
  onePionExchange := 3
  leadingOrder := -1
  subleadingOrder := 0
  regimeOf := fun _ _ _ => ()
  powerCounting := {
    contributesAt := fun _ _ _ => False
    noLaterThan := fun left right => left <= right
    suppressedRelativeTo := fun _ _ _ => False
    retainedThrough := fun _ _ => False
    resummedAt := fun _ _ => False
    perturbativeAt := fun _ _ => False }
  AmplitudeValue := Complex
  CouplingValue := Real
  pionlessContactPolynomialValueAt := fun _ mu p => ((-1 / (phase p + mu) : Real) : Complex)
  pionlessPDSLoopValueAt := fun _ _ _ _ => 0
  pionlessPDSAmplitudeValueAt := fun _ _ _ => 0
  formulaOnShellEnergyFamilyRepresentsAt := fun _ => False
  formulaContactPolynomialRepresentsAt := fun _ => False
  pionInclusiveCouplingValueAt := fun _ _ => 0
  pionlessCouplingValueAt := fun _ k mu =>
    if k = 0 then ((-1 / 1000 : Real) - mu)⁻¹
    else if k = 1 then (1 / 2) / ((-1 / 1000 : Real) - mu) ^ 2 else 0
  pionAxialCouplingValue := 0
  pionDecayConstantValue := 1
  pionInclusiveC0 := fun _ => 0
  pionInclusiveC2 := fun _ => 0
  pionInclusiveD2 := fun _ => 0
  subtractionScaleValueAt := id
  nucleonMassValue := 4 * Real.pi
  couplingValueAsReal := id
  momentumValue := coordinate
  scatteringLength := fun _ => -1000
  effectiveRange := fun _ => 1
  momentumTimesPhaseShiftCotangentValueAt := fun _ => phase
  lowMomentumEffectiveRangeExpansionAt := fun _ p => 0 < coordinate p ∧ coordinate p < 1
  fullAmplitudeValueAt := fun _ _ _ => 0
  physicalAmplitudeValue := fun _ _ => 0
  subleadingPionLoopValueAt := fun _ _ _ => 0
  subleadingPionMassInsertionValueAt := fun _ _ _ => 0
  pionMassValue := 1
  truncatedAmplitudeValueWithTermAt := fun _ _ _ _ => 0
  truncatedAmplitudeValueWithoutTermAt := fun _ _ _ _ => 0
  amplitudeExpansionCoefficient := fun value _ => value
  formulaCoupledAmplitudeValueAt := fun _ _ _ _ => 0
  formulaCoupledPhaseObservableValueAt := fun _ _ _ _ => 0
  coupledPhaseCoefficientAvailable := fun _ _ _ => False
  analyticCoupledAmplitudeFormulaProvided := fun _ _ _ => False
  fitUsesCoupledObservable := fun _ _ _ => False
  requiresAdditionalFitParameterAt := fun _ _ _ _ => False
  pionlessMomentum := fun p => 0 < coordinate p ∧ coordinate p < 1
  pionScaleMomentum := fun _ => False
  naturalScatteringLength := fun _ => False
  largeScatteringLength := fun _ => False
  nearThresholdState := fun _ => False
  pdsSubtractionAt := fun _ => False
  pionlessScaleComparisonFactor := 2
  pionlessContactOrderAt := fun _ _ _ _ => 0
  pionlessBubbleLoopOrderAt := fun _ _ => 0
  physicalAmplitudeRequiredScaleIndependent := fun _ _ => False
  ordinaryMSCountingValid := fun _ _ => False
  momentumSmallComparedWithShortRangeScale := fun _ _ => False
  momentumSmallComparedWithInverseScatteringLength := fun _ _ => False
  pionlessLeadingAmplitudeValueAt := fun _ _ _ => 0
  pionlessDerivativeInsertionAmplitudeValueAt := fun _ _ _ => 0
  radiationPionAmplitudeCoefficientAt := fun _ _ _ n => if n = 1 then 1 else 0
  fitUsesNijmegenPhaseShifts := fun _ _ => False
  fitOptimizedThroughTwoHundredMeV := fun _ => False
  leadingCouplingNearLargeLengthValue := fun _ => False
  derivativeCouplingHasExpectedSize := fun _ => False
  singletFitLeadingC0 := fun _ _ => 0
  singletFitFirstC0 := fun _ _ => 0
  singletFitC2 := fun _ _ => 0
  singletFitD2 := fun _ _ => 0
  phaseShiftAgreementGood := fun _ _ => False
  fitSuggestsExpansionValid := fun _ _ => False
  subleadingLeadingRatioAtLeastHalfAboveHundredMeV := fun _ _ => False
  neglectedQuadraticTermsControlledAboveHundredMeV := fun _ _ => False
  coupledPowerCountingAnalogous := fun _ => False

private def phase (p : Real) : Real :=
  if p = 0 then 17 else 1 / 1000 + (1 / 2) * p ^ 2 + p ^ 4

-- Formal coefficient diagnostic, not a nuclear amplitude calculation.
-- The imaginary coordinate stores an allowed higher-order scale variation.
private def coefficientAgreementControl :=
  { data id phase with
    amplitudeExpansionCoefficient := fun value n =>
      if n = 0 then 1 else if n = 1 then (value.re : Complex) else (value.im : Complex)
    truncatedAmplitudeValueWithTermAt := fun _ _ mu _ => (mu : Complex) * Complex.I
    truncatedAmplitudeValueWithoutTermAt := fun _ _ mu _ =>
      (mu : Complex) + (mu : Complex) * Complex.I }

example : coefficientAgreementControl.quarkMassCountertermRequired () 1 ∧
    ¬coefficientAgreementControl.amplitudesAgreeThrough
      (coefficientAgreementControl.truncatedAmplitudeValueWithTermAt 2 () 0 1)
      (coefficientAgreementControl.truncatedAmplitudeValueWithTermAt 2 () 1 1) 2 := by
  constructor
  · rw [NuclearScatteringFramework.quark_mass_counterterm_required_iff_coefficient_witness]
    refine ⟨?_, 0, 1, 1, by norm_num, ?_⟩
    · intro a b n hn
      have cases : n = 0 ∨ n = 1 := by omega
      rcases cases with rfl | rfl <;> simp [coefficientAgreementControl, data]
    · change (((0 : Complex) + 0 * Complex.I).re : Complex) ≠
        (((1 : Complex) + 1 * Complex.I).re : Complex)
      norm_num
  · intro agreement
    have wrong := agreement 2 le_rfl
    change (((0 : Complex) * Complex.I).im : Complex) =
      (((1 : Complex) * Complex.I).im : Complex) at wrong
    norm_num at wrong

-- A retained RG solution near mu=1, not a global continuation or nuclear fit.
private def localPionFlow : PionInclusiveRGFlow :=
  ⟨4 * Real.pi, 1, 1, fun mu => if mu < 2 then 0 else 1,
    fun _ => 0, fun _ => 7⟩

private theorem localPionEquations (mu : Real) (positive : 0 < mu) (below : mu < 2) :
    localPionFlow.RetainedBetaEquationsAt mu := by
  have nearby : localPionFlow.c0 =ᶠ[nhds mu] (fun _ => 0) := by
    filter_upwards [gt_mem_nhds below] with x hx
    simp [localPionFlow, hx]
  have slope := (hasDerivAt_const mu (0 : Real)).congr_of_eventuallyEq nearby
  refine ⟨positive, ?_⟩
  intro kind
  cases kind with
  | c0 => simpa [localPionFlow, PionInclusiveRGFlow.coupling,
      PionInclusiveRGFlow.beta, below] using slope
  | c2 => simpa [localPionFlow, PionInclusiveRGFlow.coupling,
      PionInclusiveRGFlow.beta] using hasDerivAt_const mu (0 : Real)
  | d2 => simpa [localPionFlow, PionInclusiveRGFlow.coupling,
      PionInclusiveRGFlow.beta, below] using hasDerivAt_const mu (7 : Real)

private def localPionData :
    NuclearScatteringFramework Unit Real Real (Fin 3) (Fin 4) Int Unit Unit :=
  { data id phase with
    subtractionScaleValueAt := fun _ => 1
    pionAxialCouplingValue := localPionFlow.axialCoupling
    pionDecayConstantValue := localPionFlow.pionDecayConstant
    pionInclusiveC0 := localPionFlow.c0
    pionInclusiveC2 := localPionFlow.c2
    pionInclusiveD2 := localPionFlow.d2
    pionInclusiveCouplingValueAt := fun k _ => if k = 2 then (7 : Real) else (0 : Real) }

-- A nonempty selected domain has actual open-neighborhood equations. Nothing
-- forces an arbitrary continuation outside it to solve those equations.
example : localPionData.pionInclusiveRGControlledCouplings ∧
    ¬(∀ mu, 0 < mu -> localPionData.pionInclusiveRetainedFlow.RetainedBetaEquationsAt mu) := by
  constructor
  · refine ⟨?_, ⟨0, by norm_num [localPionData]⟩, ?_, ?_⟩
    · change 0 < 4 * Real.pi ∧ 0 < (1 : Real)
      constructor <;> positivity
    · intro scale _positive
      change ∀ᶠ mu in nhds (1 : Real), localPionFlow.RetainedBetaEquationsAt mu
      filter_upwards [lt_mem_nhds (show (0 : Real) < 1 by norm_num),
        gt_mem_nhds (show (1 : Real) < 2 by norm_num)] with mu positive below
      exact localPionEquations mu positive below
    · intro kind scale _positive
      cases kind with
      | c0 =>
        change (if (0 : Fin 3) = 2 then (7 : Real) else 0) =
          (if (1 : Real) < 2 then 0 else 1)
        norm_num [show (0 : Fin 3) ≠ 2 by decide]
      | c2 =>
        change (if (1 : Fin 3) = 2 then (7 : Real) else 0) = 0
        norm_num [show (1 : Fin 3) ≠ 2 by decide]
      | d2 =>
        change (if (2 : Fin 3) = 2 then (7 : Real) else 0) = 7
        norm_num
  · intro globalEquations
    have equation := (globalEquations 3 (by norm_num)).2 .c0
    have nearby : localPionFlow.c0 =ᶠ[nhds (3 : Real)] (fun _ => 1) := by
      filter_upwards [lt_mem_nhds (show (2 : Real) < 3 by norm_num)] with x hx
      simp [localPionFlow, not_lt_of_ge (le_of_lt hx)]
    have slope := (hasDerivAt_const (3 : Real) (1 : Real)).congr_of_eventuallyEq nearby
    have mismatch := equation.unique slope
    norm_num [localPionData, localPionFlow, data, NuclearScatteringFramework.pionInclusiveRetainedFlow,
      PionInclusiveRGFlow.beta, Real.pi_ne_zero] at mismatch

-- Nonzero low-order coefficients with one scale-dependent coefficient.
-- These are formal coefficient diagnostics, not a nuclear amplitude model.
private def coefficientData (degree : Nat) :
    NuclearScatteringFramework Unit Real Real (Fin 3) (Fin 4) Int Unit Unit :=
  { data id phase with
    fullAmplitudeValueAt := fun _ _ _ => (1 : Complex)
    physicalAmplitudeValue := fun _ _ => (1 : Complex)
    truncatedAmplitudeValueWithTermAt := fun _ _ scale _ => (scale : Complex)
    amplitudeExpansionCoefficient := fun (value : Complex) n => if n = degree then value else 1 }

example :
    let f := coefficientData 2
    let expansion := f.pionAmplitudeScaleExpansion () (1 / 2)
    expansion.CompletesAt ∧ f.fullAmplitudeScaleIndependent () (1 / 2) ∧
      expansion.OmittedBeyondSubleadingAt ∧ expansion.ThroughSubleadingAt ∧
      ¬expansion.ExactRetainedScaleIndependentAt ∧ expansion.omitted 3 2 = -2 := by
  dsimp only
  have complete := (coefficientData 2).pion_amplitude_scale_expansion_is_complete () (1 / 2)
  have invariant : (coefficientData 2).fullAmplitudeScaleIndependent () (1 / 2) := by
    intro scale
    rfl
  have low : ((coefficientData 2).pionAmplitudeScaleExpansion () (1 / 2)).OmittedBeyondSubleadingAt := by
    intro scale n retained
    have different : n ≠ 2 := by omega
    simp [NuclearScatteringFramework.pionAmplitudeScaleExpansion, coefficientData, different]
  refine ⟨complete, invariant, low, ?_, ?_, ?_⟩
  · exact ((coefficientData 2).pionAmplitudeScaleExpansion () (1 / 2)).completion_and_full_invariance_derive_computed_order_invariance
      complete low ((coefficientData 2).full_amplitude_invariance_preserves_every_formal_coefficient
        () (1 / 2) invariant)
  · intro exactInvariant
    have mismatch := exactInvariant 1 3 2
    change (1 : Complex) = 3 at mismatch
    norm_num at mismatch
  · change (1 : Complex) - 3 = -2
    norm_num

-- Defining the residual does not make a leading omission higher-order.
example :
    let f := coefficientData 0
    let expansion := f.pionAmplitudeScaleExpansion () (1 / 2)
    expansion.CompletesAt ∧ f.fullAmplitudeScaleIndependent () (1 / 2) ∧
      ¬expansion.OmittedBeyondSubleadingAt ∧ ¬expansion.ThroughSubleadingAt := by
  dsimp only
  refine ⟨(coefficientData 0).pion_amplitude_scale_expansion_is_complete () (1 / 2), ?_, ?_, ?_⟩
  · intro scale
    rfl
  · intro omitted
    have mismatch := omitted 3 0 (by norm_num)
    change (1 : Complex) - 3 = 0 at mismatch
    norm_num at mismatch
  · intro invariant
    have mismatch := invariant 1 3 0 (by norm_num)
    change (1 : Complex) = 3 at mismatch
    norm_num at mismatch

-- Completeness permits a higher-order residual but rejects a retained one,
-- even when full and computed amplitudes agree at the named reference scale.
example : (coefficientData 2).subleadingAmplitudeComplete () 1 (1 / 2) ∧
    (∀ n, (coefficientData 1).amplitudeExpansionCoefficient
      ((coefficientData 1).fullAmplitudeValueAt () 1 (1 / 2)) n =
      (coefficientData 1).amplitudeExpansionCoefficient
        ((coefficientData 1).truncatedAmplitudeValueWithTermAt 2 () 1 (1 / 2)) n) ∧
    ¬(coefficientData 1).subleadingAmplitudeComplete () 1 (1 / 2) := by
  refine ⟨?_, fun _ => rfl, ?_⟩
  · intro scale n retained
    have different : n ≠ 2 := by omega
    simp [coefficientData, different]
  · intro complete
    have mismatch := complete 3 1 (by norm_num)
    change (1 : Complex) = 3 at mismatch
    norm_num at mismatch

private def radiationData (degree : Nat) :=
  { data id phase with
    radiationPionAmplitudeCoefficientAt := fun _ scale _ n => if n = degree then (scale : Complex) else 0 }

-- These formal coefficient controls do not compute radiation-pion graphs.
example : (radiationData 2).radiationPionsAbsentAtSubleadingOrder () (1 / 2) ∧
    (radiationData 2).radiationPionAmplitudeCoefficientAt () 3 (1 / 2) 2 = 3 ∧
    ¬(radiationData 1).radiationPionsAbsentAtSubleadingOrder () (1 / 2) := by
  refine ⟨?_, by norm_num [radiationData], ?_⟩
  · intro scale n retained
    have different : n ≠ 2 := by omega
    simp [radiationData, different]
  · intro absent
    have mismatch := absent 3 1 (by norm_num)
    norm_num [radiationData] at mismatch

private theorem threshold : (data id phase).effectiveRangeDataMatched () := by
  refine ⟨by norm_num [data], ⟨id, ?_⟩, ?_⟩
  · filter_upwards [every_positive_control_radius_contains_the_actual_approach 1 (by norm_num)]
      with p hp
    exact ⟨rfl, hp⟩
  · intro tolerance positive
    refine ⟨min 1 tolerance, lt_min (by norm_num) positive, ?_⟩
    intro p _physical hp small
    change 0 < p at hp
    change p < min 1 tolerance at small
    have normalized : ((phase p - (-(-1000 : Real)⁻¹)) / p ^ 2 - 1 / 2) = p ^ 2 := by
      simp only [phase, if_neg (ne_of_gt hp)]
      norm_num
      field_simp [ne_of_gt hp]
      ring
    change |(phase p - (-(-1000 : Real)⁻¹)) / p ^ 2 - 1 / 2| < tolerance
    rw [normalized, abs_of_nonneg (sq_nonneg p)]
    have lessOne : p < 1 := lt_of_lt_of_le small (min_le_left _ _)
    have lessTolerance : p < tolerance := lt_of_lt_of_le small (min_le_right _ _)
    nlinarith

-- Nonzero residual and finite negative scattering length; zero-momentum
-- values are deliberately not inferred from a punctured threshold limit.
example : (data id phase).effectiveRangeDataMatched () ∧
    phase 0 = 17 ∧ (data id phase).effectiveRangeExpansionRemainderAt () (1 / 2) = 1 / 16 := by
  refine ⟨threshold, by norm_num [phase], ?_⟩
  norm_num [NuclearScatteringFramework.effectiveRangeExpansionRemainderAt, data, phase]

example : Tendsto (fun p => (data id phase).effectiveRangeExpansionRemainderAt () p / p ^ 2)
    approach (nhds 0) := by
  apply (data id phase).effective_range_matching_controls_sampled_remainder () threshold id
  filter_upwards [every_positive_control_radius_contains_the_actual_approach 1 (by norm_num)]
    with p hp
  exact ⟨rfl, hp⟩

private theorem calibrated : (data id phase).PionlessObservableMatchingAt () := by
  have domain : ∀ᶠ p in approach, (data id phase).momentumValue p = p ∧
      (data id phase).lowMomentumEffectiveRangeExpansionAt () p := by
    filter_upwards [every_positive_control_radius_contains_the_actual_approach 1 (by norm_num)]
      with p hp
    exact ⟨rfl, hp⟩
  have observable := (data id phase).effective_range_matching_identifies_observable_coefficients
    () threshold id domain
  norm_num [data] at observable
  refine ⟨?_, id, domain, ?_, ?_⟩
  · change 0 < 4 * Real.pi
    positivity
  · intro mu nonpole
    have hn : (-1 / 1000 : Real) - mu ≠ 0 := by
      change -mu + (-1000 : Real)⁻¹ ≠ 0 at nonpole
      norm_num at nonpole
      convert nonpole using 1 <;> ring
    have observable' : HasFirstTwoCoefficients phase (-(-1 / 1000 : Real)) (1 / 2) := by
      convert observable using 1 <;> norm_num
    have values := (ContactMatching.canonical_contact_coefficients_iff_values
      phase mu (-1 / 1000) (1 / 2) (1 / ((-1 / 1000) - mu))
      ((1 / 2) / ((-1 / 1000) - mu) ^ 2) observable' hn).mpr ⟨rfl, rfl⟩
    simpa [data, Real.pi_ne_zero] using values
  · intro mu _nonpole
    apply Eventually.of_forall
    intro p
    change -1 / (phase p + mu) =
      (4 * Real.pi / (4 * Real.pi)) * (((-1 / (phase p + mu) : Real) : Complex).re)
    rw [div_self (mul_ne_zero (by norm_num) Real.pi_ne_zero), one_mul, Complex.ofReal_re]

-- This same nonzero-residual example reaches the existing RG conclusion.
example : (data id phase).equationElevenPionlessRunningValuesAt () :=
  (data id phase).observable_matching_derives_running_values () threshold calibrated

-- Without actual ERE calibration, totalized real division lets a constant
-- K=0 pass the reduced contact-only contract even at its singular scale.
-- It cannot represent the declared a=1 observable. The reduction must remain
-- conditional, not a standalone equivalence or a physical singular model.
private def singularContact :
    NuclearScatteringFramework Unit Real Real (Fin 3) (Fin 4) Int Unit Unit :=
  { data id (fun _ => 0) with
    scatteringLength := fun _ => 1
    effectiveRange := fun _ => 0
    pionlessCouplingValueAt := fun _ k mu => if k = 0 then -1 / mu else 0 }

private theorem singularDomain : ∀ᶠ p in approach,
    singularContact.momentumValue p = p ∧
      singularContact.lowMomentumEffectiveRangeExpansionAt () p := by
  filter_upwards [every_positive_control_radius_contains_the_actual_approach 1 (by norm_num)]
    with p hp
  exact ⟨rfl, hp⟩

example : singularContact.PionlessObservableMatchingAt () ∧
    ¬singularContact.effectiveRangeDataMatched () ∧
    (singularContact.pionlessRGFlow ()).NonpoleAt 0 ∧
    ¬(∀ᶠ p in approach,
      singularContact.momentumTimesPhaseShiftCotangentValueAt () p + 0 ≠ 0) := by
  letI : approach.NeBot := the_positive_energy_approach_is_nontrivial
  refine ⟨?_, ?_, ?_, ?_⟩
  · refine ⟨?_, id, singularDomain, ?_, ?_⟩
    · change 0 < 4 * Real.pi
      positivity
    · intro mu _nonpole
      simpa [HasFirstTwoCoefficients, singularContact, data, Real.pi_ne_zero] using
        (tendsto_const_nhds : Tendsto (fun _ : Real => (0 : Real)) approach (nhds 0))
    · intro mu _nonpole
      apply Eventually.of_forall
      intro p
      change -1 / (0 + mu) =
        (4 * Real.pi / (4 * Real.pi)) * (((-1 / (0 + mu) : Real) : Complex).re)
      rw [div_self (mul_ne_zero (by norm_num) Real.pi_ne_zero), one_mul, Complex.ofReal_re]
  · intro matching
    have observable := singularContact.effective_range_matching_identifies_observable_coefficients
      () matching id singularDomain
    have observable' : HasFirstTwoCoefficients (fun _ : Real => 0) (-1) 0 := by
      simpa [singularContact, data] using observable
    have impossible : (0 : Real) = -1 := tendsto_nhds_unique tendsto_const_nhds observable'.constant_limit
    norm_num at impossible
  · norm_num [NuclearScatteringFramework.pionlessRGFlow, PionlessRGFlow.NonpoleAt,
      singularContact]
  · intro away
    obtain ⟨p, nonzero⟩ := away.exists
    exact nonzero (by simp [singularContact, data])

-- The same numerical comparison factor controls both boundaries of the
-- selected scale window. Zero and negative momenta are not physical limits
-- of this pointwise predicate, and MS is not an enhanced comparable scale.
example : (data id phase).scaleComparableToMomentum (1 / 4) (1 / 2) ∧
    (data id phase).scaleComparableToMomentum 1 (1 / 2) := by
  norm_num [NuclearScatteringFramework.scaleComparableToMomentum, data]

example : ¬(data id phase).scaleComparableToMomentum 0 (1 / 2) ∧
    ¬(data id phase).scaleComparableToMomentum 0 0 ∧
    ¬(data id phase).scaleComparableToMomentum (-1) (-1) ∧
    ¬(data id phase).scaleComparableToMomentum 3 (1 / 2) := by
  norm_num [NuclearScatteringFramework.scaleComparableToMomentum, data]

-- No fixed finite factor makes a nonzero fixed subtraction scale comparable
-- to every positive momentum. A factor chosen anew at each pair would lose this.
example (factor : Real) :
    ¬∀ p : Real, 0 < p ->
      ({data id phase with pionlessScaleComparisonFactor := factor}).scaleComparableToMomentum 1 p := by
  intro all
  have lower : 1 <= factor := (all 1 (by norm_num)).1
  have denominatorPositive : 0 < 2 * (factor + 1) := by linarith
  have pPositive : 0 < (1 : Real) / (2 * (factor + 1)) := one_div_pos.mpr denominatorPositive
  have upper := (all _ pPositive).2.2.2
  change 1 <= factor * (1 / (2 * (factor + 1))) at upper
  have small : factor * (1 / (2 * (factor + 1))) < 1 := by
    rw [mul_one_div]
    exact (div_lt_one denominatorPositive).2 (by linarith)
  exact (not_lt_of_ge upper) small

-- Comparability alone must not silently supply the separate nonpole domain.
example :
    ({data id phase with scatteringLength := fun _ => 1}).scaleComparableToMomentum 1 1 ∧
      ¬(({data id phase with scatteringLength := fun _ => 1}).pionlessRGFlow ()).NonpoleAt 1 := by
  norm_num [NuclearScatteringFramework.scaleComparableToMomentum,
    NuclearScatteringFramework.pionlessRGFlow, PionlessRGFlow.NonpoleAt, data]

-- The corrected adapter predicate supplies the actual numerical inequalities
-- consumed by the complete controlled-window theorem, not another assigned label.
example {Channel Scale Momentum Coupling Term Order Regime Fit : Type}
    (framework : NuclearScatteringFramework Channel Scale Momentum Coupling Term Order Regime Fit)
    (channel : Channel) (scale : Scale) (momentum : Momentum) (cutoff bound rho epsilon : Real)
    (matching : framework.effectiveRangeDataMatched channel)
    (families : framework.PionlessObservableMatchingAt channel)
    (comparable : framework.scaleComparableToMomentum scale momentum)
    (cutoffPositive : 0 < cutoff)
    (naturalRange : |cutoff * (framework.effectiveRange channel / 2)| <= bound)
    (ratioPositive : 0 < rho)
    (loopWindow : rho ^ 2 + 2 * framework.pionlessScaleComparisonFactor * rho <= 1)
    (precisionPositive : 0 < epsilon) (precisionBelowOne : epsilon < 1)
    (lower : |(framework.scatteringLength channel)⁻¹| / rho < framework.momentumValue momentum)
    (upper : framework.momentumValue momentum < epsilon * cutoff / (bound + 1))
    (formula : (framework.pionlessContactExpansionReadoutAt channel scale momentum).EquationThirteenAt) :
    let readout := framework.pionlessContactExpansionReadoutAt channel scale momentum
    ‖readout.correctionReducedAmplitude‖ < epsilon * ‖readout.leadingReducedAmplitude‖ ∧
      ∀ n : Nat, ‖readout.leadingReducedAmplitude‖ <=
        ‖(Finset.range (n + 1)).sum (fun j =>
            -(readout.scaledLeadingCoupling : Complex) *
              (-(readout.scaledLeadingCoupling : Complex) *
                ((readout.subtractionScale : Complex) + Complex.I * (readout.momentum : Complex))) ^ j) -
          readout.leadingReducedAmplitude‖ := by
  obtain ⟨physical, sample, domain, couplings, _readout⟩ := families
  have observable := framework.effective_range_matching_identifies_observable_coefficients
    channel matching sample domain
  have boundNonnegative : 0 <= bound := (abs_nonneg _).trans naturalRange
  have separation : |(framework.scatteringLength channel)⁻¹| * (bound + 1) <
      rho * epsilon * cutoff := by
    have ordered := (div_lt_div_iff₀ ratioPositive (by linarith : 0 < bound + 1)).mp
      (lower.trans upper)
    nlinarith
  have complete := (framework.pionlessRGFlow channel).observable_matching_realizes_a_controlled_resummation_window
    (fun q => framework.momentumTimesPhaseShiftCotangentValueAt channel (sample q))
    cutoff bound rho framework.pionlessScaleComparisonFactor epsilon physical observable
    couplings cutoffPositive naturalRange ratioPositive
    comparable.1 loopWindow precisionPositive precisionBelowOne separation
  have atPoint := complete.2.2 (framework.momentumValue momentum)
    (framework.subtractionScaleValueAt scale) lower upper comparable.2.2.1 comparable.2.2.2
  have terms := atPoint.2.2
    (framework.pionlessContactExpansionReadoutAt channel scale momentum).leadingReducedAmplitude
    (framework.pionlessContactExpansionReadoutAt channel scale momentum).correctionReducedAmplitude
    ((PionlessContactExpansionReadout.equation_thirteen_iff_local_interaction_equations _).mp formula).2.2
  obtain ⟨_leading, _correction, _relative, precise, _small, _unitary, _linear, _defect, errors⟩ := terms
  exact ⟨precise, fun n => (errors n).2⟩

-- The reconstruction identity is compatible with a wrong effective range.
-- The new matching condition must reject it, even though the old identity holds.
private def wrongPhase (p : Real) : Real := 1 / 1000 + p ^ 2

example : (∀ p, wrongPhase p = (data id wrongPhase).effectiveRangeExpansionValueAt () p) ∧
    ¬(data id wrongPhase).effectiveRangeDataMatched () := by
  refine ⟨fun p => (data id wrongPhase).effective_range_remainder_reconstructs_observable () p, ?_⟩
  intro matched
  obtain ⟨radius, positive, estimate⟩ := matched.2.2 (1 / 4) (by norm_num)
  let p := min radius 1 / 2
  have hp : 0 < p := by dsimp [p]; positivity
  have lessRadius : p < radius := by
    have := min_le_left radius 1
    dsimp [p]
    nlinarith
  have lessOne : p < 1 := by
    have := min_le_right radius 1
    dsimp [p]
    nlinarith
  have bad := estimate p ⟨hp, lessOne⟩ hp lessRadius
  change |(wrongPhase p - (-(-1000 : Real)⁻¹)) / p ^ 2 - 1 / 2| < 1 / 4 at bad
  have normalized : (wrongPhase p - (-(-1000 : Real)⁻¹)) / p ^ 2 - 1 / 2 = 1 / 2 := by
    norm_num [wrongPhase]
    field_simp
    ring
  rw [normalized] at bad
  norm_num at bad

-- Selecting only the first of two conflicting momentum labels cannot
-- establish matching for the same physical threshold domain.
private def aliasedPhase (p : Bool × Real) : Real :=
  1 / 1000 + (if p.1 then 1 else 1 / 2) * p.2 ^ 2

example :
    HasFirstTwoCoefficients (fun p => aliasedPhase (false, p)) (1 / 1000) (1 / 2) ∧
      ¬(data Prod.snd aliasedPhase).effectiveRangeDataMatched () := by
  refine ⟨?_, ?_⟩
  · apply (tendsto_const_nhds : Tendsto (fun _ : Real => (1 / 2 : Real)) approach (nhds (1 / 2))).congr'
    have positive : ∀ᶠ p in approach, 0 < p := self_mem_nhdsWithin
    filter_upwards [positive] with p hp
    simp only [aliasedPhase, Bool.false_eq_true, ↓reduceIte, add_sub_cancel_left]
    field_simp
  · intro matched
    have coefficients := (data Prod.snd aliasedPhase).effective_range_matching_identifies_observable_coefficients
      () matched (fun p => (true, p)) (by
        filter_upwards [every_positive_control_radius_contains_the_actual_approach 1 (by norm_num)]
          with p hp
        exact ⟨rfl, hp⟩)
    have actual : HasFirstTwoCoefficients (fun p => aliasedPhase (true, p)) (1 / 1000) 1 := by
      apply (tendsto_const_nhds : Tendsto (fun _ : Real => (1 : Real)) approach (nhds 1)).congr'
      have positive : ∀ᶠ p in approach, 0 < p := self_mem_nhdsWithin
      filter_upwards [positive] with p hp
      simp only [aliasedPhase, ↓reduceIte, one_mul, add_sub_cancel_left]
      field_simp
    letI : approach.NeBot := the_positive_energy_approach_is_nontrivial
    norm_num [data] at coefficients
    have contradiction := tendsto_nhds_unique actual coefficients
    norm_num at contradiction

-- Zero scattering length is outside this finite inverse-amplitude chart.
example : ¬({data id phase with scatteringLength := fun _ => 0}).effectiveRangeDataMatched () := by
  intro matched
  exact matched.1 rfl

-- An inhabited momentum type with an empty selected domain cannot count
-- as an observed threshold family.
example : ¬({data id phase with lowMomentumEffectiveRangeExpansionAt := fun _ _ => False}).effectiveRangeDataMatched () := by
  rintro ⟨_, ⟨sample, domain⟩, _⟩
  letI : approach.NeBot := the_positive_energy_approach_is_nontrivial
  obtain ⟨p, hp⟩ := domain.exists
  exact hp.2

#print axioms NuclearScatteringFramework.effective_range_matching_iff_uniform_remainder
#print axioms NuclearScatteringFramework.effective_range_matching_identifies_observable_coefficients
#print axioms NuclearScatteringFramework.effective_range_matching_controls_sampled_remainder
#print axioms NuclearScatteringFramework.observable_matching_derives_running_values
#print axioms NuclearScatteringFramework.scale_comparison_iff_fixed_ratio_bounds
#print axioms NuclearScatteringFramework.scale_comparison_excludes_minimal_subtraction

end