import PhysicsLogic.Papers.KaplanSavageWise1998

open PhysicsLogic.Paradigm
open PhysicsLogic.Papers.KaplanSavageWise1998
open ContactPowerCounting

example {Term Order Regime : Type} :
    ∀ (c : EffectiveTheory.PowerCountingContext Term Order Regime)
      (vertex : Nat -> Term) (exponent : Int -> Order) (r : Regime)
      (couplings : Nat -> Int) (loop : Int),
    (couplings 0 = -1 ∧ couplings 1 = -2 ∧
      (∀ n, 2 <= n -> 1 <= couplings n + 2 * (n : Int))) → loop = 1 →
    InterpretsContactCountingAt c vertex exponent r couplings loop →
      c.contributesAt (vertex 0) r (exponent (-1)) ∧
      c.retainedThrough (vertex 0) (exponent (-1)) ∧
      c.retainedThrough (vertex 0) (exponent 0) ∧
      c.resummedAt (vertex 0) r ∧ ¬c.perturbativeAt (vertex 0) r ∧
      c.contributesAt (vertex 1) r (exponent 0) ∧
      c.retainedThrough (vertex 1) (exponent 0) ∧ c.perturbativeAt (vertex 1) r :=
  PhysicsLogic.Papers.KaplanSavageWise1998.ContactPowerCounting.diagram_interpretation_derives_mixed_treatments

-- Every former output remains available from the stronger source assignment.
example {Term Order Regime : Type} :
    ∀ (c : EffectiveTheory.PowerCountingContext Term Order Regime)
      (vertex : Nat -> Term) (exponent : Int -> Order) (r : Regime)
      (couplings : Nat -> Int) (loop : Int),
    (∀ n, couplings n = -((n : Int) + 1)) → loop = 1 →
    InterpretsContactCountingAt c vertex exponent r couplings loop →
      c.contributesAt (vertex 0) r (exponent (-1)) ∧
      c.retainedThrough (vertex 0) (exponent (-1)) ∧
      c.retainedThrough (vertex 0) (exponent 0) ∧
      c.resummedAt (vertex 0) r ∧ ¬c.perturbativeAt (vertex 0) r ∧
      c.contributesAt (vertex 1) r (exponent 0) ∧
      c.retainedThrough (vertex 1) (exponent 0) ∧ c.perturbativeAt (vertex 1) r := by
  intro c vertex exponent r couplings loop source loopOrder interpretation
  exact diagram_interpretation_derives_mixed_treatments c vertex exponent r couplings loop
    ⟨by simpa using source 0, by simpa using source 1,
      fun n hn => by rw [source n]; omega⟩ loopOrder interpretation

-- The interpretation is inhabited. The unused comparison/suppression fields
-- below only compare nominal derivative degree; no physical soundness is claimed.
example : ∃ c : EffectiveTheory.PowerCountingContext Nat Int Unit,
    InterpretsContactCountingAt c id id () (fun n => -((n : Int) + 1)) 1 := by
  refine ⟨{
    contributesAt := fun n _ q => -((n : Int) + 1) + 2 * (n : Int) = q
    noLaterThan := fun q s => q ≤ s
    suppressedRelativeTo := fun _ n m => m < n
    retainedThrough := fun n q => ∃ v : List Nat, v ≠ [] ∧ n ∈ v ∧
      momentumOrder (fun k => -((k : Int) + 1)) 1 v ≤ q
    resummedAt := fun n _ => ∀ bound : Nat, ∃ v : List Nat, v ≠ [] ∧
      momentumOrder (fun k => -((k : Int) + 1)) 1 v ≤ 0 ∧ bound < v.count n
    perturbativeAt := fun n _ => ∃ bound : Nat, ∀ v : List Nat, v ≠ [] →
      momentumOrder (fun k => -((k : Int) + 1)) 1 v ≤ 0 → v.count n ≤ bound },
    fun _ _ _ => Iff.rfl, fun _ _ _ => Iff.rfl, fun _ => Iff.rfl, fun _ => Iff.rfl⟩

