import PhysicsLogic.Papers.KaplanSavageWise1998

open PhysicsLogic.Papers.KaplanSavageWise1998

example : ∀ (f : PionInclusiveRGFlow) (m mu p : Real),
    f.PionDiagramDomainAt m mu p ->
    (f.pionLogPrefactor m mu p ≠ 0 ↔ f.axialCoupling ≠ 0 ∧ f.c0 mu ≠ 0) :=
  PhysicsLogic.Papers.KaplanSavageWise1998.PionInclusiveRGFlow.pion_log_prefactor_nonzero_iff

example : ∀ (f : PionInclusiveRGFlow) (m mu p : Real), 0 < mu ->
    HasDerivAt (fun v : Real => f.pionLogPrefactor m mu p * (Real.log v : Complex))
      (f.pionLogPrefactor m mu p / (mu : Complex)) mu :=
  PhysicsLogic.Papers.KaplanSavageWise1998.PionInclusiveRGFlow.explicit_pion_log_response_at_fixed_dressing

example {C S P K T O R F : Type} : ∀
    (f : NuclearScatteringFramework C S P K T O R F) (c : C) (p : P),
    ((∀ s, f.pionInclusiveRetainedFlow.PionDiagramDomainAt f.pionMassValue
        (f.subtractionScaleValueAt s) (f.momentumValue p) ->
      f.subleadingPionLoopValueAt c s p =
        f.logarithmicPionLoopFormulaValueAt c s p) ∧
      ∃ a b, f.pionInclusiveRetainedFlow.PionDiagramDomainAt f.pionMassValue
          (f.subtractionScaleValueAt a) (f.momentumValue p) ∧
        f.pionInclusiveRetainedFlow.PionDiagramDomainAt f.pionMassValue
          (f.subtractionScaleValueAt b) (f.momentumValue p) ∧
        f.logarithmicPionLoopFormulaValueAt c a p ≠ f.logarithmicPionLoopFormulaValueAt c b p) ↔
    (f.logarithmicScaleDependenceAtSubleadingOrder c p ∧
      ∃ a b, f.pionInclusiveRetainedFlow.PionDiagramDomainAt f.pionMassValue
          (f.subtractionScaleValueAt a) (f.momentumValue p) ∧
        f.pionInclusiveRetainedFlow.PionDiagramDomainAt f.pionMassValue
          (f.subtractionScaleValueAt b) (f.momentumValue p) ∧
        f.logarithmicPionLoopFormulaValueAt c a p ≠ f.logarithmicPionLoopFormulaValueAt c b p) :=
  PhysicsLogic.Papers.KaplanSavageWise1998.NuclearScatteringFramework.former_pion_log_contract_iff_explicit_log_and_graph_variation

example {C S P K T O R F : Type} : ∀
    (f : NuclearScatteringFramework C S P K T O R F) (c : C) (p : P),
    f.logarithmicScaleDependenceAtSubleadingOrder c p ->
    ∃ s, f.pionInclusiveRetainedFlow.PionDiagramDomainAt f.pionMassValue
        (f.subtractionScaleValueAt s) (f.momentumValue p) ∧
      (let mu := f.subtractionScaleValueAt s
       let prefactor := f.pionInclusiveRetainedFlow.pionLogPrefactor f.pionMassValue
         mu (f.momentumValue p)
       HasDerivAt (fun v : Real => prefactor * (Real.log v : Complex))
         (prefactor / (mu : Complex)) mu ∧ prefactor / (mu : Complex) ≠ 0) :=
  PhysicsLogic.Papers.KaplanSavageWise1998.NuclearScatteringFramework.explicit_pion_log_has_a_nonzero_fixed_dressing_response

-- A single represented scale can have a nonzero explicit log coefficient,
-- but cannot supply a two-sample variation witness. This tests only the
-- nominal subcontract, not the open scale image of the full graded route.
example :
    let f := PionInclusiveRGFlow.Countermodels.nonzeroPionJet
    let sample : Unit -> Real := fun _ => 1
    (∃ s, f.PionDiagramDomainAt 1 (sample s) 1 ∧
      f.pionLogPrefactor 1 (sample s) 1 ≠ 0) ∧
    ¬(∃ a b, f.PionDiagramDomainAt 1 (sample a) 1 ∧
      f.PionDiagramDomainAt 1 (sample b) 1 ∧
      f.twoLoopPionAmplitude 1 (sample a) 1 ≠
        f.twoLoopPionAmplitude 1 (sample b) 1) := by
  dsimp
  let f := PionInclusiveRGFlow.Countermodels.nonzeroPionJet
  have domain : f.PionDiagramDomainAt 1 1 1 :=
    ⟨PionInclusiveRGFlow.Countermodels.the_retained_jet_has_actual_nonzero_pion_beta_equations.1,
      by norm_num, by norm_num, by norm_num,
      f.real_dressing_cannot_vanish_at_positive_momentum 1 1 (by norm_num)⟩
  constructor
  · refine ⟨(), domain, (f.pion_log_prefactor_nonzero_iff 1 1 1 domain).mpr ?_⟩
    constructor
    · change (1 : Real) ≠ 0
      norm_num
    · change (1 + 2 * ((1 : Real) - 1)) ≠ 0
      rw [sub_self, mul_zero, add_zero]
      exact one_ne_zero
  · simp

-- Removing either interaction makes the explicit log coefficient zero,
-- irrespective of whether the printed kernel still contains a logarithm.
example (f : PionInclusiveRGFlow) (m mu p : Real) :
    ({ f with axialCoupling := 0 } : PionInclusiveRGFlow).pionLogPrefactor m mu p = 0 ∧
    ({ f with c0 := fun _ => 0 } : PionInclusiveRGFlow).pionLogPrefactor m mu p = 0 := by
  simp [PionInclusiveRGFlow.pionLogPrefactor, PionInclusiveRGFlow.pionDiagramLeadingAmplitude]

#print axioms PhysicsLogic.Papers.KaplanSavageWise1998.NuclearScatteringFramework.explicit_pion_log_has_a_nonzero_fixed_dressing_response