import PhysicsLogic.Papers.KaplanSavageWise1998.Fidelity

open PhysicsLogic.Papers.KaplanSavageWise1998

universe uChannel uScale uMomentum uCoupling uTerm uOrder uRegime uFit

example : forall {Channel : Type uChannel} {Scale : Type uScale} {Momentum : Type uMomentum}
    {Coupling : Type uCoupling} {Term : Type uTerm} {Order : Type uOrder}
    {Regime : Type uRegime} {Fit : Type uFit}
    (context : SemanticContext Channel Scale Momentum Coupling Term Order Regime Fit)
    (certificate : routedArgument.RouteSemanticallyCertified
      context.interpretAtom .largeLengthPowerCounting)
    (positive : 0 < context.framework.momentumValue context.expansionMomentum),
    let r := context.framework.pionlessContactExpansionReadoutAt
      context.expansionChannel context.expansionScale context.expansionMomentum
    r.EquationThirteenAt ∧
      PhysicsLogic.Framework.ElasticSWave.ElasticUnitaryAt r.momentum r.leadingReducedAmplitude ∧
      PhysicsLogic.Framework.ElasticSWave.LinearizedOpticalTheoremAt r.momentum
        r.leadingReducedAmplitude r.correctionReducedAmplitude ∧
    (forall t : Real,
      (r.leadingReducedAmplitude + (t : Complex) * r.correctionReducedAmplitude) +
        ((r.scaledLeadingCoupling + t * r.scaledInsertion : Real) : Complex) *
          ((r.subtractionScale : Complex) + Complex.I * (r.momentum : Complex)) *
            (r.leadingReducedAmplitude + (t : Complex) * r.correctionReducedAmplitude) +
        ((r.scaledLeadingCoupling + t * r.scaledInsertion : Real) : Complex) =
      (t : Complex) ^ 2 * (r.scaledInsertion : Complex) *
        ((r.subtractionScale : Complex) + Complex.I * (r.momentum : Complex)) *
          r.correctionReducedAmplitude) :=
  PhysicsLogic.Papers.KaplanSavageWise1998.SemanticContext.certified_mixed_expansion_retains_actual_terms_and_perturbative_unitarity

#print axioms PhysicsLogic.Papers.KaplanSavageWise1998.SemanticContext.certified_mixed_expansion_retains_actual_terms_and_perturbative_unitarity

-- Both route outputs are required, and their channel identification is explicit.
-- No equality between the threshold sampling momentum and prediction momentum,
-- nor between the RG route's selected scale and the prediction scale, is needed.
example : forall {Channel : Type uChannel} {Scale : Type uScale} {Momentum : Type uMomentum}
    {Coupling : Type uCoupling} {Term : Type uTerm} {Order : Type uOrder}
    {Regime : Type uRegime} {Fit : Type uFit}
    (c : SemanticContext Channel Scale Momentum Coupling Term Order Regime Fit),
    routedArgument.RouteSemanticallyCertified c.interpretAtom .pionlessPDS ->
    routedArgument.RouteSemanticallyCertified c.interpretAtom .largeLengthPowerCounting ->
    c.lowChannel = c.expansionChannel ->
    forall cutoff bound rho : Real,
    0 < c.framework.momentumValue c.expansionMomentum ->
    0 < c.framework.subtractionScaleValueAt c.expansionScale ->
    0 < cutoff -> rho < 1 ->
    |(c.framework.scatteringLength c.expansionChannel)⁻¹| <=
      rho * c.framework.subtractionScaleValueAt c.expansionScale ->
    |cutoff * (c.framework.effectiveRange c.expansionChannel / 2)| <= bound ->
    let r := c.framework.pionlessContactExpansionReadoutAt c.expansionChannel c.expansionScale c.expansionMomentum
    r.EquationThirteenAt ∧
      (1 / (1 + rho) <= |r.subtractionScale * r.scaledLeadingCoupling| ∧
        |r.subtractionScale * r.scaledLeadingCoupling| <= 1 / (1 - rho)) ∧
      r.leadingReducedAmplitude =
        (-(((c.framework.scatteringLength c.expansionChannel)⁻¹ : Real) : Complex) -
          Complex.I * (r.momentum : Complex))⁻¹ ∧
      r.correctionReducedAmplitude =
        -((c.framework.effectiveRange c.expansionChannel / 2 * r.momentum ^ 2 : Real) : Complex) *
          r.leadingReducedAmplitude ^ 2 ∧
      ‖r.correctionReducedAmplitude‖ <= (bound * r.momentum / cutoff) * ‖r.leadingReducedAmplitude‖ ∧
      (bound * r.momentum < cutoff -> ‖r.correctionReducedAmplitude‖ < ‖r.leadingReducedAmplitude‖) ∧
      (forall n : Nat,
        let loopSum := (Finset.range (n + 1)).sum (fun j =>
          -(r.scaledLeadingCoupling : Complex) * (-(r.scaledLeadingCoupling : Complex) *
            ((r.subtractionScale : Complex) + Complex.I * (r.momentum : Complex))) ^ j)
        ‖loopSum - r.leadingReducedAmplitude‖ =
          (|r.scaledLeadingCoupling| * ‖(r.subtractionScale : Complex) + Complex.I * (r.momentum : Complex)‖) ^
            (n + 1) * ‖r.leadingReducedAmplitude‖ ∧
        (1 <= |r.scaledLeadingCoupling| * ‖(r.subtractionScale : Complex) + Complex.I * (r.momentum : Complex)‖ ->
          ‖r.leadingReducedAmplitude‖ <= ‖loopSum - r.leadingReducedAmplitude‖)) :=
  PhysicsLogic.Papers.KaplanSavageWise1998.SemanticContext.certified_routes_control_the_same_pionless_amplitudes

#print axioms PhysicsLogic.Papers.KaplanSavageWise1998.SemanticContext.certified_routes_control_the_same_pionless_amplitudes

-- Readout-level boundary: two real-contact elastic-unitary amplitudes can
-- belong to different inverse scattering lengths. This is not a realization
-- of the full source certificates, and does not identify the two channels.
set_option backward.isDefEq.respectTransparency false in
example :
    PhysicsLogic.Framework.ElasticSWave.ElasticUnitaryAt 1
      (PhysicsLogic.Framework.ElasticSWave.contactAmplitude (-1 / 2) 1 1) ∧
    PhysicsLogic.Framework.ElasticSWave.ElasticUnitaryAt 1
      (PhysicsLogic.Framework.ElasticSWave.contactAmplitude (-1 / 3) 1 1) ∧
    PhysicsLogic.Framework.ElasticSWave.contactAmplitude (-1 / 2) 1 1 ≠
      PhysicsLogic.Framework.ElasticSWave.contactAmplitude (-1 / 3) 1 1 := by
  refine ⟨PhysicsLogic.Framework.ElasticSWave.real_contact_amplitude_is_elastic_unitary _ _ _
      (PhysicsLogic.Framework.ElasticSWave.contact_denominator_ne_zero_of_positive_momentum _ _ 1 (by norm_num)),
    PhysicsLogic.Framework.ElasticSWave.real_contact_amplitude_is_elastic_unitary _ _ _
      (PhysicsLogic.Framework.ElasticSWave.contact_denominator_ne_zero_of_positive_momentum _ _ 1 (by norm_num)), ?_⟩
  intro equality
  have realParts := congrArg Complex.re equality
  norm_num [PhysicsLogic.Framework.ElasticSWave.contactAmplitude,
    PhysicsLogic.Framework.ElasticSWave.contactDenominator, Complex.div_re, Complex.normSq_apply] at realParts