-- The same interpretation with natural contact orders does not require C0
-- resummation. The explicit enhanced exponents are doing essential work.
example : ∃ c : EffectiveTheory.PowerCountingContext Nat Int Unit,
    InterpretsContactCountingAt c id id () (fun _ => 0) 1 ∧ ¬c.resummedAt 0 () := by
  let c : EffectiveTheory.PowerCountingContext Nat Int Unit := {
    contributesAt := fun n _ q => (0 : Int) + 2 * (n : Int) = q
    noLaterThan := fun q s => q ≤ s
    suppressedRelativeTo := fun _ n m => m < n
    retainedThrough := fun n q => ∃ v : List Nat, v ≠ [] ∧ n ∈ v ∧
      momentumOrder (fun _ => 0) 1 v ≤ q
    resummedAt := fun n _ => ∀ bound : Nat, ∃ v : List Nat, v ≠ [] ∧
      momentumOrder (fun _ => 0) 1 v ≤ 0 ∧ bound < v.count n
    perturbativeAt := fun n _ => ∃ bound : Nat, ∀ v : List Nat, v ≠ [] →
      momentumOrder (fun _ => 0) 1 v ≤ 0 → v.count n ≤ bound }
  refine ⟨c, ⟨fun _ _ _ => Iff.rfl, fun _ _ _ => Iff.rfl,
    fun _ => Iff.rfl, fun _ => Iff.rfl⟩, ?_⟩
  intro unbounded
  obtain ⟨v, _nonempty, retained, exceeds⟩ := unbounded 1
  have lengthBound := natural_counting_bounds_loop_count v 0 retained
  have countBound := List.count_le_length (a := 0) (l := v)
  omega

-- Strict reduction of the actual treatment theorem: all eight conclusions
-- hold with natural orders for excluded higher contacts. This is a diagram
-- interface witness, not a nuclear model or a claim about numerical amplitudes.
example : ∃ (c : EffectiveTheory.PowerCountingContext Nat Int Unit)
    (couplings : Nat -> Int),
    InterpretsContactCountingAt c id id () couplings 1 ∧
    (c.contributesAt 0 () (-1) ∧ c.retainedThrough 0 (-1) ∧ c.retainedThrough 0 0 ∧
      c.resummedAt 0 () ∧ ¬c.perturbativeAt 0 () ∧
      c.contributesAt 1 () 0 ∧ c.retainedThrough 1 0 ∧ c.perturbativeAt 1 ()) ∧
    ¬(∀ n, couplings n = -((n : Int) + 1)) := by
  let couplings : Nat -> Int := fun n => if n = 0 then -1 else if n = 1 then -2 else 0
  let c : EffectiveTheory.PowerCountingContext Nat Int Unit := {
    contributesAt := fun n _ q => couplings n + 2 * (n : Int) = q
    noLaterThan := fun q s => q ≤ s
    suppressedRelativeTo := fun _ n m => m < n
    retainedThrough := fun n q => ∃ v : List Nat, v ≠ [] ∧ n ∈ v ∧
      momentumOrder couplings 1 v ≤ q
    resummedAt := fun n _ => ∀ bound : Nat, ∃ v : List Nat, v ≠ [] ∧
      momentumOrder couplings 1 v ≤ 0 ∧ bound < v.count n
    perturbativeAt := fun n _ => ∃ bound : Nat, ∀ v : List Nat, v ≠ [] →
      momentumOrder couplings 1 v ≤ 0 → v.count n ≤ bound }
  have interpretation : InterpretsContactCountingAt c id id () couplings 1 :=
    ⟨fun _ _ _ => Iff.rfl, fun _ _ _ => Iff.rfl, fun _ => Iff.rfl, fun _ => Iff.rfl⟩
  have orders : couplings 0 = -1 ∧ couplings 1 = -2 ∧
      (∀ n, 2 <= n -> 1 <= couplings n + 2 * (n : Int)) := by
    refine ⟨by norm_num [couplings], by norm_num [couplings], ?_⟩
    intro n high
    simp only [couplings, if_neg (by omega : n ≠ 0), if_neg (by omega : n ≠ 1), zero_add]
    omega
  refine ⟨c, couplings, interpretation,
    diagram_interpretation_derives_mixed_treatments c id id () couplings 1 orders rfl interpretation,
    ?_⟩
  intro exactOrders
  have wrong := exactOrders 2
  norm_num [couplings] at wrong

-- Grading an interaction by every chain containing it forces self-suppression
-- if the shared strict-order soundness law is applied. This exposes a type-role
-- mismatch, not a failure of KSW's physical expansion or numerical convergence.
example {Term Order Regime : Type}
    (c : EffectiveTheory.PowerCountingContext Term Order Regime)
    (vertex : Nat -> Term) (exponent : Int -> Order) (r : Regime)
    (old : ∀ n q (_ : q <= 0), c.contributesAt (vertex n) r (exponent q) ↔
      ∃ v : List Nat, v ≠ [] ∧ n ∈ v ∧
        momentumOrder (fun j => -((j : Int) + 1)) 1 v = q)
    (ordered : c.noLaterThan (exponent (-1)) (exponent 0))
    (strict : ¬c.noLaterThan (exponent 0) (exponent (-1)))
    (sound : c.SoundAt r) : c.suppressedRelativeTo r (vertex 0) (vertex 0) := by
  have leading := (old 0 (-1) (by omega)).mpr
    ⟨[0], by simp, by simp, by norm_num [momentumOrder]⟩
  have dressed := (old 0 0 le_rfl).mpr
    ⟨[0, 1], by simp, by simp, by norm_num [momentumOrder]⟩
  exact sound (vertex 0) (vertex 0) (exponent (-1)) (exponent 0)
    leading dressed ordered strict

