import PhysicsLogic.Framework.LargeScatteringLengthResummation import PhysicsLogic.Framework.LowEnergyEffectiveRangeReduction import PhysicsLogic.Framework.EffectiveRangeBoundStateExtraction import PhysicsLogic.Philosophy.Measurement import PhysicsLogic.Paradigm.RenormalizationGroup import Mathlib.Analysis.SpecialFunctions.ExpDeriv /-! An independent pionless nuclear-EFT consumer. KSW's original 1998 paper, printed equations (11)-(13), determines normalized running contacts and a single derivative insertion. No paper module or production control is used. All amplitudes here are reduced amplitudes f = M A/(4 pi). The real inverse scattering length and effective range are physical inputs, not fit outputs. Resumming the derivative contact is a separate algebraic completion, not the source's prescribed first-order approximation or a claim of EFT accuracy. -/ set_option autoImplicit false set_option backward.isDefEq.respectTransparency false namespace PhysicsLogicConsumer.NuclearScattering open PhysicsLogic.Framework.ElasticSWave noncomputable section structure LowEnergyData where inverseScatteringLength : Real effectiveRange : Real momentum : Real referenceShortDistanceLength : Real namespace LowEnergyData def AdmissibleScaleAt (data : LowEnergyData) (scale : Real) : Prop := 0 < data.momentum ∧ data.inverseScatteringLength - scale ≠ 0 /-- A hierarchy of the selected scales, not an assumed error estimate. -/ def LowEnergyHierarchyAt (data : LowEnergyData) : Prop := 0 < data.referenceShortDistanceLength ∧ |data.effectiveRange| ≤ data.referenceShortDistanceLength ∧ |data.inverseScatteringLength| * data.referenceShortDistanceLength ≤ 1 / 16 ∧ 0 < data.momentum ∧ data.momentum * data.referenceShortDistanceLength ≤ 1 / 16 def runningContact (data : LowEnergyData) (scale : Real) : Real := (data.inverseScatteringLength - scale)⁻¹ def derivativeInsertion (data : LowEnergyData) (scale : Real) : Real := data.effectiveRange / 2 * (data.runningContact scale) ^ 2 * data.momentum ^ 2 def leading (data : LowEnergyData) (scale : Real) : Complex := contactAmplitude (data.runningContact scale) scale data.momentum def correction (data : LowEnergyData) (scale : Real) : Complex := contactInsertionAmplitude (data.runningContact scale) (data.derivativeInsertion scale) scale data.momentum def resummedDerivativeContact (data : LowEnergyData) (scale : Real) : Complex := contactAmplitude (data.runningContact scale + data.derivativeInsertion scale) scale data.momentum theorem running_contact_changes_with_scale (data : LowEnergyData) (left right : Real) (different : left ≠ right) : data.runningContact left ≠ data.runningContact right := by intro same have inverse := congrArg (fun value : Real => value⁻¹) same simp only [runningContact, inv_inv] at inverse exact different (by linarith) theorem running_contact_recovers_leading_scattering_length_amplitude (data : LowEnergyData) (scale : Real) (admissible : data.AdmissibleScaleAt scale) : data.leading scale = reducedAmplitude (-data.inverseScatteringLength) data.momentum := by have nonzero : data.runningContact scale ≠ 0 := inv_ne_zero admissible.2 unfold leading rw [nonzero_contact_recovers_effective_range_function _ _ _ nonzero] congr 1 simp only [runningContact, inv_inv] ring theorem running_insertion_recovers_effective_range_correction (data : LowEnergyData) (scale : Real) (admissible : data.AdmissibleScaleAt scale) : data.correction scale = inverseRangeCorrection (data.effectiveRange / 2 * data.momentum ^ 2) (reducedAmplitude (-data.inverseScatteringLength) data.momentum) := by have leadingMatching : (data.inverseScatteringLength - scale) * data.runningContact scale = 1 := by simp [runningContact, admissible.2] have derivativeMatching : (data.inverseScatteringLength - scale) * (data.effectiveRange / 2 * (data.runningContact scale) ^ 2) = data.effectiveRange / 2 * data.runningContact scale := by calc _ = (data.effectiveRange / 2 * data.runningContact scale) * ((data.inverseScatteringLength - scale) * data.runningContact scale) := by ring _ = _ := by rw [leadingMatching, mul_one] exact (matched_contacts_recover_the_two_effective_range_terms _ _ _ _ _ _ leadingMatching derivativeMatching).2 theorem running_contacts_preserve_the_two_amplitude_terms (data : LowEnergyData) (left right : Real) (leftAdmissible : data.AdmissibleScaleAt left) (rightAdmissible : data.AdmissibleScaleAt right) : data.leading left = data.leading right ∧ data.correction left = data.correction right := by constructor · rw [data.running_contact_recovers_leading_scattering_length_amplitude left leftAdmissible, data.running_contact_recovers_leading_scattering_length_amplitude right rightAdmissible] · rw [data.running_insertion_recovers_effective_range_correction left leftAdmissible, data.running_insertion_recovers_effective_range_correction right rightAdmissible] theorem source_expansion_is_nonvacuous_and_unitary_through_first_order (data : LowEnergyData) (scale : Real) (admissible : data.AdmissibleScaleAt scale) : NonvacuousElasticSWaveAt (-data.inverseScatteringLength) data.momentum (data.leading scale) ∧ LinearizedOpticalTheoremAt data.momentum (data.leading scale) (data.correction scale) := by refine ⟨?_, ?_⟩ · rw [data.running_contact_recovers_leading_scattering_length_amplitude scale admissible] exact real_effective_range_function_realizes_elastic_scattering _ _ admissible.1 · exact real_contact_insertion_satisfies_linearized_unitarity _ _ _ _ admissible.1 (contact_denominator_ne_zero_of_positive_momentum _ _ _ admissible.1) theorem resumming_derivative_contact_retains_exact_remainder (data : LowEnergyData) (scale : Real) (positive : 0 < data.momentum) : data.resummedDerivativeContact scale = data.leading scale + data.correction scale + (data.derivativeInsertion scale : Complex) ^ 2 * ((scale : Complex) + Complex.I * (data.momentum : Complex)) / (contactDenominator (data.runningContact scale) scale data.momentum ^ 2 * contactDenominator (data.runningContact scale + data.derivativeInsertion scale) scale data.momentum) := contact_shift_has_exact_quadratic_remainder _ _ _ _ (contact_denominator_ne_zero_of_positive_momentum _ _ _ positive) (contact_denominator_ne_zero_of_positive_momentum _ _ _ positive) end LowEnergyData namespace LowEnergyData open PhysicsLogic.Paradigm.RenormalizationGroup /-- The two retained source amplitudes at a fixed positive prediction momentum. The parameter coordinates are M C0/(4 pi) and M C2/(4 pi); only positive, nonpole subtraction scales are compared. -/ def scatteringScaleMatchingContext (data : LowEnergyData) : ScaleMatchingContext Unit Real {mu : Real // 0 < mu ∧ data.AdmissibleScaleAt mu} Unit Unit (Complex × Complex) (Real × Real) where effectiveAt := Subtype.val parameterAt := fun mu => (data.runningContact mu, data.effectiveRange / 2 * (data.runningContact mu) ^ 2) observableIn := fun _ _ => True targetPredicts := fun _ _ value => value = (reducedAmplitude (-data.inverseScatteringLength) data.momentum, inverseRangeCorrection (data.effectiveRange / 2 * data.momentum ^ 2) (reducedAmplitude (-data.inverseScatteringLength) data.momentum)) effectivePredicts := fun mu _ value => value = (data.leading mu, data.correction mu) /-- Multiplying by the canonical momentum dimensions is a change of parameter coordinates, not a change to either amplitude prediction. -/ def dimensionlessScaleMatchingContext (data : LowEnergyData) : ScaleMatchingContext Unit Real {mu : Real // 0 < mu ∧ data.AdmissibleScaleAt mu} Unit Unit (Complex × Complex) (Real × Real) := { data.scatteringScaleMatchingContext with parameterAt := fun mu => (mu.1 * (data.scatteringScaleMatchingContext.parameterAt mu).1, mu.1 ^ 3 * (data.scatteringScaleMatchingContext.parameterAt mu).2) } /-- At infinite scattering length, the dimensionless leading contact is -1, but the derivative contact is mu*r0/2. The full retained parameter pair is constant only at zero effective range. This is not a fixed-point theorem for an EFT with unexamined higher couplings, nor a full-amplitude error bound. -/ theorem unitary_limit_parameter_coordinates_preserve_predictions_not_variation (data : LowEnergyData) (positive : 0 < data.momentum) (unitaryLimit : data.inverseScatteringLength = 0) : let raw := data.scatteringScaleMatchingContext let normalized := data.dimensionlessScaleMatchingContext raw.ParametersRun ∧ (normalized.ParametersRun ↔ data.effectiveRange ≠ 0) ∧ (∀ mu, normalized.parameterAt mu = (-1, data.effectiveRange / 2 * mu.1)) ∧ (∀ mu, (normalized.parameterAt mu).1 / mu.1 = (raw.parameterAt mu).1 ∧ (normalized.parameterAt mu).2 / mu.1 ^ 3 = (raw.parameterAt mu).2) ∧ raw.NonvacuousScaleIndependentPredictionsAt () (fun _ => True) ∧ normalized.NonvacuousScaleIndependentPredictionsAt () (fun _ => True) := by intro raw normalized let left : {mu : Real // 0 < mu ∧ data.AdmissibleScaleAt mu} := ⟨1, by norm_num [AdmissibleScaleAt, unitaryLimit, positive]⟩ let right : {mu : Real // 0 < mu ∧ data.AdmissibleScaleAt mu} := ⟨2, by norm_num [AdmissibleScaleAt, unitaryLimit, positive]⟩ have distinct : left ≠ right := by intro equal have coordinates := congrArg Subtype.val equal norm_num [left, right] at coordinates have coordinates (mu) : normalized.parameterAt mu = (-1, data.effectiveRange / 2 * mu.1) := by apply Prod.ext <;> dsimp [normalized, dimensionlessScaleMatchingContext, scatteringScaleMatchingContext, runningContact] <;> rw [unitaryLimit] <;> simp only [zero_sub, inv_neg] <;> field_simp [ne_of_gt mu.property.1] <;> ring have matching : ∀ mu, raw.MatchedAt () mu () (fun _ => True) := by intro mu _ _ _ value change (value = (data.leading mu.1, data.correction mu.1)) ↔ _ rw [data.running_contact_recovers_leading_scattering_length_amplitude mu.1 mu.property.2, data.running_insertion_recovers_effective_range_correction mu.1 mu.property.2] rfl have active : raw.TargetPredictionActiveAt () () (fun _ => True) := ⟨(), _, trivial, trivial, rfl⟩ refine ⟨?_, ?_, coordinates, ?_, ?_, ?_⟩ · refine ⟨left, right, ?_⟩ intro equal have first := congrArg Prod.fst equal exact data.running_contact_changes_with_scale 1 2 (by norm_num) first · constructor · rintro ⟨mu, nu, different⟩ zeroRange apply different rw [coordinates mu, coordinates nu, zeroRange] simp · intro nonzeroRange refine ⟨left, right, ?_⟩ intro equal rw [coordinates left, coordinates right] at equal have second := congrArg Prod.snd equal dsimp [left, right] at second exact nonzeroRange (by linarith) · intro mu change (mu.1 * (raw.parameterAt mu).1) / mu.1 = _ ∧ (mu.1 ^ 3 * (raw.parameterAt mu).2) / mu.1 ^ 3 = _ constructor <;> field_simp [ne_of_gt mu.property.1] · exact all_scale_matching_and_active_target_establish_nonvacuous_scale_independent_predictions raw () () (fun _ => True) ⟨left, right, distinct⟩ active matching · exact all_scale_matching_and_active_target_establish_nonvacuous_scale_independent_predictions normalized () () (fun _ => True) ⟨left, right, distinct⟩ active matching end LowEnergyData /-- A long negative scattering length relative to the reference range. The values are a dimensionless test, not empirical NN data. -/ def nuclearData : LowEnergyData where inverseScatteringLength := -1 effectiveRange := 1 / 16 momentum := 1 referenceShortDistanceLength := 1 / 16 theorem nuclear_terms_have_nonzero_derivative_insertion : nuclearData.leading 0 = (1 + Complex.I) / 2 ∧ nuclearData.correction 0 = -Complex.I / 64 := by norm_num [LowEnergyData.leading, LowEnergyData.correction, LowEnergyData.runningContact, LowEnergyData.derivativeInsertion, nuclearData, contactAmplitude, contactInsertionAmplitude, contactDenominator, Complex.ext_iff, Complex.div_re, Complex.div_im, Complex.normSq_apply, pow_two, Complex.mul_re, Complex.mul_im] theorem nuclear_truncation_is_orderwise_not_exactly_unitary : nuclearData.LowEnergyHierarchyAt ∧ nuclearData.runningContact 0 ≠ nuclearData.runningContact 1 ∧ nuclearData.leading 0 = nuclearData.leading 1 ∧ nuclearData.correction 0 = nuclearData.correction 1 ∧ NonvacuousElasticSWaveAt (-nuclearData.inverseScatteringLength) nuclearData.momentum (nuclearData.leading 0) ∧ LinearizedOpticalTheoremAt nuclearData.momentum (nuclearData.leading 0) (nuclearData.correction 0) ∧ (∀ parameter : Real, opticalDefect nuclearData.momentum (nuclearData.leading 0 + (parameter : Complex) * nuclearData.correction 0) = -nuclearData.momentum * parameter ^ 2 * Complex.normSq (nuclearData.correction 0)) ∧ ¬ElasticUnitaryAt nuclearData.momentum (nuclearData.leading 0 + nuclearData.correction 0) ∧ ElasticUnitaryAt nuclearData.momentum (nuclearData.resummedDerivativeContact 0) ∧ nuclearData.resummedDerivativeContact 0 ≠ nuclearData.leading 0 + nuclearData.correction 0 := by have zeroAdmissible : nuclearData.AdmissibleScaleAt 0 := by norm_num [LowEnergyData.AdmissibleScaleAt, nuclearData] have oneAdmissible : nuclearData.AdmissibleScaleAt 1 := by norm_num [LowEnergyData.AdmissibleScaleAt, nuclearData] have unchanged := nuclearData.running_contacts_preserve_the_two_amplitude_terms 0 1 zeroAdmissible oneAdmissible have source := nuclearData.source_expansion_is_nonvacuous_and_unitary_through_first_order 0 zeroAdmissible have optical := (nonvacuous_elastic_s_wave_has_unitarity_and_optical_theorem _ _ _ source.1).2 have nonzero : nuclearData.correction 0 ≠ 0 := by rw [nuclear_terms_have_nonzero_derivative_insertion.2] norm_num [Complex.ext_iff] have truncated : ¬ElasticUnitaryAt nuclearData.momentum (nuclearData.leading 0 + nuclearData.correction 0) := by simpa using nonzero_first_order_truncation_is_not_exactly_unitary nuclearData.momentum 1 (nuclearData.leading 0) (nuclearData.correction 0) zeroAdmissible.1 (by norm_num) nonzero optical source.2 have resummed : ElasticUnitaryAt nuclearData.momentum (nuclearData.resummedDerivativeContact 0) := real_contact_amplitude_is_elastic_unitary _ _ _ (contact_denominator_ne_zero_of_positive_momentum _ _ _ zeroAdmissible.1) refine ⟨by norm_num [LowEnergyData.LowEnergyHierarchyAt, nuclearData], nuclearData.running_contact_changes_with_scale 0 1 (by norm_num), unchanged.1, unchanged.2, source.1, source.2, ?_, truncated, resummed, ?_⟩ · intro parameter exact first_order_truncation_has_quadratic_optical_defect _ _ _ _ optical source.2 · intro same rw [same] at resummed exact truncated resummed theorem exactly_unitary_two_contact_resummations_need_not_be_scale_independent : nuclearData.leading 0 = nuclearData.leading 1 ∧ nuclearData.correction 0 = nuclearData.correction 1 ∧ ElasticUnitaryAt nuclearData.momentum (nuclearData.resummedDerivativeContact 0) ∧ ElasticUnitaryAt nuclearData.momentum (nuclearData.resummedDerivativeContact 1) ∧ nuclearData.resummedDerivativeContact 0 ≠ nuclearData.resummedDerivativeContact 1 := by have equalTerms := nuclearData.running_contacts_preserve_the_two_amplitude_terms 0 1 (by norm_num [LowEnergyData.AdmissibleScaleAt, nuclearData]) (by norm_num [LowEnergyData.AdmissibleScaleAt, nuclearData]) refine ⟨equalTerms.1, equalTerms.2, ?_, ?_, ?_⟩ · exact real_contact_amplitude_is_elastic_unitary _ _ _ (contact_denominator_ne_zero_of_positive_momentum _ _ _ (by norm_num [nuclearData])) · exact real_contact_amplitude_is_elastic_unitary _ _ _ (contact_denominator_ne_zero_of_positive_momentum _ _ _ (by norm_num [nuclearData])) · intro same have realPart := congrArg Complex.re same norm_num [LowEnergyData.resummedDerivativeContact, LowEnergyData.runningContact, LowEnergyData.derivativeInsertion, nuclearData, contactAmplitude, contactDenominator, Complex.div_re, Complex.normSq_apply, Complex.mul_re, Complex.mul_im] at realPart namespace SquareWell open PhysicsLogic.Framework.NeutralBoundState Filter open scoped Topology /-- Units hbar = 1, reduced mass = 1/2, energy = -1, and interior potential = -2. The comparison mode is only the exterior part of the regular radial solution. -/ def radius : Real := 3 * Real.pi / 4 def interiorAmplitude : Real := Real.exp (-radius) / Real.sin radius def interior (position : Real) : Real := interiorAmplitude * Real.sin position def exterior : Real → Real := decayingFactor 1 def matchedWave (position : Real) : Real := if position ≤ radius then interior position else exterior position theorem matching_radius_trigonometry : 0 < radius ∧ Real.sin radius ≠ 0 ∧ Real.cos radius = -Real.sin radius := by have positive : 0 < radius := by unfold radius; positivity refine ⟨positive, (Real.sin_pos_of_pos_of_lt_pi positive ?_).ne', ?_⟩ · unfold radius linarith [Real.pi_pos] · rw [show radius = Real.pi - Real.pi / 4 by unfold radius; ring, Real.cos_pi_sub, Real.sin_pi_sub, Real.cos_pi_div_four, Real.sin_pi_div_four] theorem interior_has_derivative (position : Real) : HasDerivAt interior (interiorAmplitude * Real.cos position) position := (Real.hasDerivAt_sin position).const_mul interiorAmplitude theorem exterior_has_derivative (position : Real) : HasDerivAt exterior (-exterior position) position := by simpa only [neg_mul, one_mul] using decaying_factor_has_derivative 1 position theorem interior_and_exterior_match_value_and_derivative : interior radius = exterior radius ∧ deriv interior radius = deriv exterior radius ∧ interior radius ≠ 0 := by have value : interior radius = Real.exp (-radius) := by exact div_mul_cancel₀ _ matching_radius_trigonometry.2.1 have exteriorValue : exterior radius = Real.exp (-radius) := by simp [exterior, decayingFactor] refine ⟨value.trans exteriorValue.symm, ?_, ?_⟩ · rw [(interior_has_derivative radius).deriv, (exterior_has_derivative radius).deriv, matching_radius_trigonometry.2.2, mul_neg] exact congrArg Neg.neg (value.trans exteriorValue.symm) · rw [value] exact Real.exp_ne_zero _ theorem each_piece_satisfies_selected_radial_equation (position : Real) : -deriv (deriv interior) position - 2 * interior position = -interior position ∧ -deriv (deriv exterior) position = -exterior position := by have interiorDerivative : deriv interior = fun position => interiorAmplitude * Real.cos position := by funext position exact (interior_has_derivative position).deriv have interiorSecond : deriv (deriv interior) position = -interior position := by rw [interiorDerivative] exact ((Real.hasDerivAt_cos position).const_mul interiorAmplitude).deriv.trans (mul_neg _ _) have exteriorDerivative : deriv exterior = fun position => -exterior position := by funext position exact (exterior_has_derivative position).deriv have exteriorSecond : deriv (deriv exterior) position = exterior position := by rw [exteriorDerivative] simpa only [neg_neg] using (exterior_has_derivative position).neg.deriv rw [interiorSecond, exteriorSecond] constructor <;> ring theorem matched_wave_is_regular_nonzero_and_decaying : matchedWave 0 = 0 ∧ matchedWave radius ≠ 0 ∧ Tendsto matchedWave atTop (𝓝 0) := by refine ⟨?_, ?_, ?_⟩ · simp [matchedWave, matching_radius_trigonometry.1.le, interior] · simpa only [matchedWave, le_refl, if_true] using interior_and_exterior_match_value_and_derivative.2.2 · have agrees : exterior =ᶠ[atTop] matchedWave := by filter_upwards [eventually_gt_atTop radius] with position beyond simp [matchedWave, not_le.mpr beyond] exact (positive_inverse_length_gives_decay 1 (by norm_num)).congr' agrees def logarithmicDerivative : Real := deriv interior radius / interior radius theorem interior_logarithmic_derivative_is_negative_one : logarithmicDerivative = -1 := by unfold logarithmicDerivative rw [interior_and_exterior_match_value_and_derivative.2.1, (exterior_has_derivative radius).deriv, ← interior_and_exterior_match_value_and_derivative.1] exact neg_div_self (interior_and_exterior_match_value_and_derivative.2.2) /-- Matching u = exp(-ikr) - S exp(ikr) to the actual interior derivative. Only the selected negative-energy boundary value is used here. -/ def continuedSMatrix (momentum : Complex) : Complex := Complex.exp (-2 * Complex.I * momentum * (radius : Complex)) * ((logarithmicDerivative : Complex) + Complex.I * momentum) / ((logarithmicDerivative : Complex) - Complex.I * momentum) theorem matched_bound_point_is_an_s_matrix_zero_not_a_denominator_zero : (logarithmicDerivative : Complex) - Complex.I * (-Complex.I) ≠ 0 ∧ continuedSMatrix (-Complex.I) = 0 := by constructor · rw [interior_logarithmic_derivative_is_negative_one] norm_num [Complex.ext_iff] · simp [continuedSMatrix, interior_logarithmic_derivative_is_negative_one] def exteriorMode : RadialMode := ⟨1, 1, -continuedSMatrix (-Complex.I)⟩ theorem library_recognizes_the_matched_bound_mode : exteriorMode.NonvacuousBoundMode := by apply exteriorMode.no_growing_component_realizes_bound_mode (by norm_num [exteriorMode]) (by norm_num [exteriorMode]) simp only [exteriorMode, matched_bound_point_is_an_s_matrix_zero_not_a_denominator_zero.2, neg_zero] theorem comparison_mode_is_the_exterior_not_the_regular_interior : (∀ position : Real, exteriorMode.valueAt position = (exterior position : Complex)) ∧ ¬exteriorMode.RegularAtOrigin ∧ matchedWave 0 = 0 := by refine ⟨?_, exteriorMode.nonvacuous_bound_mode_is_not_regular_at_origin library_recognizes_the_matched_bound_mode, matched_wave_is_regular_nonzero_and_decaying.1⟩ intro position simp [RadialMode.valueAt, exteriorMode, exterior, matched_bound_point_is_an_s_matrix_zero_not_a_denominator_zero.2] theorem library_computes_the_actual_exterior_radial_weight : exteriorMode.radialWeightBeyond radius = Real.exp (-2 * radius) / 2 ∧ 0 < exteriorMode.radialWeightBeyond radius ∧ MeasureTheory.IntegrableOn (fun position => Complex.normSq (exteriorMode.valueAt position)) (Set.Ioi radius) := by refine ⟨?_, exteriorMode.bound_mode_exterior_weight_is_positive library_recognizes_the_matched_bound_mode radius, exteriorMode.bound_mode_has_integrable_exterior_weight library_recognizes_the_matched_bound_mode radius⟩ simpa only [exteriorMode, Complex.normSq_one, one_mul, mul_one] using exteriorMode.bound_mode_exterior_weight_is_computed library_recognizes_the_matched_bound_mode radius end SquareWell namespace ShapeRemainder open PhysicsLogic.Framework.NeutralBoundState /-- Explicit analytic on-shell data, not an assertion of an underlying potential. -/ def phaseFunction (momentum : Complex) : Complex := -57 / 256 + momentum ^ 2 / 2 + momentum ^ 4 def realPhaseFunction (momentum : Real) : Real := -57 / 256 + momentum ^ 2 / 2 + momentum ^ 4 def continuedSMatrix (momentum : Complex) : Complex := (phaseFunction momentum + Complex.I * momentum) / (phaseFunction momentum - Complex.I * momentum) def boundMomentum : Complex := -Complex.I / 4 theorem real_and_continued_phase_data_agree (momentum : Real) : phaseFunction (momentum : Complex) = (realPhaseFunction momentum : Complex) := by norm_num [phaseFunction, realPhaseFunction] theorem real_momentum_data_retain_elastic_unitarity (momentum : Real) (positive : 0 < momentum) : NonvacuousElasticSWaveAt (realPhaseFunction momentum) momentum (reducedAmplitude (realPhaseFunction momentum) momentum) ∧ sMatrix momentum (reducedAmplitude (realPhaseFunction momentum) momentum) = continuedSMatrix (momentum : Complex) := by refine ⟨real_effective_range_function_realizes_elastic_scattering _ _ positive, ?_⟩ rw [s_matrix_is_outgoing_incoming_ratio _ _ (denominator_ne_zero_of_positive_momentum _ _ positive)] simp [continuedSMatrix, real_and_continued_phase_data_agree, denominator] theorem continued_phase_data_have_a_nonpole_bound_zero : phaseFunction boundMomentum = -1 / 4 ∧ phaseFunction boundMomentum - Complex.I * boundMomentum ≠ 0 ∧ continuedSMatrix boundMomentum = 0 := by norm_num [phaseFunction, boundMomentum, continuedSMatrix, Complex.ext_iff, Complex.div_re, Complex.div_im, Complex.normSq_apply, pow_succ, Complex.mul_re, Complex.mul_im] def selectedMode : RadialMode := ⟨1 / 4, 1, -continuedSMatrix boundMomentum⟩ theorem continued_zero_realizes_a_decaying_mode_with_nonzero_binding_residual : selectedMode.NonvacuousBoundMode ∧ effectiveRangeResidual (57 / 256) 1 (1 / 4) = -1 / 256 := by refine ⟨selectedMode.no_growing_component_realizes_bound_mode (by norm_num [selectedMode]) (by norm_num [selectedMode]) ?_, ?_⟩ · simp only [selectedMode, continued_phase_data_have_a_nonpole_bound_zero.2.2, neg_zero] · norm_num [effectiveRangeResidual] theorem library_exposes_and_bounds_the_nonzero_range_error : extractedRange (57 / 256) (1 / 4) - 1 = -1 / 8 ∧ |extractedRange (57 / 256) (1 / 4) - 1| ≤ 1 / 8 := by constructor · rw [range_extraction_error_is_scaled_binding_residual (57 / 256) 1 (1 / 4) (by norm_num), continued_zero_realizes_a_decaying_mode_with_nonzero_binding_residual.2] norm_num · have bound := controlled_binding_residual_bounds_range_error (57 / 256) 1 (1 / 4) (1 / 256) (by norm_num) (by rw [continued_zero_realizes_a_decaying_mode_with_nonzero_binding_residual.2]; norm_num) norm_num at bound ⊢ exact bound end ShapeRemainder /-! Independent phase families test the shared error contract and the conditioning of its elastic-amplitude readout. No paper or production countermodel is imported, and no fixed nuclear potential is asserted. -/ namespace LowEnergyExpansion open PhysicsLogic.Framework.EffectiveRangeExpansion open PhysicsLogic.Framework.ElasticSWave noncomputable section /-- Independent dimensionless phase data, not a reconstructed nuclear potential. -/ def referencePhase : Real -> Real := twoParameterPhaseFunction 7 6 def sourcePhase (momentum : Real) : Real := referencePhase momentum + 5 * momentum ^ 4 def reconstructedPhase (momentum : Real) : Real := sourcePhase momentum + 2 * momentum ^ 4 theorem the_source_phase_has_a_uniform_quartic_remainder : HasQuarticError sourcePhase referencePhase := by refine ⟨1, 5, by norm_num, by norm_num, ?_⟩ intro momentum positive _small simp [sourcePhase, abs_of_nonneg (mul_nonneg (by norm_num : (0 : Real) <= 5) (pow_nonneg positive.le 4))] theorem the_reconstruction_has_an_independent_quartic_error : HasQuarticError reconstructedPhase sourcePhase := by refine ⟨1, 2, by norm_num, by norm_num, ?_⟩ intro momentum positive _small simp [reconstructedPhase, abs_of_nonneg (mul_nonneg (by norm_num : (0 : Real) <= 2) (pow_nonneg positive.le 4))] theorem the_library_derives_the_actual_effective_range_expansion : NonvacuousEffectiveRangeExpansionAt sourcePhase 7 6 := quartic_control_establishes_nonvacuous_effective_range_expansion _ _ _ the_source_phase_has_a_uniform_quartic_remainder theorem the_library_identifies_the_unique_low_energy_coefficients (inverseLength effectiveRange : Real) (claimed : NonvacuousEffectiveRangeExpansionAt sourcePhase inverseLength effectiveRange) : inverseLength = 7 ∧ effectiveRange = 6 := the_actual_effective_range_coefficients_are_unique _ _ _ _ _ claimed the_library_derives_the_actual_effective_range_expansion theorem the_library_exhibits_a_positive_momentum_prediction : ∃ momentum coefficient, 0 < momentum ∧ 0 <= coefficient ∧ |sourcePhase momentum - referencePhase momentum| <= coefficient * momentum ^ 4 := nonvacuous_expansion_has_a_matched_positive_momentum _ _ _ the_library_derives_the_actual_effective_range_expansion theorem the_library_composes_independent_phase_reconstruction_errors : HasQuarticError reconstructedPhase referencePhase := independent_quartic_errors_compose_through_the_shared_paradigm _ _ _ the_reconstruction_has_an_independent_quartic_error the_source_phase_has_a_uniform_quartic_remainder theorem the_reconstructed_phase_has_the_same_first_two_coefficients : NonvacuousEffectiveRangeExpansionAt reconstructedPhase 7 6 := quartic_control_establishes_nonvacuous_effective_range_expansion _ _ _ the_library_composes_independent_phase_reconstruction_errors theorem the_source_truncation_has_a_computed_nonzero_remainder : HasFirstTwoCoefficients sourcePhase (-7) 3 ∧ sourcePhase (1 / 2) - referencePhase (1 / 2) = 5 / 16 := by refine ⟨?_, ?_⟩ · convert ((nonvacuous_expansion_iff_control_and_actual_coefficients sourcePhase 7 6).mp the_library_derives_the_actual_effective_range_expansion).2 using 1 norm_num · norm_num [sourcePhase, referencePhase, twoParameterPhaseFunction] theorem the_library_bounds_the_actual_threshold_amplitude (momentum : Real) (positive : 0 < momentum) : ‖reducedAmplitude (sourcePhase momentum) momentum - reducedAmplitude (referencePhase momentum) momentum‖ <= 5 * momentum ^ 2 := by have phaseBound : |sourcePhase momentum - referencePhase momentum| <= 5 * momentum ^ 4 := by simp [sourcePhase, abs_of_nonneg (mul_nonneg (by norm_num : (0 : Real) <= 5) (pow_nonneg positive.le 4))] have amplitude := controlled_phase_error_bounds_amplitude_error (sourcePhase momentum) (referencePhase momentum) momentum (5 * momentum ^ 4) momentum positive le_rfl phaseBound calc _ <= 5 * momentum ^ 4 / momentum ^ 2 := amplitude _ = 5 * momentum ^ 2 := by field_simp theorem the_controlled_phases_give_actual_elastic_scattering (momentum : Real) (positive : 0 < momentum) : NonvacuousElasticSWaveAt (sourcePhase momentum) momentum (reducedAmplitude (sourcePhase momentum) momentum) ∧ NonvacuousElasticSWaveAt (reconstructedPhase momentum) momentum (reducedAmplitude (reconstructedPhase momentum) momentum) := ⟨real_effective_range_function_realizes_elastic_scattering _ _ positive, real_effective_range_function_realizes_elastic_scattering _ _ positive⟩ theorem same_effective_range_coefficients_do_not_fix_the_scattering_amplitude : NonvacuousEffectiveRangeExpansionAt sourcePhase 7 6 ∧ NonvacuousEffectiveRangeExpansionAt reconstructedPhase 7 6 ∧ reducedAmplitude (sourcePhase (1 / 2)) (1 / 2) ≠ reducedAmplitude (reconstructedPhase (1 / 2)) (1 / 2) := by refine ⟨the_library_derives_the_actual_effective_range_expansion, the_reconstructed_phase_has_the_same_first_two_coefficients, ?_⟩ intro equal have first := inverse_amplitude_recovers_real_effective_range_function (sourcePhase (1 / 2)) (1 / 2) have second := inverse_amplitude_recovers_real_effective_range_function (reconstructedPhase (1 / 2)) (1 / 2) rw [equal] at first have phases := congrArg Complex.re (first.symm.trans second) norm_num [sourcePhase, reconstructedPhase, referencePhase, twoParameterPhaseFunction] at phases def resonantCorrection (momentum : Real) : Real := momentum ^ 4 theorem the_resonant_phase_has_a_controlled_effective_range_expansion : NonvacuousEffectiveRangeExpansionAt resonantCorrection 0 0 := by apply quartic_control_establishes_nonvacuous_effective_range_expansion refine ⟨1, 1, by norm_num, by norm_num, ?_⟩ intro momentum positive _small simp [resonantCorrection, twoParameterPhaseFunction, abs_of_nonneg (pow_nonneg positive.le 4)] theorem a_phase_error_tolerance_is_not_an_amplitude_error_tolerance : NonvacuousEffectiveRangeExpansionAt resonantCorrection 0 0 ∧ NonvacuousElasticSWaveAt (resonantCorrection (1 / 2)) (1 / 2) (reducedAmplitude (resonantCorrection (1 / 2)) (1 / 2)) ∧ NonvacuousElasticSWaveAt 0 (1 / 2) (reducedAmplitude 0 (1 / 2)) ∧ |resonantCorrection (1 / 2) - 0| <= 1 / 16 ∧ ¬(‖reducedAmplitude (resonantCorrection (1 / 2)) (1 / 2) - reducedAmplitude 0 (1 / 2)‖ <= 1 / 16) := by refine ⟨the_resonant_phase_has_a_controlled_effective_range_expansion, real_effective_range_function_realizes_elastic_scattering _ _ (by norm_num), real_effective_range_function_realizes_elastic_scattering _ _ (by norm_num), by norm_num [resonantCorrection], ?_⟩ have square : ‖reducedAmplitude (resonantCorrection (1 / 2)) (1 / 2) - reducedAmplitude 0 (1 / 2)‖ ^ 2 = 4 / 65 := by rw [Complex.sq_norm] norm_num [resonantCorrection, reducedAmplitude, denominator, Complex.inv_def, Complex.normSq_apply, Complex.re_ofNat, Complex.im_ofNat] intro small have nonnegative := norm_nonneg (reducedAmplitude (resonantCorrection (1 / 2)) (1 / 2) - reducedAmplitude 0 (1 / 2)) nlinarith end end LowEnergyExpansion namespace CoulombPhaseTransfer /-- Independent on-shell use of Bethe (51). The shared special-function correction is an input; it cancels from comparisons at the same D and k. These are Coulomb-relative nuclear amplitudes, not a total charged cross section or a realization by one energy-independent nuclear potential. -/ structure Datum where bohrRadius : Real momentum : Real sourceCorrection : Real namespace Datum def PhysicalAt (data : Datum) : Prop := 0 < data.bohrRadius ∧ 0 < data.momentum def parameter (data : Datum) : Real := 1 / (data.momentum * data.bohrRadius) def penetration (data : Datum) : Real := (2 * Real.pi * data.parameter) / (Real.exp (2 * Real.pi * data.parameter) - 1) def plotScale (data : Datum) : Real := data.bohrRadius * data.penetration def phaseFunction (data : Datum) (plot : Real) : Real := (plot - data.sourceCorrection) / data.plotScale def plotForPhase (data : Datum) (phase : Real) : Real := data.sourceCorrection + data.plotScale * phase def amplitude (data : Datum) (plot : Real) : Complex := reducedAmplitude (data.phaseFunction plot) data.momentum theorem the_actual_repulsive_factor_is_positive_and_less_than_one (data : Datum) (physical : data.PhysicalAt) : 0 < data.penetration ∧ data.penetration < 1 := by have parameterPositive : 0 < data.parameter := one_div_pos.mpr (mul_pos physical.2 physical.1) have exponentPositive : 0 < 2 * Real.pi * data.parameter := by positivity have denominatorPositive : 0 < Real.exp (2 * Real.pi * data.parameter) - 1 := sub_pos.mpr (Real.one_lt_exp_iff.mpr exponentPositive) refine ⟨div_pos exponentPositive denominatorPositive, ?_⟩ unfold penetration apply (div_lt_one denominatorPositive).mpr have strict := Real.add_one_lt_exp exponentPositive.ne' linarith theorem the_plot_scale_is_positive (data : Datum) (physical : data.PhysicalAt) : 0 < data.plotScale := mul_pos physical.1 (data.the_actual_repulsive_factor_is_positive_and_less_than_one physical).1 theorem the_source_plot_recovers_the_selected_nuclear_phase (data : Datum) (physical : data.PhysicalAt) (phase : Real) : data.phaseFunction (data.plotForPhase phase) = phase := by unfold phaseFunction plotForPhase rw [add_sub_cancel_left, mul_div_cancel_left₀ _ (data.the_plot_scale_is_positive physical).ne'] theorem the_library_realizes_the_actual_coulomb_relative_amplitude (data : Datum) (physical : data.PhysicalAt) (plot : Real) : NonvacuousElasticSWaveAt (data.phaseFunction plot) data.momentum (data.amplitude plot) := real_effective_range_function_realizes_elastic_scattering _ _ physical.2 theorem the_same_energy_plot_error_has_its_own_coulomb_conversion_factor (data : Datum) (physical : data.PhysicalAt) (left right : Real) : |data.phaseFunction left - data.phaseFunction right| = |left - right| / data.plotScale := by have difference : data.phaseFunction left - data.phaseFunction right = (left - right) / data.plotScale := by unfold phaseFunction ring rw [difference, abs_div, abs_of_pos (data.the_plot_scale_is_positive physical)] theorem the_library_transfers_the_converted_plot_error_to_the_nuclear_amplitude (data : Datum) (physical : data.PhysicalAt) (left right tolerance : Real) (plotControl : |left - right| ≤ tolerance) : ‖data.amplitude left - data.amplitude right‖ ≤ tolerance / (data.plotScale * data.momentum ^ 2) := by have scalePositive := data.the_plot_scale_is_positive physical have phaseControl : |data.phaseFunction left - data.phaseFunction right| ≤ tolerance / data.plotScale := by rw [data.the_same_energy_plot_error_has_its_own_coulomb_conversion_factor physical left right] exact div_le_div_of_nonneg_right plotControl scalePositive.le have amplitudeControl := controlled_phase_error_bounds_amplitude_error (data.phaseFunction left) (data.phaseFunction right) data.momentum (tolerance / data.plotScale) data.momentum physical.2 le_rfl phaseControl simpa only [div_div] using amplitudeControl end Datum def diagnostic (correction : Real) : Datum where bohrRadius := 1 momentum := 1 / 4 sourceCorrection := correction theorem a_small_coulomb_plot_error_is_not_the_same_amplitude_error (correction : Real) : let data := diagnostic correction NonvacuousElasticSWaveAt 0 data.momentum (data.amplitude (data.plotForPhase 0)) ∧ NonvacuousElasticSWaveAt (1 / 4) data.momentum (data.amplitude (data.plotForPhase (1 / 4))) ∧ |data.plotForPhase 0 - data.plotForPhase (1 / 4)| ≤ 1 / 4 ∧ ¬(‖data.amplitude (data.plotForPhase 0) - data.amplitude (data.plotForPhase (1 / 4))‖ ≤ 1 / 4) := by let data := diagnostic correction have physical : data.PhysicalAt := by norm_num [Datum.PhysicalAt, data, diagnostic] have phase0 := data.the_source_plot_recovers_the_selected_nuclear_phase physical 0 have phase1 := data.the_source_plot_recovers_the_selected_nuclear_phase physical (1 / 4) have first := data.the_library_realizes_the_actual_coulomb_relative_amplitude physical (data.plotForPhase 0) have second := data.the_library_realizes_the_actual_coulomb_relative_amplitude physical (data.plotForPhase (1 / 4)) rw [phase0] at first rw [phase1] at second refine ⟨first, second, ?_, ?_⟩ · have factor := data.the_actual_repulsive_factor_is_positive_and_less_than_one physical have difference : data.plotForPhase 0 - data.plotForPhase (1 / 4) = -(data.penetration / 4) := by dsimp [Datum.plotForPhase, Datum.plotScale, data, diagnostic] ring rw [difference, abs_neg, abs_of_pos (div_pos factor.1 (by norm_num))] linarith [factor.2] · have amplitude0 : data.amplitude (data.plotForPhase 0) = reducedAmplitude 0 (1 / 4) := by unfold Datum.amplitude rw [phase0] rfl have amplitude1 : data.amplitude (data.plotForPhase (1 / 4)) = reducedAmplitude (1 / 4) (1 / 4) := by unfold Datum.amplitude rw [phase1] rfl have squared : ‖data.amplitude (data.plotForPhase 0) - data.amplitude (data.plotForPhase (1 / 4))‖ ^ 2 = 8 := by rw [amplitude0, amplitude1, Complex.sq_norm] norm_num [reducedAmplitude, denominator, Complex.inv_def, Complex.normSq_apply, Complex.re_ofNat, Complex.im_ofNat] intro small have nonnegative := norm_nonneg (data.amplitude (data.plotForPhase 0) - data.amplitude (data.plotForPhase (1 / 4))) nlinarith end CoulombPhaseTransfer namespace NeutralParameterComparison open PhysicsLogic.Framework.EffectiveRangeExpansion /-- Independent on-shell two-parameter responses. These are not claims that the two-parameter law is exact for a selected nuclear potential. -/ def amplitude (inverseLength effectiveRange momentum : Real) : Complex := reducedAmplitude (twoParameterPhaseFunction inverseLength effectiveRange momentum) momentum theorem the_library_transfers_inverse_length_and_effective_range_errors (actualLength estimatedLength actualRange estimatedRange momentum lengthError rangeError : Real) (positive : 0 < momentum) (lengthControl : |actualLength - estimatedLength| ≤ lengthError) (rangeControl : |actualRange - estimatedRange| ≤ rangeError) : ‖amplitude actualLength actualRange momentum - amplitude estimatedLength estimatedRange momentum‖ ≤ (lengthError + (momentum ^ 2 / 2) * rangeError) / momentum ^ 2 := by have difference : twoParameterPhaseFunction actualLength actualRange momentum - twoParameterPhaseFunction estimatedLength estimatedRange momentum = -(actualLength - estimatedLength) + (momentum ^ 2 / 2) * (actualRange - estimatedRange) := by unfold twoParameterPhaseFunction ring have phaseControl : |twoParameterPhaseFunction actualLength actualRange momentum - twoParameterPhaseFunction estimatedLength estimatedRange momentum| ≤ lengthError + (momentum ^ 2 / 2) * rangeError := by rw [difference] calc _ ≤ |-(actualLength - estimatedLength)| + |(momentum ^ 2 / 2) * (actualRange - estimatedRange)| := abs_add_le _ _ _ = |actualLength - estimatedLength| + (momentum ^ 2 / 2) * |actualRange - estimatedRange| := by rw [abs_neg, abs_mul, abs_of_nonneg (show 0 ≤ momentum ^ 2 / 2 by positivity)] _ ≤ _ := add_le_add lengthControl (mul_le_mul_of_nonneg_left rangeControl (div_nonneg (sq_nonneg _) (by norm_num))) exact controlled_phase_error_bounds_amplitude_error _ _ _ _ _ positive le_rfl phaseControl theorem the_library_recognizes_both_parameterized_scattering_responses (leftLength rightLength leftRange rightRange momentum : Real) (positive : 0 < momentum) : NonvacuousElasticSWaveAt (twoParameterPhaseFunction leftLength leftRange momentum) momentum (amplitude leftLength leftRange momentum) ∧ NonvacuousElasticSWaveAt (twoParameterPhaseFunction rightLength rightRange momentum) momentum (amplitude rightLength rightRange momentum) := ⟨real_effective_range_function_realizes_elastic_scattering _ _ positive, real_effective_range_function_realizes_elastic_scattering _ _ positive⟩ theorem opposite_inverse_lengths_can_have_identical_cross_sections : (1 : Real) ≠ -1 ∧ NonvacuousElasticSWaveAt (twoParameterPhaseFunction 1 0 1) 1 (amplitude 1 0 1) ∧ NonvacuousElasticSWaveAt (twoParameterPhaseFunction (-1) 0 1) 1 (amplitude (-1) 0 1) ∧ amplitude 1 0 1 ≠ amplitude (-1) 0 1 ∧ 4 * Real.pi * Complex.normSq (amplitude 1 0 1) = 4 * Real.pi * Complex.normSq (amplitude (-1) 0 1) := by have responses := the_library_recognizes_both_parameterized_scattering_responses 1 (-1) 0 0 1 (by norm_num) refine ⟨by norm_num, responses.1, responses.2, ?_, ?_⟩ · intro same have left := inverse_amplitude_recovers_real_effective_range_function (twoParameterPhaseFunction 1 0 1) 1 have right := inverse_amplitude_recovers_real_effective_range_function (twoParameterPhaseFunction (-1) 0 1) 1 change Complex.I * (1 : Complex) + (amplitude 1 0 1)⁻¹ = _ at left change Complex.I * (1 : Complex) + (amplitude (-1) 0 1)⁻¹ = _ at right rw [same] at left have impossible := congrArg Complex.re (left.symm.trans right) norm_num [twoParameterPhaseFunction] at impossible · congr 1 norm_num [amplitude, twoParameterPhaseFunction, reducedAmplitude, denominator, Complex.inv_def, Complex.normSq_apply, Complex.re_ofNat, Complex.im_ofNat] end NeutralParameterComparison /-! Bethe 1949, p. 39, and Blatt-Jackson 1949, pp. 18-19, keep phase shifts, low-energy coefficients and experimental cross sections distinct. This independent single-channel diagnostic makes the first inverse problem explicit. The zero-effective-range model is not a fit to nuclear data. The richer record assumes a complex amplitude readout; it does not derive an experimental phase-measurement procedure from intensity measurements. -/ namespace CrossSectionRecords open PhysicsLogic.Philosophy.Measurement abbrev Momentum := {value : Real // 0 < value ∧ value ≤ 1} def topMomentum : Momentum := ⟨1, by norm_num⟩ def amplitude (inverseLength momentum : Real) : Complex := NeutralParameterComparison.amplitude inverseLength 0 momentum def crossSection (inverseLength : Real) (momentum : Momentum) : Real := 4 * Real.pi * Complex.normSq (amplitude inverseLength momentum.1) def records : RecordAccessContext Real Bool ((Momentum -> Real) × Complex) Real where admissible := fun inverseLength => inverseLength ≠ 0 recordAt := fun phaseAccess inverseLength => (crossSection inverseLength, if phaseAccess then amplitude inverseLength 1 else 0) valueAt := id theorem every_observed_momentum_has_actual_elastic_scattering (inverseLength : Real) (momentum : Momentum) : NonvacuousElasticSWaveAt (-inverseLength) momentum.1 (amplitude inverseLength momentum.1) := by simpa [amplitude, NeutralParameterComparison.amplitude, PhysicsLogic.Framework.EffectiveRangeExpansion.twoParameterPhaseFunction] using real_effective_range_function_realizes_elastic_scattering (-inverseLength) momentum.1 momentum.2.1 theorem the_whole_cross_section_curve_is_computed (inverseLength : Real) (momentum : Momentum) : crossSection inverseLength momentum = 4 * Real.pi * (inverseLength ^ 2 + momentum.1 ^ 2)⁻¹ := by simp [crossSection, amplitude, NeutralParameterComparison.amplitude, PhysicsLogic.Framework.EffectiveRangeExpansion.twoParameterPhaseFunction, reducedAmplitude, denominator, Complex.normSq_apply, pow_two] theorem reversing_the_inverse_length_preserves_every_observed_cross_section (inverseLength : Real) : crossSection (-inverseLength) = crossSection inverseLength := by funext momentum rw [the_whole_cross_section_curve_is_computed, the_whole_cross_section_curve_is_computed, neg_sq] theorem the_complex_amplitude_supplies_a_calibrated_signed_readout (inverseLength : Real) : -(Complex.I + (amplitude inverseLength 1)⁻¹).re = inverseLength := by have recovered := congrArg (fun value : Complex => -value.re) (inverse_amplitude_recovers_real_effective_range_function (-inverseLength) 1) simpa [amplitude, NeutralParameterComparison.amplitude, PhysicsLogic.Framework.EffectiveRangeExpansion.twoParameterPhaseFunction] using recovered theorem matching_rate_curves_determine_the_squared_inverse_length (first second : Real) (same : crossSection first = crossSection second) : first ^ 2 = second ^ 2 := by have equalAtOne := congrFun same topMomentum rw [the_whole_cross_section_curve_is_computed, the_whole_cross_section_curve_is_computed] at equalAtOne have sameInverse := mul_left_cancel₀ (show 4 * Real.pi ≠ 0 by positivity) equalAtOne have sameDenominator := inv_injective sameInverse simp only [topMomentum, one_pow] at sameDenominator linarith theorem the_rate_record_constrains_the_squared_inverse_length (inverseLength : Real) (nonzero : inverseLength ≠ 0) : records.RecordConstrainsValueAt false (records.recordAt false inverseLength) (fun value => value ^ 2 = inverseLength ^ 2) := by refine ⟨⟨inverseLength, nonzero, rfl⟩, ?_⟩ intro alternative compatible have curves := congrArg Prod.fst compatible.2 exact matching_rate_curves_determine_the_squared_inverse_length alternative inverseLength curves theorem the_library_rejects_signed_length_determination_even_from_the_whole_curve (inverseLength : Real) (positive : 0 < inverseLength) : ¬∃ value, records.RecordDeterminesValueAt false (records.recordAt false inverseLength) value := by apply records.ambiguous_record_does_not_determine_a_value false inverseLength (-inverseLength) (ne_of_gt positive) (neg_ne_zero.mpr (ne_of_gt positive)) · exact Prod.ext (reversing_the_inverse_length_preserves_every_observed_cross_section inverseLength).symm rfl · change inverseLength ≠ -inverseLength linarith theorem the_library_retains_magnitude_information_despite_the_sign_ambiguity : records.RecordConstrainsValueAt false (records.recordAt false 2) (fun value => |value| = 2) ∧ ¬∃ value, records.RecordDeterminesValueAt false (records.recordAt false 2) value := by refine ⟨?_, the_library_rejects_signed_length_determination_even_from_the_whole_curve 2 (by norm_num)⟩ apply records.record_constraint_mono false (records.recordAt false 2) (fun value => value ^ 2 = (2 : Real) ^ 2) (fun value => |value| = 2) (the_rate_record_constrains_the_squared_inverse_length 2 (by norm_num)) intro value square nlinarith [sq_abs value, abs_nonneg value] theorem amplitude_access_refines_rate_only_access : records.RecordsRefineAt true false := by intro first second _firstAllowed _secondAllowed same change (crossSection first, (0 : Complex)) = (crossSection second, 0) have curves : crossSection first = crossSection second := congrArg Prod.fst same exact Prod.ext curves rfl theorem the_library_determines_the_signed_parameter_with_complex_amplitude_access (inverseLength : Real) (nonzero : inverseLength ≠ 0) : records.RecordDeterminesValueAt true (records.recordAt true inverseLength) inverseLength := records.calibrated_decoder_determines_record_value true (fun record => -(Complex.I + record.2⁻¹).re) (fun candidate _ => the_complex_amplitude_supplies_a_calibrated_signed_readout candidate) inverseLength nonzero theorem the_library_preserves_the_magnitude_constraint_under_refined_access : records.RecordConstrainsValueAt true (records.recordAt true 2) (fun value => |value| = 2) := records.finer_records_preserve_value_constraints true false amplitude_access_refines_rate_only_access 2 (by norm_num [records]) (fun value => |value| = 2) the_library_retains_magnitude_information_despite_the_sign_ambiguity.1 theorem rate_only_access_does_not_refine_amplitude_access : ¬records.RecordsRefineAt false true := by intro refines have finer := records.finer_records_preserve_determined_values false true refines 2 (by norm_num [records]) 2 (the_library_determines_the_signed_parameter_with_complex_amplitude_access 2 (by norm_num)) exact the_library_rejects_signed_length_determination_even_from_the_whole_curve 2 (by norm_num) ⟨2, finer⟩ theorem the_two_test_amplitudes_have_equal_rates_and_opposite_real_parts : amplitude 2 1 = (-2 + Complex.I) / 5 ∧ amplitude (-2) 1 = (2 + Complex.I) / 5 ∧ crossSection 2 topMomentum = 4 * Real.pi / 5 ∧ crossSection (-2) = crossSection 2 := by refine ⟨?_, ?_, ?_, reversing_the_inverse_length_preserves_every_observed_cross_section 2⟩ · norm_num [amplitude, NeutralParameterComparison.amplitude, PhysicsLogic.Framework.EffectiveRangeExpansion.twoParameterPhaseFunction, reducedAmplitude, denominator, Complex.inv_def, Complex.ext_iff, Complex.normSq_apply] · norm_num [amplitude, NeutralParameterComparison.amplitude, PhysicsLogic.Framework.EffectiveRangeExpansion.twoParameterPhaseFunction, reducedAmplitude, denominator, Complex.inv_def, Complex.ext_iff, Complex.normSq_apply] · rw [the_whole_cross_section_curve_is_computed] norm_num [topMomentum] ring #check (the_library_retains_magnitude_information_despite_the_sign_ambiguity : records.RecordConstrainsValueAt false (records.recordAt false 2) (fun value => |value| = 2) ∧ ¬∃ value, records.RecordDeterminesValueAt false (records.recordAt false 2) value) #check (rate_only_access_does_not_refine_amplitude_access : ¬records.RecordsRefineAt false true) end CrossSectionRecords namespace RangeTruncation /-! KSW's pionless expansion treats the effective-range insertion separately from unknown higher coefficients of k cot(delta). The bounds below concern that selected insertion. The reference length in LowEnergyHierarchyAt is not a proved range of a nuclear potential or a bound on every omitted coefficient. -/ theorem the_declared_hierarchy_bounds_the_relative_insertion (data : LowEnergyData) (hierarchy : data.LowEnergyHierarchyAt) : |data.effectiveRange / 2 * data.momentum ^ 2| / data.momentum ≤ 1 / 32 := by have positive := hierarchy.2.2.2.1 have rangeBound : |data.effectiveRange| * data.momentum ≤ 1 / 16 := by calc _ ≤ data.referenceShortDistanceLength * data.momentum := mul_le_mul_of_nonneg_right hierarchy.2.1 positive.le _ = data.momentum * data.referenceShortDistanceLength := mul_comm _ _ _ ≤ _ := hierarchy.2.2.2.2 have relative : |data.effectiveRange / 2 * data.momentum ^ 2| / data.momentum = |data.effectiveRange| * data.momentum / 2 := by rw [abs_mul, abs_div, abs_of_pos (by norm_num : (0 : Real) < 2), abs_of_nonneg (sq_nonneg data.momentum)] field_simp rw [relative] linarith theorem the_single_insertion_has_a_small_relative_norm (data : LowEnergyData) (scale : Real) (hierarchy : data.LowEnergyHierarchyAt) (admissible : data.AdmissibleScaleAt scale) : ‖data.correction scale‖ ≤ (1 / 32 : Real) * ‖data.leading scale‖ := by rw [data.running_insertion_recovers_effective_range_correction scale admissible, data.running_contact_recovers_leading_scattering_length_amplitude scale admissible] exact (real_inverse_range_insertion_has_relative_bound _ _ _ admissible.1).trans (mul_le_mul_of_nonneg_right (the_declared_hierarchy_bounds_the_relative_insertion data hierarchy) (norm_nonneg _)) theorem resumming_only_the_range_term_has_a_quadratic_relative_error (data : LowEnergyData) (scale : Real) (hierarchy : data.LowEnergyHierarchyAt) (admissible : data.AdmissibleScaleAt scale) : ‖reducedAmplitude (-data.inverseScatteringLength + data.effectiveRange / 2 * data.momentum ^ 2) data.momentum - (data.leading scale + data.correction scale)‖ ≤ (1 / 1024 : Real) * ‖data.leading scale‖ := by rw [data.running_insertion_recovers_effective_range_correction scale admissible, data.running_contact_recovers_leading_scattering_length_amplitude scale admissible] have small := the_declared_hierarchy_bounds_the_relative_insertion data hierarchy have nonnegative : 0 ≤ |data.effectiveRange / 2 * data.momentum ^ 2| / data.momentum := div_nonneg (abs_nonneg _) admissible.1.le have squared : (|data.effectiveRange / 2 * data.momentum ^ 2| / data.momentum) ^ 2 ≤ 1 / 1024 := by nlinarith exact (real_inverse_range_shift_has_relative_quadratic_error _ _ _ admissible.1).trans (mul_le_mul_of_nonneg_right squared (norm_nonneg _)) theorem a_physical_phase_remainder_needs_its_own_error_budget (data : LowEnergyData) (scale actualPhase phaseError : Real) (hierarchy : data.LowEnergyHierarchyAt) (admissible : data.AdmissibleScaleAt scale) (phaseControl : |actualPhase - (-data.inverseScatteringLength + data.effectiveRange / 2 * data.momentum ^ 2)| ≤ phaseError) : ‖reducedAmplitude actualPhase data.momentum - (data.leading scale + data.correction scale)‖ ≤ phaseError / data.momentum ^ 2 + (1 / 1024 : Real) * ‖data.leading scale‖ := by calc _ ≤ ‖reducedAmplitude actualPhase data.momentum - reducedAmplitude (-data.inverseScatteringLength + data.effectiveRange / 2 * data.momentum ^ 2) data.momentum‖ + ‖reducedAmplitude (-data.inverseScatteringLength + data.effectiveRange / 2 * data.momentum ^ 2) data.momentum - (data.leading scale + data.correction scale)‖ := by simpa only [dist_eq_norm] using dist_triangle (reducedAmplitude actualPhase data.momentum) (reducedAmplitude (-data.inverseScatteringLength + data.effectiveRange / 2 * data.momentum ^ 2) data.momentum) (data.leading scale + data.correction scale) _ ≤ _ := add_le_add (controlled_phase_error_bounds_amplitude_error _ _ _ _ _ admissible.1 le_rfl phaseControl) (resumming_only_the_range_term_has_a_quadratic_relative_error data scale hierarchy admissible) /-- A unitary on-shell diagnostic with the same first two coefficients but a large quartic coefficient. It is not a finite-range potential realization or a counterexample to a power counting that controls all higher coefficients. -/ theorem two_low_energy_coefficients_and_unitarity_do_not_bound_the_omitted_terms : let phase : Real → Real := fun momentum => 1 + momentum ^ 2 / 32 - 33 * momentum ^ 4 / 32 nuclearData.LowEnergyHierarchyAt ∧ PhysicsLogic.Framework.EffectiveRangeExpansion.NonvacuousEffectiveRangeExpansionAt phase nuclearData.inverseScatteringLength nuclearData.effectiveRange ∧ (∀ momentum : Real, 0 < momentum → NonvacuousElasticSWaveAt (phase momentum) momentum (reducedAmplitude (phase momentum) momentum)) ∧ (1 / 2 : Real) < ‖reducedAmplitude (phase nuclearData.momentum) nuclearData.momentum - (nuclearData.leading 0 + nuclearData.correction 0)‖ := by dsimp only refine ⟨by norm_num [LowEnergyData.LowEnergyHierarchyAt, nuclearData], ?_, fun momentum positive => real_effective_range_function_realizes_elastic_scattering _ _ positive, ?_⟩ · apply PhysicsLogic.Framework.EffectiveRangeExpansion.quartic_control_establishes_nonvacuous_effective_range_expansion refine ⟨1, 33 / 32, by norm_num, by norm_num, ?_⟩ intro momentum positive _small have difference : (1 + momentum ^ 2 / 32 - 33 * momentum ^ 4 / 32) - PhysicsLogic.Framework.EffectiveRangeExpansion.twoParameterPhaseFunction nuclearData.inverseScatteringLength nuclearData.effectiveRange momentum = -(33 / 32 * momentum ^ 4) := by simp only [PhysicsLogic.Framework.EffectiveRangeExpansion.twoParameterPhaseFunction, nuclearData] ring rw [difference, abs_neg, abs_of_nonneg (by positivity)] · rw [nuclear_terms_have_nonzero_derivative_insertion.1, nuclear_terms_have_nonzero_derivative_insertion.2] have squared : ‖reducedAmplitude (1 + nuclearData.momentum ^ 2 / 32 - 33 * nuclearData.momentum ^ 4 / 32) nuclearData.momentum - ((1 + Complex.I) / 2 + -Complex.I / 64)‖ ^ 2 = 2113 / 4096 := by rw [Complex.sq_norm] norm_num [nuclearData, reducedAmplitude, denominator, Complex.inv_def, Complex.normSq_apply, Complex.re_ofNat, Complex.im_ofNat, Complex.div_re, Complex.div_im] have nonnegative := norm_nonneg (reducedAmplitude (1 + nuclearData.momentum ^ 2 / 32 - 33 * nuclearData.momentum ^ 4 / 32) nuclearData.momentum - ((1 + Complex.I) / 2 + -Complex.I / 64)) nlinarith end RangeTruncation namespace ReadoutComparison open PhysicsLogic.Philosophy.Representation open PhysicsLogic.Paradigm.ScaleAndRegime /-! KSW's original amplitude relation (author TeX label 8) retains the real function k cot(delta). Bethe 1949 p. 40 (17) instead gives the single-channel cross section 4 pi |f|^2; the spin-averaged neutron-proton total is different. These readout tests do not identify delta as a unique real angle or reconstruct a nuclear potential. Algebraic equivalence is separate from approximation stability and from the positive-momentum elastic domain. -/ /-- Nonemptiness is shared by all three total readout relations. Positivity of the momentum band, approximation control and phase recovery are separate. -/ theorem all_three_readouts_have_the_same_active_momentum_sector (phase : Real → Real) (band : Set Real) (sector : Real → Prop) : (phaseApproximationContext.ActiveTargetSectorAt phase band sector ↔ ∃ momentum, sector momentum ∧ momentum ∈ band) ∧ (amplitudeApproximationContext.ActiveTargetSectorAt phase band sector ↔ ∃ momentum, sector momentum ∧ momentum ∈ band) ∧ ((amplitudeApproximationContext.predictions.mapValues (fun _ amplitude => 4 * Real.pi * Complex.normSq amplitude)).ActivePredictionSectorAt phase band sector ↔ ∃ momentum, sector momentum ∧ momentum ∈ band) := by have base : phaseApproximationContext.predictions.ActivePredictionSectorAt phase band sector ↔ ∃ momentum, sector momentum ∧ momentum ∈ band := by constructor · rintro ⟨momentum, _value, selected, available, _predicted⟩ exact ⟨momentum, selected, available⟩ · rintro ⟨momentum, selected, available⟩ exact ⟨momentum, phase momentum, selected, available, rfl⟩ have amplitude : amplitudeApproximationContext.predictions.ActivePredictionSectorAt phase band sector ↔ ∃ momentum, sector momentum ∧ momentum ∈ band := (active_prediction_sector_iff_value_readout phaseApproximationContext.predictions (fun momentum value => reducedAmplitude value momentum) phase band sector).symm.trans base exact ⟨base, amplitude, (active_prediction_sector_iff_value_readout amplitudeApproximationContext.predictions (fun _ value => 4 * Real.pi * Complex.normSq value) phase band sector).symm.trans amplitude⟩ /-- The formulas remain total at zero momentum in Lean, but that point is outside the declared elastic approximation regime. Activity does not repair it. -/ theorem active_totalized_readouts_do_not_establish_physical_validity : let phase : Real → Real := fun _ => 0 let band : Set Real := {0} let sector : Real → Prop := fun _ => True phaseApproximationContext.ActiveTargetSectorAt phase band sector ∧ amplitudeApproximationContext.ActiveTargetSectorAt phase band sector ∧ (amplitudeApproximationContext.predictions.mapValues (fun _ amplitude => 4 * Real.pi * Complex.normSq amplitude)).ActivePredictionSectorAt phase band sector ∧ ¬phaseApproximationContext.validity.validAt phase band ∧ ¬amplitudeApproximationContext.validity.validAt phase band := by dsimp only have active := all_three_readouts_have_the_same_active_momentum_sector (fun _ => 0) {0} (fun _ => True) have inhabited : ∃ momentum : Real, True ∧ momentum ∈ ({0} : Set Real) := ⟨0, trivial, by simp⟩ refine ⟨active.1.mpr inhabited, active.2.1.mpr inhabited, active.2.2.mpr inhabited, ?_, ?_⟩ all_goals intro valid have impossible : (0 : Real) < 0 := valid 0 (by simp) exact (lt_irrefl 0) impossible theorem complex_amplitude_equivalence_preserves_the_effective_range_function (left right : Real → Real) (band : Set Real) (sector : Real → Prop) : phaseApproximationContext.predictions.EmpiricallyEquivalent left right band sector ↔ amplitudeApproximationContext.predictions.EmpiricallyEquivalent left right band sector := by apply empirical_equivalence_iff_readout_equivalence_of_separating_predictions phaseApproximationContext.predictions (fun momentum value => reducedAmplitude value momentum) intro momentum _selected _available leftValue rightValue _leftPrediction _rightPrediction same have denominators := congrArg (fun value : Complex => value⁻¹) same simp only [reducedAmplitude, inv_inv] at denominators simpa [denominator] using congrArg Complex.re denominators /-- A specified nonnegative branch suffices for the intensity readout to separate the predicted inverse-amplitude values. The branch is an additional input, not a consequence of the cross section or of elastic unitarity. -/ theorem a_nonnegative_branch_makes_cross_section_agreement_reflective (left right : Real → Real) (band : Set Real) (sector : Real → Prop) (branch : ∀ momentum, sector momentum → momentum ∈ band → 0 ≤ left momentum ∧ 0 ≤ right momentum) : phaseApproximationContext.predictions.EmpiricallyEquivalent left right band sector ↔ (phaseApproximationContext.predictions.mapValues (fun momentum value => 4 * Real.pi * Complex.normSq (reducedAmplitude value momentum))).EmpiricallyEquivalent left right band sector := by apply empirical_equivalence_iff_readout_equivalence_of_separating_predictions intro momentum selected available leftValue rightValue leftPrediction rightPrediction same change leftValue = left momentum at leftPrediction change rightValue = right momentum at rightPrediction subst leftValue subst rightValue have normEquality := mul_left_cancel₀ (by positivity : (4 * Real.pi : Real) ≠ 0) same simp only [reducedAmplitude, Complex.normSq_inv] at normEquality have denominatorEquality := congrArg (fun value : Real => value⁻¹) normEquality simp only [inv_inv] at denominatorEquality simp [denominator, Complex.normSq_apply] at denominatorEquality have nonnegative := branch momentum selected available nlinarith [nonnegative.1, nonnegative.2] /-- Equal intensity throughout a positive-momentum sector does not identify the complex amplitude, even when both on-shell models obey elastic unitarity. The constant k cot(delta) examples are not finite-range potential realizations. -/ theorem elastic_cross_section_equivalence_does_not_determine_complex_amplitudes : let left : Real → Real := fun _ => 1 let right : Real → Real := fun _ => -1 let band : Set Real := Set.Ioi 0 let sector : Real → Prop := fun momentum => 0 < momentum let readout := amplitudeApproximationContext.predictions.mapValues (fun _ amplitude => 4 * Real.pi * Complex.normSq amplitude) (∀ momentum, 0 < momentum → NonvacuousElasticSWaveAt (left momentum) momentum (reducedAmplitude (left momentum) momentum) ∧ NonvacuousElasticSWaveAt (right momentum) momentum (reducedAmplitude (right momentum) momentum)) ∧ readout.EmpiricallyEquivalent left right band sector ∧ ¬amplitudeApproximationContext.predictions.EmpiricallyEquivalent left right band sector := by dsimp only have intensity (momentum : Real) : 4 * Real.pi * Complex.normSq (reducedAmplitude 1 momentum) = 4 * Real.pi * Complex.normSq (reducedAmplitude (-1) momentum) := by simp [reducedAmplitude, denominator, Complex.normSq_apply] refine ⟨fun momentum positive => ⟨real_effective_range_function_realizes_elastic_scattering _ _ positive, real_effective_range_function_realizes_elastic_scattering _ _ positive⟩, ?_, ?_⟩ · apply active_prediction_and_exact_agreement_establish_empirical_equivalence · exact ⟨1, 4 * Real.pi * Complex.normSq (reducedAmplitude 1 1), by norm_num, by norm_num [amplitudeApproximationContext, ApproximationContext.mapValues, PredictionContext.mapValues, phaseApproximationContext], ⟨reducedAmplitude 1 1, ⟨1, rfl, rfl⟩, rfl⟩⟩ · intro momentum _selected _available output change (∃ amplitude, (∃ value, value = (1 : Real) ∧ amplitude = reducedAmplitude value momentum) ∧ output = 4 * Real.pi * Complex.normSq amplitude) ↔ (∃ amplitude, (∃ value, value = (-1 : Real) ∧ amplitude = reducedAmplitude value momentum) ∧ output = 4 * Real.pi * Complex.normSq amplitude) simp only [exists_eq_left, intensity] · intro equivalent have leftPrediction : amplitudeApproximationContext.predictions.predicts (fun _ => 1) 1 (reducedAmplitude 1 1) := ⟨1, rfl, rfl⟩ have rightPrediction := (equivalent.2 1 (by norm_num) (by norm_num [amplitudeApproximationContext, ApproximationContext.mapValues, PredictionContext.mapValues, phaseApproximationContext]) (reducedAmplitude 1 1)).mp leftPrediction obtain ⟨value, valueEq, amplitudes⟩ := rightPrediction change value = (-1 : Real) at valueEq subst value have realParts := congrArg Complex.re amplitudes norm_num [reducedAmplitude, denominator, Complex.inv_re, Complex.normSq_apply] at realParts end ReadoutComparison namespace ReadoutStability /- Each member is the constant, analytic inverse-amplitude function K(p)=shift, compared with K(p)=0. The shift changes scattering length, not the subtraction scale of one fixed system. These are unitary on-shell diagnostics, not nuclear fits, finite-range potential constructions, or a regulator-removal theorem. -/ theorem a_constant_inverse_amplitude_shift_has_exact_uniform_phase_error (shift error : Real) : phaseApproximationContext.ControlledApproximation (fun _ => shift) (fun _ => 0) (Set.Ioc 0 1) (fun _ => True) error ↔ |shift| ≤ error := by rw [controlled_phase_approximation_iff_nonempty_sector_and_uniform_error] constructor · intro controlled simpa using controlled.2.2 1 trivial (by norm_num) · intro bound exact ⟨fun _ inside => inside.1, ⟨1, trivial, by norm_num⟩, fun _ _ _ => by simpa using bound⟩ theorem inverse_amplitude_functions_converge_uniformly_on_the_positive_band : ∀ tolerance : Real, 0 < tolerance → ∃ cutoff : Real, 0 < cutoff ∧ ∀ shift : Real, 0 < shift → shift < cutoff → phaseApproximationContext.ControlledApproximation (fun _ => shift) (fun _ => 0) (Set.Ioc 0 1) (fun _ => True) tolerance := by intro tolerance positive refine ⟨tolerance, positive, ?_⟩ intro shift shifted small rw [a_constant_inverse_amplitude_shift_has_exact_uniform_phase_error, abs_of_pos shifted] exact small.le theorem the_moving_momentum_exposes_the_amplitude_error (shift : Real) (positive : 0 < shift) : (reducedAmplitude 0 shift - reducedAmplitude shift shift).im = 1 / (2 * shift) ∧ 1 / (2 * shift) ≤ ‖reducedAmplitude shift shift - reducedAmplitude 0 shift‖ := by have imaginaryValue : (reducedAmplitude 0 shift - reducedAmplitude shift shift).im = 1 / (2 * shift) := by have nonzero := ne_of_gt positive simp [reducedAmplitude, denominator, Complex.inv_im, Complex.normSq_apply] field_simp ring refine ⟨imaginaryValue, ?_⟩ have bound := Complex.abs_im_le_norm (reducedAmplitude 0 shift - reducedAmplitude shift shift) simpa only [imaginaryValue, abs_of_pos (by positivity : 0 < 1 / (2 * shift)), norm_sub_rev] using bound theorem uniform_phase_control_and_unitarity_do_not_give_uniform_amplitude_control (shift : Real) (positive : 0 < shift) (atMostOne : shift ≤ 1) : phaseApproximationContext.ControlledApproximation (fun _ => shift) (fun _ => 0) (Set.Ioc 0 1) (fun _ => True) shift ∧ (∀ momentum, 0 < momentum → NonvacuousElasticSWaveAt shift momentum (reducedAmplitude shift momentum) ∧ NonvacuousElasticSWaveAt 0 momentum (reducedAmplitude 0 momentum)) ∧ ¬amplitudeApproximationContext.ControlledApproximation (fun _ => shift) (fun _ => 0) (Set.Ioc 0 1) (fun _ => True) (1 / 4) := by refine ⟨?_, fun momentum inDomain => ⟨real_effective_range_function_realizes_elastic_scattering _ _ inDomain, real_effective_range_function_realizes_elastic_scattering _ _ inDomain⟩, ?_⟩ · rw [a_constant_inverse_amplitude_shift_has_exact_uniform_phase_error, abs_of_pos positive] · rw [controlled_amplitude_approximation_iff_nonempty_sector_and_uniform_error] intro controlled have bound := controlled.2.2 shift trivial ⟨positive, atMostOne⟩ have imaginary := (the_moving_momentum_exposes_the_amplitude_error shift positive).2 have impossible : 1 / (2 * shift) ≤ (1 : Real) / 4 := imaginary.trans bound have scaled := (div_le_iff₀ (by positivity : 0 < 2 * shift)).mp impossible linarith theorem a_positive_momentum_floor_restores_uniform_amplitude_convergence (floor : Real) (positive : 0 < floor) (atMostOne : floor ≤ 1) : ∀ tolerance : Real, 0 < tolerance → ∃ cutoff : Real, 0 < cutoff ∧ ∀ shift : Real, 0 < shift → shift < cutoff → amplitudeApproximationContext.ControlledApproximation (fun _ => shift) (fun _ => 0) (Set.Icc floor 1) (fun _ => True) tolerance := by intro tolerance accurate refine ⟨tolerance * floor ^ 2, mul_pos accurate (sq_pos_of_pos positive), ?_⟩ intro shift shifted small rw [controlled_amplitude_approximation_iff_nonempty_sector_and_uniform_error] refine ⟨fun _ inside => positive.trans_le inside.1, ⟨floor, trivial, le_rfl, atMostOne⟩, ?_⟩ intro momentum _selected inside have bound := controlled_phase_error_bounds_amplitude_error shift 0 momentum shift floor positive inside.1 (by simp [abs_of_pos shifted]) exact bound.trans (le_of_lt ((div_lt_iff₀ (sq_pos_of_pos positive)).mpr small)) /-- Every fixed positive momentum admits a cutoff, but it may depend on that momentum. This does not assert a uniform cutoff down to threshold. -/ theorem every_fixed_positive_momentum_has_amplitude_convergence (momentum : Real) (positive : 0 < momentum) : ∀ tolerance : Real, 0 < tolerance → ∃ cutoff : Real, 0 < cutoff ∧ ∀ shift : Real, 0 < shift → shift < cutoff → ‖reducedAmplitude shift momentum - reducedAmplitude 0 momentum‖ < tolerance := by intro tolerance accurate refine ⟨tolerance * momentum ^ 2, mul_pos accurate (sq_pos_of_pos positive), ?_⟩ intro shift shifted small exact lt_of_le_of_lt (controlled_phase_error_bounds_amplitude_error shift 0 momentum shift momentum positive le_rfl (by simp [abs_of_pos shifted])) ((div_lt_iff₀ (sq_pos_of_pos positive)).mpr small) /-- The fixed band has no threshold problem. The inverse readout can still be ill-conditioned because both amplitudes become small. -/ theorem large_phase_values_have_small_amplitude_separation (large momentum : Real) (largePositive : 0 < large) (positive : 0 < momentum) : ‖reducedAmplitude large momentum - reducedAmplitude (2 * large) momentum‖ ≤ 1 / (2 * large) := by have firstBound : large ≤ ‖denominator large momentum‖ := by simpa [denominator, abs_of_pos largePositive] using Complex.abs_re_le_norm (denominator large momentum) have secondBound : 2 * large ≤ ‖denominator (2 * large) momentum‖ := by simpa [denominator, abs_of_pos (by positivity : 0 < 2 * large)] using Complex.abs_re_le_norm (denominator (2 * large) momentum) rw [phase_difference_gives_exact_amplitude_distance _ _ _ positive] have numerator : |large - 2 * large| = large := by rw [show large - 2 * large = -large by ring, abs_neg, abs_of_pos largePositive] rw [numerator] calc large / (‖denominator large momentum‖ * ‖denominator (2 * large) momentum‖) ≤ large / (large * (2 * large)) := div_le_div_of_nonneg_left largePositive.le (by positivity) (mul_le_mul firstBound secondBound (by positivity) (norm_nonneg _)) _ = 1 / (2 * large) := by field_simp theorem exact_unitarity_and_a_positive_momentum_floor_do_not_control_inverse_recovery : ∀ tolerance : Real, 0 < tolerance → ∃ large : Real, 1 ≤ large ∧ (∀ momentum, 0 < momentum → NonvacuousElasticSWaveAt large momentum (reducedAmplitude large momentum) ∧ NonvacuousElasticSWaveAt (2 * large) momentum (reducedAmplitude (2 * large) momentum)) ∧ amplitudeApproximationContext.ControlledApproximation (fun _ => large) (fun _ => 2 * large) (Set.Icc 1 2) (fun _ => True) tolerance ∧ ¬phaseApproximationContext.ControlledApproximation (fun _ => large) (fun _ => 2 * large) (Set.Icc 1 2) (fun _ => True) (1 / 2) := by intro tolerance positive let large := 1 + 1 / tolerance have largeAtLeastOne : 1 ≤ large := by have inversePositive : 0 < 1 / tolerance := one_div_pos.mpr positive dsimp [large] linarith have largePositive : 0 < large := lt_of_lt_of_le (by norm_num) largeAtLeastOne have small : 1 / (2 * large) ≤ tolerance := by apply (div_le_iff₀ (by positivity : 0 < 2 * large)).mpr dsimp [large] have identity : tolerance * (1 / tolerance) = 1 := by field_simp nlinarith refine ⟨large, largeAtLeastOne, fun momentum inDomain => ⟨real_effective_range_function_realizes_elastic_scattering _ _ inDomain, real_effective_range_function_realizes_elastic_scattering _ _ inDomain⟩, ?_, ?_⟩ · rw [controlled_amplitude_approximation_iff_nonempty_sector_and_uniform_error] exact ⟨fun _ inside => lt_of_lt_of_le (by norm_num) inside.1, ⟨1, trivial, by norm_num⟩, fun momentum _ inside => (large_phase_values_have_small_amplitude_separation large momentum largePositive (lt_of_lt_of_le (by norm_num) inside.1)).trans small⟩ · rw [controlled_phase_approximation_iff_nonempty_sector_and_uniform_error] intro recovered have bound := recovered.2.2 1 trivial (by norm_num) have absolute : |large - 2 * large| = large := by rw [show large - 2 * large = -large by ring, abs_neg, abs_of_pos largePositive] rw [absolute] at bound linarith theorem bounded_phase_values_on_a_fixed_band_allow_stable_inverse_recovery (left right : Real → Real) (error : Real) (controlled : amplitudeApproximationContext.ControlledApproximation left right (Set.Icc 1 2) (fun _ => True) error) (bounded : ∀ momentum ∈ Set.Icc (1 : Real) 2, |left momentum| ≤ 1 ∧ |right momentum| ≤ 1) : phaseApproximationContext.ControlledApproximation left right (Set.Icc 1 2) (fun _ => True) (9 * error) := by have lower (value momentum : Real) (valueBound : |value| ≤ 1) (inBand : momentum ∈ Set.Icc (1 : Real) 2) : 1 / 3 ≤ ‖reducedAmplitude value momentum‖ := by have positive : 0 < momentum := lt_of_lt_of_le (by norm_num) inBand.1 have normPositive : 0 < ‖denominator value momentum‖ := norm_pos_iff.mpr (denominator_ne_zero_of_positive_momentum value momentum positive) have upper : ‖denominator value momentum‖ ≤ 3 := by calc ‖denominator value momentum‖ ≤ ‖(value : Complex)‖ + ‖Complex.I * (momentum : Complex)‖ := norm_sub_le _ _ _ = |value| + momentum := by simp [abs_of_pos positive] _ ≤ 3 := by linarith [inBand.2] simpa [reducedAmplitude, norm_inv, one_div] using one_div_le_one_div_of_le normPositive upper have recovered := controlled_amplitude_approximation_recovers_the_phase left right (Set.Icc 1 2) (fun _ => True) error (1 / 3) controlled (by norm_num) (fun momentum _ inside => ⟨lower _ _ (bounded momentum inside).1 inside, lower _ _ (bounded momentum inside).2 inside⟩) convert recovered using 1 ring end ReadoutStability theorem the_real_phase_formula_supplies_both_unitarity_readouts (phase momentum : Real) (amplitude : Complex) (positive : 0 < momentum) (formula : amplitude = ((phase : Complex) - Complex.I * (momentum : Complex))⁻¹) : Complex.normSq (1 + 2 * Complex.I * (momentum : Complex) * amplitude) = 1 ∧ amplitude.im = momentum * Complex.normSq amplitude := by exact nonvacuous_elastic_s_wave_has_unitarity_and_optical_theorem phase momentum amplitude ((nonvacuous_elastic_s_wave_iff_explicit_amplitude _ _ _).mpr ⟨positive, formula⟩) theorem zero_contact_is_unitary_but_outside_the_finite_inverse_range_chart (scale momentum : Real) (positive : 0 < momentum) : contactAmplitude 0 scale momentum = 0 ∧ ElasticUnitaryAt momentum 0 ∧ OpticalTheoremAt momentum 0 ∧ ¬∃ phase : Real, NonvacuousElasticSWaveAt phase momentum 0 := by refine ⟨by simp [contactAmplitude], by simp [ElasticUnitaryAt, sMatrix], by simp [OpticalTheoremAt], ?_⟩ rintro ⟨phase, physical⟩ have nonzero : reducedAmplitude phase momentum ≠ 0 := inv_ne_zero (denominator_ne_zero_of_positive_momentum _ _ positive) exact nonzero physical.2.symm /-- Fixed-unit, on-shell algebraic data, not a nuclear fit. The same amplitude fails the norm-square test if the source's factor 2 pi is changed to 4 pi. -/ theorem the_bubble_amplitude_needs_the_source_s_matrix_normalization : let mass : Real := 4 * Real.pi let amplitude : Complex := (-1 + Complex.I) / 2 0 < mass ∧ (1 + (mass : Complex) * Complex.I / (4 * Real.pi : Real) ≠ 0) ∧ Complex.I * amplitude = -Complex.I / (1 + (mass : Complex) * Complex.I / (4 * Real.pi : Real)) ∧ Complex.normSq (1 + Complex.I * (mass / (2 * Real.pi) : Real) * amplitude) = 1 ∧ Complex.normSq (1 + Complex.I * (mass / (4 * Real.pi) : Real) * amplitude) = 1 / 2 := by have denominator : contactDenominator 1 0 1 ≠ 0 := contact_denominator_ne_zero_of_positive_momentum _ _ _ (by norm_num) have unitary := real_contact_amplitude_is_elastic_unitary 1 0 1 denominator have computed : contactAmplitude 1 0 1 = (-1 + Complex.I) / 2 := by norm_num [contactAmplitude, contactDenominator, Complex.ext_iff, Complex.div_re, Complex.div_im, Complex.normSq_apply] rw [computed] at unitary dsimp refine ⟨by positivity, ?_, ?_, ?_, ?_⟩ · norm_num [Complex.ext_iff, Real.pi_ne_zero] · norm_num [Complex.ext_iff, Complex.div_re, Complex.div_im, Complex.normSq_apply, Real.pi_ne_zero] · rw [show 4 * Real.pi / (2 * Real.pi) = (2 : Real) by field_simp; ring] simpa [ElasticUnitaryAt, sMatrix, mul_comm] using unitary · norm_num [Complex.mul_re, Complex.mul_im, Complex.div_re, Complex.div_im, Complex.normSq_apply, Real.pi_ne_zero] end end PhysicsLogicConsumer.NuclearScattering