import PhysicsLogic.Papers.KaplanSavageWise1998 open PhysicsLogic.Papers.KaplanSavageWise1998 PhysicsLogic.Framework.ElasticSWave open PionlessContactExpansionReadout example : forall (r : PionlessContactExpansionReadout), r.EquationThirteenAt ↔ 0 < r.mass ∧ 0 ≤ r.momentum ∧ (r.leadingReducedAmplitude + (r.scaledLeadingCoupling : Complex) * ((r.subtractionScale : Complex) + Complex.I * (r.momentum : Complex)) * r.leadingReducedAmplitude = -(r.scaledLeadingCoupling : Complex) ∧ r.correctionReducedAmplitude + (r.scaledLeadingCoupling : Complex) * ((r.subtractionScale : Complex) + Complex.I * (r.momentum : Complex)) * r.correctionReducedAmplitude = -(r.scaledInsertion : Complex) * (1 + ((r.subtractionScale : Complex) + Complex.I * (r.momentum : Complex)) * r.leadingReducedAmplitude)) := PhysicsLogic.Papers.KaplanSavageWise1998.PionlessContactExpansionReadout.equation_thirteen_iff_local_interaction_equations -- Higher interactions and amplitudes are unconstrained, not silently zero. example : forall (r : PionlessContactExpansionReadout) (higherInteraction higherResult : PowerSeries Complex), r.EquationThirteenAt ↔ 0 < r.mass ∧ 0 ≤ r.momentum ∧ let interaction : PowerSeries Complex := PowerSeries.C (r.scaledLeadingCoupling : Complex) + PowerSeries.X * PowerSeries.C (r.scaledInsertion : Complex) + PowerSeries.X ^ 2 * higherInteraction let result : PowerSeries Complex := PowerSeries.C r.leadingReducedAmplitude + PowerSeries.X * PowerSeries.C r.correctionReducedAmplitude + PowerSeries.X ^ 2 * higherResult forall n : Nat, n <= 1 -> PowerSeries.coeff n (result + interaction * PowerSeries.C ((r.subtractionScale : Complex) + Complex.I * (r.momentum : Complex)) * result + interaction) = 0 := PhysicsLogic.Papers.KaplanSavageWise1998.PionlessContactExpansionReadout.equation_thirteen_iff_graded_scattering_equation -- The complete quantitative source conclusion has a standalone signature. -- The running model has five data fields; no route certificate or unrelated -- pion/fit/channel context is required. All numerical premises remain visible. example : forall (flow : PionlessRGFlow), flow.EquationElevenAt -> forall (mu p cutoff bound rho : Real) (leading correction : Complex), 0 < p -> 0 < mu -> 0 < cutoff -> rho < 1 -> |flow.inverseScatteringLength| <= rho * mu -> |cutoff * (flow.effectiveRange / 2)| <= bound -> (let g0 := flow.mass / (4 * Real.pi) * flow.c0 mu let g2 := flow.mass / (4 * Real.pi) * flow.c2 mu leading + (g0 : Complex) * ((mu : Complex) + Complex.I * (p : Complex)) * leading = -(g0 : Complex) ∧ correction + (g0 : Complex) * ((mu : Complex) + Complex.I * (p : Complex)) * correction = -((g2 * p ^ 2 : Real) : Complex) * (1 + ((mu : Complex) + Complex.I * (p : Complex)) * leading)) -> let g0 := flow.mass / (4 * Real.pi) * flow.c0 mu flow.NonpoleAt mu ∧ (1 / (1 + rho) <= |mu * g0| ∧ |mu * g0| <= 1 / (1 - rho)) ∧ leading = (-(flow.inverseScatteringLength : Complex) - Complex.I * (p : Complex))⁻¹ ∧ correction = -((flow.effectiveRange / 2 * p ^ 2 : Real) : Complex) * leading ^ 2 ∧ ‖correction‖ <= (bound * p / cutoff) * ‖leading‖ ∧ (bound * p < cutoff -> ‖correction‖ < ‖leading‖) ∧ (forall n : Nat, let partialSum := (Finset.range (n + 1)).sum (fun j => -(g0 : Complex) * (-(g0 : Complex) * ((mu : Complex) + Complex.I * (p : Complex))) ^ j) ‖partialSum - leading‖ = (|g0| * ‖(mu : Complex) + Complex.I * (p : Complex)‖) ^ (n + 1) * ‖leading‖ ∧ (1 <= |g0| * ‖(mu : Complex) + Complex.I * (p : Complex)‖ -> ‖leading‖ <= ‖partialSum - leading‖)) := PhysicsLogic.Papers.KaplanSavageWise1998.PionlessRGFlow.matched_running_values_control_resummation_and_first_correction -- A unitary-limit, nonzero-range diagnostic at mu=2 and p=1/10. The actual -- first correction is smaller while every finite raw leading sum has an -- error at least as large as the leading amplitude. This is not nuclear data. example (n : Nat) : ‖(1 : Complex)‖ < ‖10 * Complex.I‖ ∧ ‖10 * Complex.I‖ <= ‖(Finset.range (n + 1)).sum (fun j => (1 / 2 : Complex) * ((1 / 2 : Complex) * (2 + Complex.I * (1 / 10))) ^ j) - 10 * Complex.I‖ := by let flow : PionlessRGFlow := ⟨4 * Real.pi, 0, 2, fun mu => (-mu)⁻¹, fun mu => (-mu)⁻¹ ^ 2⟩ have values : flow.EquationElevenAt := by refine ⟨by dsimp [PionlessRGFlow.PhysicalAt, flow]; positivity, ?_⟩ intro mu _ constructor <;> dsimp [flow, PionlessRGFlow.c0Solution, PionlessRGFlow.c2Solution] <;> field_simp <;> ring have localEquations : let g0 := flow.mass / (4 * Real.pi) * flow.c0 2 let g2 := flow.mass / (4 * Real.pi) * flow.c2 2 10 * Complex.I + (g0 : Complex) * (2 + Complex.I * (1 / 10)) * (10 * Complex.I) = -(g0 : Complex) ∧ (1 : Complex) + (g0 : Complex) * (2 + Complex.I * (1 / 10)) = -((g2 * (1 / 10) ^ 2 : Real) : Complex) * (1 + (2 + Complex.I * (1 / 10)) * (10 * Complex.I)) := by norm_num [flow, Real.pi_ne_zero, Complex.ext_iff, Complex.mul_re, Complex.mul_im] have core := flow.matched_running_values_control_resummation_and_first_correction values 2 (1 / 10) 1 1 0 (10 * Complex.I) 1 (by norm_num) (by norm_num) (by norm_num) (by norm_num) (by norm_num [flow]) (by norm_num [flow]) (by simpa using localEquations) have ratio : 1 <= |flow.mass / (4 * Real.pi) * flow.c0 2| * ‖((2 : Real) : Complex) + Complex.I * ((1 / 10 : Real) : Complex)‖ := by have lower := Complex.re_le_norm ((2 : Complex) + Complex.I * (1 / 10 : Complex)) norm_num [flow, Real.pi_ne_zero] at lower ⊢ linarith refine ⟨core.2.2.2.2.2.1 (by norm_num), ?_⟩ simpa [flow, Real.pi_ne_zero] using (core.2.2.2.2.2.2 n).2 ratio example : forall (flow : PionlessRGFlow), flow.EquationElevenAt -> forall p cutoff bound : Real, 0 < p -> 0 < cutoff -> |cutoff * (flow.effectiveRange / 2)| <= bound -> forall mu (leading correction : Complex), flow.NonpoleAt mu -> let g0 := flow.mass / (4 * Real.pi) * flow.c0 mu let g2 := flow.mass / (4 * Real.pi) * flow.c2 mu (leading + (g0 : Complex) * ((mu : Complex) + Complex.I * (p : Complex)) * leading = -(g0 : Complex) ∧ correction + (g0 : Complex) * ((mu : Complex) + Complex.I * (p : Complex)) * correction = -((g2 * p ^ 2 : Real) : Complex) * (1 + ((mu : Complex) + Complex.I * (p : Complex)) * leading)) -> leading = (-(flow.inverseScatteringLength : Complex) - Complex.I * (p : Complex))⁻¹ ∧ correction = -((flow.effectiveRange / 2 * p ^ 2 : Real) : Complex) * leading ^ 2 ∧ ‖correction‖ <= (bound * p / cutoff) * ‖leading‖ := PhysicsLogic.Papers.KaplanSavageWise1998.PionlessRGFlow.running_values_control_resummed_terms example : forall (r : PionlessContactExpansionReadout), r.EquationThirteenAt ↔ 0 < r.mass ∧ 0 ≤ r.momentum ∧ (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.PionlessContactExpansionReadout.equation_thirteen_iff_first_order_scattering_equation example : ∀ (r : PionlessContactExpansionReadout), r.EquationThirteenAt ↔ 0 < r.mass ∧ 0 ≤ r.momentum ∧ r.bubbleDenominator ≠ 0 ∧ r.leadingReducedAmplitude = contactAmplitude r.scaledLeadingCoupling r.subtractionScale r.momentum ∧ r.correctionReducedAmplitude = contactInsertionAmplitude r.scaledLeadingCoupling r.scaledInsertion r.subtractionScale r.momentum := PhysicsLogic.Papers.KaplanSavageWise1998.PionlessContactExpansionReadout.equation_thirteen_iff_reduced_source_terms example : ∀ (r : PionlessContactExpansionReadout), r.EquationThirteenAt ↔ 0 < r.mass ∧ 0 ≤ r.momentum ∧ r.bubbleDenominator ≠ 0 ∧ r.leadingAmplitude = -(r.leadingCoupling : Complex) / r.bubbleDenominator ∧ r.derivativeInsertionAmplitude = -(r.derivativeCoupling : Complex) * (r.momentum : Complex)^2 / r.bubbleDenominator^2 := PhysicsLogic.Papers.KaplanSavageWise1998.PionlessContactExpansionReadout.equation_thirteen_iff_source_terms example : ∀ (r : PionlessContactExpansionReadout), r.EquationThirteenAt → r.leadingReducedAmplitude = contactAmplitude r.scaledLeadingCoupling r.subtractionScale r.momentum ∧ r.correctionReducedAmplitude = contactInsertionAmplitude r.scaledLeadingCoupling r.scaledInsertion r.subtractionScale r.momentum := equation_thirteen_has_actual_reduced_amplitudes example : ∀ (r : PionlessContactExpansionReadout), r.EquationThirteenAt → 0 < r.momentum → ElasticUnitaryAt r.momentum r.leadingReducedAmplitude ∧ LinearizedOpticalTheoremAt r.momentum r.leadingReducedAmplitude r.correctionReducedAmplitude := equation_thirteen_realizes_perturbative_elastic_unitarity example : ∀ (r : PionlessContactExpansionReadout), r.EquationThirteenAt → 0 < r.momentum → ∀ t : Real, opticalDefect r.momentum (r.leadingReducedAmplitude + (t : Complex) * r.correctionReducedAmplitude) = -r.momentum * t^2 * Complex.normSq r.correctionReducedAmplitude := equation_thirteen_truncation_has_quadratic_optical_defect universe uChannel uScale uMomentum uCoupling uTerm uOrder uRegime uFit -- A complete core contract: no paper adapter, channel, fit, pion sector or -- interpretation flags occur. The reduced amplitude equations remain inputs. example : ∀ (flow : PionlessRGFlow) (phase : Real -> Real) (contact : Real -> Real -> Real) (p cutoff bound : Real), flow.PhysicalAt -> PhysicsLogic.Framework.EffectiveRangeExpansion.HasFirstTwoCoefficients phase (-flow.inverseScatteringLength) (flow.effectiveRange / 2) -> (∀ mu, flow.NonpoleAt mu -> PhysicsLogic.Framework.EffectiveRangeExpansion.HasFirstTwoCoefficients (contact mu) (flow.mass / (4 * Real.pi) * flow.c0 mu) (flow.mass / (4 * Real.pi) * flow.c2 mu)) -> (∀ mu, flow.NonpoleAt mu -> Filter.Eventually (fun q => (phase q + mu) * contact mu q = -1) PhysicsLogic.Framework.EffectiveRangeExpansion.approach) -> 0 < p -> 0 < cutoff -> |cutoff * (flow.effectiveRange / 2)| <= bound -> flow.EquationElevenAt ∧ (∀ mu, flow.NonpoleAt mu -> flow.ExactBetaDerivativesAt mu) ∧ ∀ mu (leading correction : Complex), flow.NonpoleAt mu -> let g0 := flow.mass / (4 * Real.pi) * flow.c0 mu let g2 := flow.mass / (4 * Real.pi) * flow.c2 mu (leading + (g0 : Complex) * ((mu : Complex) + Complex.I * (p : Complex)) * leading = -(g0 : Complex) ∧ correction + (g0 : Complex) * ((mu : Complex) + Complex.I * (p : Complex)) * correction = -((g2 * p ^ 2 : Real) : Complex) * (1 + ((mu : Complex) + Complex.I * (p : Complex)) * leading)) -> leading = (-((flow.inverseScatteringLength : Real) : Complex) - Complex.I * (p : Complex))⁻¹ ∧ correction = -((flow.effectiveRange / 2 * p ^ 2 : Real) : Complex) * leading ^ 2 ∧ ‖correction‖ <= (bound * p / cutoff) * ‖leading‖ := PhysicsLogic.Papers.KaplanSavageWise1998.PionlessRGFlow.observable_family_controls_running_and_resummed_terms -- Matching equations, beta equations, and full-amplitude invariance are not inputs. example : ∀ {Channel : Type uChannel} {Scale : Type uScale} {Momentum : Type uMomentum} {Coupling : Type uCoupling} {Term : Type uTerm} {Order : Type uOrder} {Regime : Type uRegime} {Fit : Type uFit} (f : NuclearScatteringFramework Channel Scale Momentum Coupling Term Order Regime Fit) (channel : Channel) (scale : Scale) (momentum : Momentum) (cutoff bound : Real), f.effectiveRangeDataMatched channel -> f.PionlessObservableMatchingAt channel -> (f.pionlessRGFlow channel).NonpoleAt (f.subtractionScaleValueAt scale) -> (f.pionlessContactExpansionReadoutAt channel scale momentum).EquationThirteenAt -> 0 < f.momentumValue momentum -> 0 < cutoff -> |cutoff * (f.effectiveRange channel / 2)| <= bound -> let r := f.pionlessContactExpansionReadoutAt channel scale momentum r.leadingReducedAmplitude = (-(f.scatteringLength channel)⁻¹ - Complex.I * (f.momentumValue momentum : Complex))⁻¹ ∧ r.correctionReducedAmplitude = -((f.effectiveRange channel / 2 * f.momentumValue momentum ^ 2 : Real) : Complex) * r.leadingReducedAmplitude ^ 2 ∧ ‖r.correctionReducedAmplitude‖ <= (bound * f.momentumValue momentum / cutoff) * ‖r.leadingReducedAmplitude‖ ∧ ∀ otherScale, (f.pionlessRGFlow channel).NonpoleAt (f.subtractionScaleValueAt otherScale) -> (f.pionlessContactExpansionReadoutAt channel otherScale momentum).EquationThirteenAt -> let other := f.pionlessContactExpansionReadoutAt channel otherScale momentum other.leadingReducedAmplitude = r.leadingReducedAmplitude ∧ other.correctionReducedAmplitude = r.correctionReducedAmplitude := PhysicsLogic.Papers.KaplanSavageWise1998.NuclearScatteringFramework.observable_matching_controls_the_first_two_pionless_amplitudes -- These cases use the shared implementation directly, not its source readback. example (derivative scale : Real) : let r : PionlessContactExpansionReadout := ⟨4 * Real.pi, 1, scale, 0, derivative, 0, -(derivative : Complex)⟩ r.EquationThirteenAt := by norm_num [equation_thirteen_iff_local_interaction_equations, leadingReducedAmplitude, correctionReducedAmplitude, scaledLeadingCoupling, scaledInsertion, bubbleDenominator, contactAmplitude, contactInsertionAmplitude, contactDenominator, Real.pi_pos, Real.pi_ne_zero] example (mass derivative scale : Real) (positive : 0 < mass) : let r : PionlessContactExpansionReadout := ⟨mass, 0, scale, 0, derivative, 0, 0⟩ r.EquationThirteenAt := by simp [equation_thirteen_iff_local_interaction_equations, leadingReducedAmplitude, correctionReducedAmplitude, scaledLeadingCoupling, scaledInsertion, positive] -- Totalized division alone would admit this zero-momentum pole; the source does not. example : let r : PionlessContactExpansionReadout := ⟨4 * Real.pi, 0, 1, -1, 3, 0, 0⟩ ¬r.EquationThirteenAt ∧ r.leadingReducedAmplitude = contactAmplitude r.scaledLeadingCoupling r.subtractionScale r.momentum ∧ r.correctionReducedAmplitude = contactInsertionAmplitude r.scaledLeadingCoupling r.scaledInsertion r.subtractionScale r.momentum := by norm_num [equation_thirteen_iff_local_interaction_equations, leadingReducedAmplitude, correctionReducedAmplitude, scaledLeadingCoupling, scaledInsertion, bubbleDenominator, contactAmplitude, contactInsertionAmplitude, contactDenominator, Real.pi_ne_zero] -- At zero mass normalization loses arbitrary dimensionful amplitudes. example : let r : PionlessContactExpansionReadout := ⟨0, 1, 0, 1, 1, 7, 11⟩ ¬r.EquationThirteenAt ∧ r.leadingReducedAmplitude = contactAmplitude r.scaledLeadingCoupling r.subtractionScale r.momentum ∧ r.correctionReducedAmplitude = contactInsertionAmplitude r.scaledLeadingCoupling r.scaledInsertion r.subtractionScale r.momentum := by norm_num [equation_thirteen_iff_local_interaction_equations, leadingReducedAmplitude, correctionReducedAmplitude, scaledLeadingCoupling, scaledInsertion, bubbleDenominator, contactAmplitude, contactInsertionAmplitude, contactDenominator] #print axioms PhysicsLogic.Papers.KaplanSavageWise1998.PionlessContactExpansionReadout.equation_thirteen_iff_source_terms #print axioms PhysicsLogic.Papers.KaplanSavageWise1998.PionlessContactExpansionReadout.equation_thirteen_iff_graded_scattering_equation #print axioms PhysicsLogic.Papers.KaplanSavageWise1998.PionlessRGFlow.observable_family_controls_running_and_resummed_terms #print axioms PhysicsLogic.Papers.KaplanSavageWise1998.PionlessRGFlow.matched_running_values_control_resummation_and_first_correction #print axioms PhysicsLogic.Papers.KaplanSavageWise1998.NuclearScatteringFramework.observable_matching_controls_the_first_two_pionless_amplitudes