-- The former all-order interpretation forced distinct labels for every
-- derivative contact, even though the source conclusion stops at order zero.
-- This preserves the historical full-to-scoped implication literally. It is
-- not an implication to the corrected vertex-grade interpretation.
example {Term Order Regime : Type}
    (c : EffectiveTheory.PowerCountingContext Term Order Regime)
    (vertex : Nat -> Term) (exponent : Int -> Order) (r : Regime)
    (couplings : Nat -> Int) (loop : Int)
    (old : (∀ n q, c.contributesAt (vertex n) r (exponent q) ↔
        ∃ v : List Nat, v ≠ [] ∧ n ∈ v ∧ momentumOrder couplings loop v = q) ∧
      (∀ n q, c.retainedThrough (vertex n) (exponent q) ↔
        ∃ v : List Nat, v ≠ [] ∧ n ∈ v ∧ momentumOrder couplings loop v ≤ q) ∧
      (∀ n, c.resummedAt (vertex n) r ↔ ∀ bound : Nat, ∃ v : List Nat, v ≠ [] ∧
        momentumOrder couplings loop v ≤ 0 ∧ bound < v.count n) ∧
      (∀ n, c.perturbativeAt (vertex n) r ↔ ∃ bound : Nat, ∀ v : List Nat, v ≠ [] →
        momentumOrder couplings loop v ≤ 0 → v.count n ≤ bound)) :
    (∀ n q (_ : q <= 0), c.contributesAt (vertex n) r (exponent q) ↔
      ∃ v : List Nat, v ≠ [] ∧ n ∈ v ∧ momentumOrder couplings loop v = q) ∧
    (∀ n q (_ : q <= 0), c.retainedThrough (vertex n) (exponent q) ↔
      ∃ v : List Nat, v ≠ [] ∧ n ∈ v ∧ momentumOrder couplings loop v <= q) ∧
    (∀ n, c.resummedAt (vertex n) r ↔ ∀ bound : Nat, ∃ v : List Nat, v ≠ [] ∧
      momentumOrder couplings loop v <= 0 ∧ bound < v.count n) ∧
    (∀ n, c.perturbativeAt (vertex n) r ↔ ∃ bound : Nat, ∀ v : List Nat, v ≠ [] →
      momentumOrder couplings loop v <= 0 → v.count n <= bound) :=
  ⟨fun n q _ => old.1 n q, fun n q _ => old.2.1 n q, old.2.2⟩

private theorem unrestricted_contributions_force_injective_contact_labels
    {Term Order Regime : Type}
    (c : EffectiveTheory.PowerCountingContext Term Order Regime)
    (vertex : Nat -> Term) (exponent : Int -> Order) (r : Regime)
    (interpretation : ∀ n q, c.contributesAt (vertex n) r (exponent q) ↔
      ∃ v : List Nat, v ≠ [] ∧ n ∈ v ∧
        momentumOrder (fun j => -((j : Int) + 1)) 1 v = q) :
    Function.Injective vertex := by
  have ordered : ∀ n m, vertex n = vertex m -> n <= m := by
    intro n m labels
    have singleton : c.contributesAt (vertex m) r (exponent ((m : Int) - 1)) :=
      (interpretation m _).mpr ⟨[m], by simp, by simp, by simp [momentumOrder]; omega⟩
    rw [← labels] at singleton
    obtain ⟨v, nonempty, member, order⟩ := (interpretation n _).mp singleton
    rw [enhanced_order_counts_derivatives_not_leading_bubbles v nonempty] at order
    have leSum := List.le_sum_of_mem member
    omega
  intro n m labels
  exact Nat.le_antisymm (ordered n m labels) (ordered m n labels.symm)

-- A three-label interface is sufficient: C0, C2, and contacts excluded
-- through this order. The actual chain still retains every derivative index.
-- The same data realizes every original mixed-treatment conclusion while
-- falsifying the former all-order contribution interpretation.
example : ∃ (c : EffectiveTheory.PowerCountingContext (Fin 3) Int Unit)
    (vertex : Nat -> Fin 3),
    InterpretsContactCountingAt c vertex id () (fun n => -((n : Int) + 1)) 1 ∧
    (c.contributesAt (vertex 0) () (-1) ∧
      c.retainedThrough (vertex 0) (-1) ∧ c.retainedThrough (vertex 0) 0 ∧
      c.resummedAt (vertex 0) () ∧ ¬c.perturbativeAt (vertex 0) () ∧
      c.contributesAt (vertex 1) () 0 ∧ c.retainedThrough (vertex 1) 0 ∧
      c.perturbativeAt (vertex 1) ()) ∧
    (∀ n, 2 <= n -> ¬c.retainedThrough (vertex n) 0) ∧
    c.NonvacuousSoundAt () ∧
    (∀ term, ¬c.suppressedRelativeTo () term term) ∧
    ¬c.contributesAt (vertex 0) () 0 ∧
    ¬(∀ n q, c.contributesAt (vertex n) () q ↔
      ∃ v : List Nat, v ≠ [] ∧ n ∈ v ∧
        momentumOrder (fun j => -((j : Int) + 1)) 1 v = q) := by
  let vertex : Nat -> Fin 3 := fun n => ⟨min n 2, by omega⟩
  let c : EffectiveTheory.PowerCountingContext (Fin 3) Int Unit := {
    contributesAt := fun n _ q => (n.val : Int) - 1 = q
    noLaterThan := fun q s => q ≤ s
    suppressedRelativeTo := fun _ n m => m.val < n.val
    retainedThrough := fun n q => ∃ v : List Nat, v ≠ [] ∧ n.val ∈ v ∧
      momentumOrder (fun j => -((j : Int) + 1)) 1 v ≤ q
    resummedAt := fun n _ => ∀ bound : Nat, ∃ v : List Nat, v ≠ [] ∧
      momentumOrder (fun j => -((j : Int) + 1)) 1 v ≤ 0 ∧ bound < v.count n.val
    perturbativeAt := fun n _ => ∃ bound : Nat, ∀ v : List Nat, v ≠ [] →
      momentumOrder (fun j => -((j : Int) + 1)) 1 v ≤ 0 → v.count n.val ≤ bound }
  have small : ∀ v : List Nat, v ≠ [] ->
      momentumOrder (fun j => -((j : Int) + 1)) 1 v <= 0 ->
      ∀ n, n ∈ v -> n <= 1 := by
    intro v nonempty order n member
    rw [enhanced_order_counts_derivatives_not_leading_bubbles v nonempty] at order
    have leSum := List.le_sum_of_mem member
    omega
  have members : ∀ v : List Nat, v ≠ [] ->
      momentumOrder (fun j => -((j : Int) + 1)) 1 v <= 0 ->
      ∀ n, (vertex n).val ∈ v ↔ n ∈ v := by
    intro v nonempty retained n
    by_cases low : n <= 1
    · simp [vertex, Nat.min_eq_left (by omega : n <= 2)]
    · have original : n ∉ v := fun h => low (small v nonempty retained n h)
      have folded : (vertex n).val ∉ v := by
        simp only [vertex, Nat.min_eq_right (by omega : 2 <= n)]
        intro h
        have := small v nonempty retained 2 h
        omega
      simp [original, folded]
  have counts : ∀ v : List Nat, v ≠ [] ->
      momentumOrder (fun j => -((j : Int) + 1)) 1 v <= 0 ->
      ∀ n, v.count (vertex n).val = v.count n := by
    intro v nonempty retained n
    by_cases low : n <= 1
    · simp [vertex, Nat.min_eq_left (by omega : n <= 2)]
    · have original : n ∉ v := fun h => low (small v nonempty retained n h)
      have folded := (members v nonempty retained n).not.mpr original
      rw [List.count_eq_zero.mpr original, List.count_eq_zero.mpr folded]
  have interpretation : InterpretsContactCountingAt c vertex id ()
      (fun n => -((n : Int) + 1)) 1 := by
    refine ⟨?_, ?_, ?_, ?_⟩
    · intro n q through
      change ((vertex n).val : Int) - 1 = q ↔ -((n : Int) + 1) + 2 * (n : Int) = q
      dsimp [vertex]
      by_cases low : n <= 2
      · rw [Nat.min_eq_left low]
        omega
      · rw [Nat.min_eq_right (by omega : 2 <= n)]
        omega
    · intro n q through
      change (∃ v : List Nat, v ≠ [] ∧ (vertex n).val ∈ v ∧
        momentumOrder (fun j => -((j : Int) + 1)) 1 v <= q) ↔ _
      constructor
      · rintro ⟨v, nonempty, member, order⟩
        exact ⟨v, nonempty, (members v nonempty (order.trans through) n).mp member, order⟩
      · rintro ⟨v, nonempty, member, order⟩
        exact ⟨v, nonempty, (members v nonempty (order.trans through) n).mpr member, order⟩
    · intro n
      change (∀ bound : Nat, ∃ v : List Nat, v ≠ [] ∧
        momentumOrder (fun j => -((j : Int) + 1)) 1 v <= 0 ∧ bound < v.count (vertex n).val) ↔ _
      constructor <;> intro unbounded bound
      · obtain ⟨v, nonempty, retained, exceeds⟩ := unbounded bound
        exact ⟨v, nonempty, retained, by simpa [counts v nonempty retained n] using exceeds⟩
      · obtain ⟨v, nonempty, retained, exceeds⟩ := unbounded bound
        exact ⟨v, nonempty, retained, by simpa [counts v nonempty retained n] using exceeds⟩
    · intro n
      change (∃ bound : Nat, ∀ v : List Nat, v ≠ [] ->
        momentumOrder (fun j => -((j : Int) + 1)) 1 v <= 0 -> v.count (vertex n).val <= bound) ↔ _
      constructor <;> rintro ⟨bound, finite⟩ <;> refine ⟨bound, ?_⟩ <;> intro v nonempty retained
      · simpa [counts v nonempty retained n] using finite v nonempty retained
      · simpa [counts v nonempty retained n] using finite v nonempty retained
  have result := diagram_interpretation_derives_mixed_treatments c vertex id ()
    (fun n => -((n : Int) + 1)) 1
    ⟨rfl, rfl, fun n hn => by dsimp; omega⟩ rfl interpretation
  refine ⟨c, vertex, interpretation, result, ?_, ?_, ?_, ?_, ?_⟩
  · intro n high retained
    obtain ⟨v, nonempty, member, order⟩ := (interpretation.2.1 n 0 le_rfl).mp retained
    have := small v nonempty order n member
    omega
  · constructor
    · intro left right leftOrder rightOrder leading correction ordered strict
      change (left.val : Int) - 1 = leftOrder at leading
      change (right.val : Int) - 1 = rightOrder at correction
      change leftOrder <= rightOrder at ordered
      change ¬rightOrder <= leftOrder at strict
      change left.val < right.val
      omega
    · refine ⟨vertex 0, vertex 1, -1, 0, ?_⟩
      norm_num [EffectiveTheory.PowerCountingContext.StrictContributionComparisonAt, c, vertex]
  · intro term
    change ¬term.val < term.val
    omega
  · change ¬((vertex 0).val : Int) - 1 = 0
    norm_num [vertex]
  · intro unrestricted
    have injective := unrestricted_contributions_force_injective_contact_labels c vertex id () unrestricted
    have wrong := injective (show vertex 2 = vertex 3 by rfl)
    omega

-- The route imports interpretation and explicit amplitude formulas, not the
-- mixed-treatment conclusion. The labels are identified without a record of proofs.
example {Channel Scale Momentum Coupling Term Order Regime Fit : Type}
    (f : NuclearScatteringFramework Channel Scale Momentum Coupling Term Order Regime Fit)
    (channel : Channel) (scale : Scale) (p : Momentum) :
    f.LargeScatteringLengthPowerCountingCalculation channel scale p ↔
      (f.largeScatteringLength channel → f.pdsSubtractionAt scale →
       f.scaleComparableToMomentum scale p → f.loopHasOrderMomentum scale p →
       f.couplingScalingEstablished channel scale p →
       ∃ vertex : Nat -> Term, ∃ exponent : Int -> Order,
         vertex 0 = f.leadingContact ∧ vertex 1 = f.firstCorrection ∧
         exponent (-1) = f.leadingOrder ∧ exponent 0 = f.subleadingOrder ∧
         InterpretsContactCountingAt f.powerCounting vertex exponent (f.regimeOf channel scale p)
           (f.pionlessContactOrderAt channel scale p) (f.pionlessBubbleLoopOrderAt scale p) ∧
         (f.pionlessContactExpansionReadoutAt channel scale p).EquationThirteenAt) := Iff.rfl

#print axioms ContactPowerCounting.diagram_interpretation_derives_mixed_treatments
#print axioms NuclearScatteringFramework.large_scattering_length_requires_resummed_leading_contact