import PhysicsLogic.Papers.KaplanSavageWise1998 import PhysicsLogic.Papers.KaplanSavageWise1998.SourceMap import PhysicsLogic.Logic.Semantics /-! # Semantic Coverage for Kaplan-Savage-Wise 1998 Every source atom is interpreted in paper-local nuclear-scattering semantics. Route certificates derive their outputs from explicit physical, calculation, fit, approximation, and deferred-work hypotheses. -/ set_option autoImplicit false namespace PhysicsLogic.Papers.KaplanSavageWise1998 open PhysicsLogic.Logic universe uChannel uScale uMomentum uCoupling uTerm uOrder uRegime uFit structure SemanticContext (Channel : Type uChannel) (Scale : Type uScale) (Momentum : Type uMomentum) (Coupling : Type uCoupling) (Term : Type uTerm) (Order : Type uOrder) (Regime : Type uRegime) (Fit : Type uFit) where framework : NuclearScatteringFramework Channel Scale Momentum Coupling Term Order Regime Fit lowChannel : Channel lowScale : Scale lowMomentum : Momentum naturalMSChannel : Channel largeLengthMSChannel : Channel msScale : Scale msMomentum : Momentum expansionChannel : Channel expansionScale : Scale expansionMomentum : Momentum singletFit : Fit coupledChannel : Channel coupledFit : Fit namespace SemanticContext variable {Channel : Type uChannel} {Scale : Type uScale} {Momentum : Type uMomentum} {Coupling : Type uCoupling} {Term : Type uTerm} {Order : Type uOrder} {Regime : Type uRegime} {Fit : Type uFit} def interpretAtom (context : SemanticContext Channel Scale Momentum Coupling Term Order Regime Fit) : Atom → Prop | .pionlessPDSSetup => context.framework.pionlessMomentum context.lowMomentum ∧ context.framework.largeScatteringLength context.lowChannel ∧ context.framework.pdsSubtractionAt context.lowScale ∧ (context.framework.pionlessLeadingContactOrderAt context.lowChannel context.lowScale context.lowMomentum = -1 ∧ context.framework.pionlessBubbleLoopOrderAt context.lowScale context.lowMomentum = 1) | .pdsLoopCalculation => context.framework.PDSLoopCalculation context.lowChannel context.lowScale context.lowMomentum | .bubbleResummationCalculation => context.framework.BubbleResummationCalculation context.lowChannel context.lowScale context.lowMomentum | .pionlessUnitarityCalculation => context.framework.PionlessUnitarityCalculation context.lowChannel context.lowScale context.lowMomentum | .pdsLoopIntegral => context.framework.pdsLoopIntegralObtained context.lowChannel context.lowScale context.lowMomentum | .pdsLoopFormula => context.framework.EquationFivePDSLoopFormulaAt | .pdsAmplitude => context.framework.pdsAmplitudeObtained context.lowChannel context.lowScale context.lowMomentum | .pdsAmplitudeFormula => context.framework.EquationSixPDSAmplitudeFormulaAt | .unitaryAmplitude => context.framework.amplitudeConsistentWithUnitarity context.lowChannel context.lowScale context.lowMomentum | .effectiveRangeMatching => context.framework.effectiveRangeDataMatched context.lowChannel | .physicalScaleIndependenceRequirement => context.framework.physicalAmplitudeRequiredScaleIndependent context.lowChannel context.lowMomentum | .pionlessRGCalculation => context.framework.PionlessRGCalculation context.lowChannel context.lowScale context.lowMomentum | .exactC0C2BetaFunctions => ∀ mu, (context.framework.pionlessRGFlow context.lowChannel).NonpoleAt mu -> (context.framework.pionlessRGFlow context.lowChannel).ExactBetaDerivativesAt mu | .c0C2PionlessRGControl => (∀ mu, (context.framework.pionlessRGFlow context.lowChannel).NonpoleAt mu -> (context.framework.pionlessRGFlow context.lowChannel).ExactBetaDerivativesAt mu) ∧ context.framework.equationElevenPionlessRunningValuesAt context.lowChannel | .fullAmplitudeScaleIndependent => context.framework.pionlessAmplitudeScaleIndependent context.lowChannel context.lowMomentum | .naturalMSSetup => context.framework.naturalScatteringLength context.naturalMSChannel ∧ context.framework.minimalSubtractionAt context.msScale ∧ context.framework.momentumSmallComparedWithShortRangeScale context.naturalMSChannel context.msMomentum | .largeLengthMSSetup => context.framework.largeScatteringLength context.largeLengthMSChannel ∧ context.framework.minimalSubtractionAt context.msScale ∧ context.framework.pionlessMomentum context.msMomentum | .naturalMSPowerCountingCalculation => context.framework.NaturalMSPowerCountingCalculation context.naturalMSChannel context.msScale context.msMomentum | .largeLengthMSRestrictionCalculation => context.framework.LargeLengthMSRestrictionCalculation context.largeLengthMSChannel context.msScale | .naturalMSCountingValid => context.framework.ordinaryMSCountingValid context.naturalMSChannel context.msMomentum | .largeLengthMSValidityRequiresInverseLengthWindow => context.framework.ordinaryMSCountingValid context.largeLengthMSChannel context.msMomentum → context.framework.momentumSmallComparedWithInverseScatteringLength context.largeLengthMSChannel context.msMomentum | .largeLengthMSRangeRestricted => context.framework.minimalSubtractionRangeRestricted context.largeLengthMSChannel | .largeLengthScalingSetup => context.framework.largeScatteringLength context.expansionChannel ∧ context.framework.pdsSubtractionAt context.expansionScale ∧ context.framework.scaleComparableToMomentum context.expansionScale context.expansionMomentum ∧ context.framework.loopHasOrderMomentum context.expansionScale context.expansionMomentum ∧ context.framework.couplingScalingEstablished context.expansionChannel context.expansionScale context.expansionMomentum | .largeLengthPowerCountingCalculation => context.framework.LargeScatteringLengthPowerCountingCalculation context.expansionChannel context.expansionScale context.expansionMomentum | .mixedKSWExpansion => context.framework.KSWMixedExpansionAt context.expansionChannel context.expansionScale context.expansionMomentum | .kswAmplitudeExpansion => context.framework.amplitudeHasKSWExpansion context.expansionChannel context.expansionScale context.expansionMomentum | .resummedNonuniformPowerCounting => context.framework.powerCounting.HasResummedLeadingSector (context.framework.regimeOf context.expansionChannel context.expansionScale context.expansionMomentum) context.framework.leadingOrder ∧ ¬context.framework.powerCounting.UniformlyPerturbativeThrough (context.framework.regimeOf context.expansionChannel context.expansionScale context.expansionMomentum) context.framework.subleadingOrder | .pionScaleSetup => context.framework.pionScaleMomentum context.expansionMomentum ∧ context.framework.KSWMixedExpansionAt context.expansionChannel context.expansionScale context.expansionMomentum | .explicitPionSubleadingCalculation => context.framework.ExplicitPionSubleadingCalculation context.expansionChannel context.expansionScale context.expansionMomentum | .potentialPionAtSubleadingOrder => context.framework.potentialPionAtSubleadingOrder context.expansionChannel context.expansionScale context.expansionMomentum | .radiationPionsAbsentAtSubleadingOrder => context.framework.radiationPionsAbsentAtSubleadingOrder context.expansionChannel context.expansionMomentum | .logarithmicSubleadingScaleDependence => context.framework.logarithmicScaleDependenceAtSubleadingOrder context.expansionChannel context.expansionMomentum | .d2CountertermRequired => context.framework.quarkMassCountertermRequired context.expansionChannel context.expansionMomentum | .d2NotSubdominantToOnePionExchange => context.framework.quarkMassCountertermNotSubdominantToOnePionExchange context.expansionChannel context.expansionScale context.expansionMomentum | .pionInclusiveRGControlledCouplings => context.framework.pionInclusiveRGControlledCouplings | .subleadingAmplitudeComplete => context.framework.subleadingAmplitudeComplete context.expansionChannel context.expansionScale context.expansionMomentum | .weinbergCountingFailure => context.framework.WeinbergCountingFailureAt context.expansionChannel context.expansionScale context.expansionMomentum | .scaleCancellationCalculation => context.framework.ScaleCancellationCalculation context.expansionChannel context.expansionScale context.expansionMomentum | .fullPionAmplitudeScaleIndependent => context.framework.fullAmplitudeScaleIndependent context.expansionChannel context.expansionMomentum | .truncatedScaleIndependentThroughSubleading => context.framework.truncatedAmplitudeScaleIndependentThroughSubleading context.expansionChannel context.expansionMomentum | .residualScaleDependenceHigherOrder => context.framework.residualScaleDependenceIsHigherOrder context.expansionChannel context.expansionMomentum | .singletFitSetup => context.framework.fitUsesNijmegenPhaseShifts context.singletFit context.expansionChannel ∧ context.framework.fitOptimizedThroughTwoHundredMeV context.singletFit | .singletFitCalculation => context.framework.SingletFitCalculation context.singletFit context.expansionChannel context.expansionScale context.expansionMomentum | .fittedCouplingsHaveExpectedScaling => context.framework.leadingCouplingNearLargeLengthValue context.singletFit ∧ context.framework.derivativeCouplingHasExpectedSize context.singletFit | .c0D2CombinationControlsSubleadingAmplitude => context.framework.amplitudeUsesOnlyPionMassCombinationThrough context.singletFit context.framework.c0 context.framework.d2 context.expansionChannel context.expansionScale context.expansionMomentum context.framework.subleadingOrder | .c0D2CombinationInterpretation => context.framework.C0D2CombinationInterpretation context.singletFit context.expansionChannel context.expansionScale context.expansionMomentum | .individualC0D2FitValuesNotSeparatelyMeaningful => context.framework.individualFitValuesNotSeparatelyMeaningfulThrough context.singletFit context.framework.c0 context.framework.d2 context.expansionChannel context.expansionScale context.expansionMomentum context.framework.subleadingOrder | .goodSingletPhaseShiftAgreement => context.framework.phaseShiftAgreementGood context.singletFit context.expansionChannel | .fitValidityExpectation => context.framework.FitValidityInterpretation context.singletFit context.expansionChannel | .fitSuggestsExpansionValidity => context.framework.fitSuggestsExpansionValid context.singletFit context.expansionChannel | .largeSubleadingLeadingRatio => context.framework.subleadingLeadingRatioAtLeastHalfAboveHundredMeV context.singletFit context.expansionChannel | .highMomentumTruncationAssessment => context.framework.HighMomentumTruncationAssessment context.singletFit context.expansionChannel | .neglectedQuadraticTermsControlled => context.framework.neglectedQuadraticTermsControlledAboveHundredMeV context.singletFit context.expansionChannel | .coupledChannelSetup => context.framework.largeScatteringLength context.coupledChannel ∧ context.framework.coupledPowerCountingAnalogous context.coupledChannel | .coupledChannelCalculation => context.framework.CoupledChannelCalculation context.coupledFit context.coupledChannel | .coupledSMatrixFormula => context.framework.DisplayedCoupledSMatrixFormulaAt context.coupledChannel context.framework.leadingOrder | .leadingCoupledAmplitudeOnlySComponent => context.framework.leadingCoupledAmplitudeOnlySComponent context.coupledChannel | .leadingMixingAndDWavePhasesZero => context.framework.leadingMixingAngleZero context.coupledChannel ∧ context.framework.leadingDWavePhaseZero context.coupledChannel | .subleadingSPhaseCalculated => context.framework.subleadingSPhaseCalculated context.coupledChannel | .mixingAndDWaveOnlyLeadingOrder => context.framework.mixingAndDWaveOnlyLeadingOrder context.coupledChannel | .analyticSubleadingCoupledFormulaDeferred => context.framework.analyticSubleadingCoupledFormulaDeferred context.coupledChannel | .coupledSPhaseFitted => context.framework.coupledSPhaseFitted context.coupledFit context.coupledChannel | .mixingAndDWaveParameterFreeAtDeclaredOrder => context.framework.coupledSPhaseFitted context.coupledFit context.coupledChannel ∧ context.framework.mixingAndDWaveParameterFreeAtDeclaredOrder context.coupledFit context.coupledChannel theorem unitary_atom_retains_actual_scalar_s_matrix (context : SemanticContext Channel Scale Momentum Coupling Term Order Regime Fit) (unitarity : context.interpretAtom .unitaryAmplitude) : Complex.normSq (context.framework.pionlessPDSFormulaReadout.elasticSMatrixValueAt context.lowChannel context.lowScale context.lowMomentum) = 1 := unitarity.2.2.1 def interpretFormula (context : SemanticContext Channel Scale Momentum Coupling Term Order Regime Fit) (formula : Formula Atom) : Prop := formula.eval context.interpretAtom def interpretedClaims (context : SemanticContext Channel Scale Momentum Coupling Term Order Regime Fit) : List (ClaimId × Prop) := claims.map fun claim => (claim.id, context.interpretFormula claim.formula) theorem every_source_claim_has_semantics (context : SemanticContext Channel Scale Momentum Coupling Term Order Regime Fit) : context.interpretedClaims.length = claims.length := by simp [interpretedClaims] private theorem atomClaim (context : SemanticContext Channel Scale Momentum Coupling Term Order Regime Fit) (id : ClaimId) (atom : Atom) (lookup : argument.claimFormula? id = some (.atom atom)) (holds : context.interpretAtom atom) : argument.ClaimHolds context.interpretAtom id := PaperArgument.claimHolds_of_formula argument context.interpretAtom id (.atom atom) lookup holds private theorem certifyPremiseFreeStep (context : SemanticContext Channel Scale Momentum Coupling Term Order Regime Fit) (id : StepId) (conclusion : ClaimId) (lookup : argument.stepRule? id = some ([], conclusion)) (holds : argument.ClaimHolds context.interpretAtom conclusion) : argument.StepSound context.interpretAtom id := PaperArgument.stepSound_of_conclusion_lookup argument context.interpretAtom id conclusion (by decide) lookup holds private theorem atomOfPremise (context : SemanticContext Channel Scale Momentum Coupling Term Order Regime Fit) (premiseIds : List ClaimId) (premises : argument.ClaimsHold context.interpretAtom premiseIds) (id : ClaimId) (atom : Atom) (membership : id ∈ premiseIds) (formulaLookup : argument.claimFormula? id = some (.atom atom)) : context.interpretAtom atom := PaperArgument.formula_eval_of_claimHolds argument context.interpretAtom id (.atom atom) formulaLookup (premises id membership) private theorem certifyPremiseAwareStep (context : SemanticContext Channel Scale Momentum Coupling Term Order Regime Fit) (id : StepId) (premises : List ClaimId) (conclusion : ClaimId) (lookup : argument.stepRule? id = some (premises, conclusion)) (rule : argument.ClaimsHold context.interpretAtom premises -> argument.ClaimHolds context.interpretAtom conclusion) : argument.StepSound context.interpretAtom id := PaperArgument.stepSound_of_rule_lookup argument context.interpretAtom id premises conclusion (by decide) lookup rule private theorem certifyRoute (context : SemanticContext Channel Scale Momentum Coupling Term Order Regime Fit) (id : RouteId) (route : ArgumentRoute RouteId RouteKind StepId ClaimId) (lookup : routedArgument.route? id = some route) (dependencies : routedArgument.RoutesSemanticallyCertified context.interpretAtom (routedArgument.routeDependencyIds route)) (stepsSound : argument.StepsSound context.interpretAtom route.steps) (derivable : RoutedArgument.stepsDerivableFrom argument (routedArgument.routeDependencyClaims route) route.steps = true) (noReductio : RoutedArgument.stepsContainNoReductio argument route.steps = true) (outputs : route.outputs.all (RoutedArgument.claimsAfterSteps argument (routedArgument.routeDependencyClaims route) route.steps).contains = true) : routedArgument.RouteSemanticallyCertified context.interpretAtom id := RoutedArgument.routeSemanticallyCertified_of_certified_dependencies routedArgument context.interpretAtom id route lookup (by decide) dependencies stepsSound derivable noReductio outputs theorem pionless_pds_route_is_semantically_realized (context : SemanticContext Channel Scale Momentum Coupling Term Order Regime Fit) (pionless : context.framework.pionlessMomentum context.lowMomentum) (largeLength : context.framework.largeScatteringLength context.lowChannel) (pds : context.framework.pdsSubtractionAt context.lowScale) (bubble : (context.framework.pionlessLeadingContactOrderAt context.lowChannel context.lowScale context.lowMomentum = -1 ∧ context.framework.pionlessBubbleLoopOrderAt context.lowScale context.lowMomentum = 1)) (loopCalculation : context.framework.PDSLoopCalculation context.lowChannel context.lowScale context.lowMomentum) (resummationCalculation : context.framework.BubbleResummationCalculation context.lowChannel context.lowScale context.lowMomentum) (unitarityCalculation : context.framework.PionlessUnitarityCalculation context.lowChannel context.lowScale context.lowMomentum) (rangeMatching : context.framework.effectiveRangeDataMatched context.lowChannel) (scaleRequirement : context.framework.physicalAmplitudeRequiredScaleIndependent context.lowChannel context.lowMomentum) (rgCalculation : context.framework.PionlessRGCalculation context.lowChannel context.lowScale context.lowMomentum) : routedArgument.RouteSemanticallyCertified context.interpretAtom .pionlessPDS := by have setupClaim := atomClaim context .pdsSetup .pionlessPDSSetup (by rfl) ⟨pionless, largeLength, pds, bubble⟩ have loopCalculationClaim := atomClaim context .loopCalculation .pdsLoopCalculation (by rfl) loopCalculation have resummationCalculationClaim := atomClaim context .resummationCalculation .bubbleResummationCalculation (by rfl) resummationCalculation have unitarityCalculationClaim := atomClaim context .unitarityCalculation .pionlessUnitarityCalculation (by rfl) unitarityCalculation have rangeClaim := atomClaim context .rangeMatching .effectiveRangeMatching (by rfl) rangeMatching have scaleClaim := atomClaim context .scaleRequirement .physicalScaleIndependenceRequirement (by rfl) scaleRequirement have rgCalculationClaim := atomClaim context .rgCalculation .pionlessRGCalculation (by rfl) rgCalculation have stepsSound : argument.StepsSound context.interpretAtom pionlessPDSRoute.steps := by change argument.StepsSound context.interpretAtom [.statePDSSetup, .stateLoopCalculation, .stateResummationCalculation, .stateUnitarityCalculation, .deriveLoopIntegral, .retainPDSLoopFormula, .derivePDSAmplitude, .retainPDSAmplitudeFormula, .deriveUnitarity, .stateEffectiveRangeMatching, .imposePhysicalScaleIndependence, .stateRGCalculation, .deriveBetaFunctions, .deriveC0C2RGControl, .deriveFullScaleIndependence] intro stepId stepMem simp at stepMem rcases stepMem with rfl | rfl | rfl | rfl | rfl | rfl | rfl | rfl | rfl | rfl | rfl | rfl | rfl | rfl | rfl · exact certifyPremiseFreeStep context .statePDSSetup .pdsSetup (by decide) setupClaim · exact certifyPremiseFreeStep context .stateLoopCalculation .loopCalculation (by decide) loopCalculationClaim · exact certifyPremiseFreeStep context .stateResummationCalculation .resummationCalculation (by decide) resummationCalculationClaim · exact certifyPremiseFreeStep context .stateUnitarityCalculation .unitarityCalculation (by decide) unitarityCalculationClaim · apply certifyPremiseAwareStep context .deriveLoopIntegral [.pdsSetup, .loopCalculation] .loopIntegral (by decide) intro premises have setupFromPremises := atomOfPremise context [.pdsSetup, .loopCalculation] premises .pdsSetup .pionlessPDSSetup (by simp) (by rfl) have calculationFromPremises := atomOfPremise context [.pdsSetup, .loopCalculation] premises .loopCalculation .pdsLoopCalculation (by simp) (by rfl) exact atomClaim context .loopIntegral .pdsLoopIntegral (by rfl) (context.framework.pds_subtraction_yields_loop_integral context.lowChannel context.lowScale context.lowMomentum setupFromPremises.1 setupFromPremises.2.2.1 calculationFromPremises) · apply certifyPremiseAwareStep context .retainPDSLoopFormula [.pdsSetup, .loopCalculation] .loopFormula (by decide) intro premises have setupFromPremises := atomOfPremise context [.pdsSetup, .loopCalculation] premises .pdsSetup .pionlessPDSSetup (by simp) (by rfl) have calculationFromPremises := atomOfPremise context [.pdsSetup, .loopCalculation] premises .loopCalculation .pdsLoopCalculation (by simp) (by rfl) exact atomClaim context .loopFormula .pdsLoopFormula (by rfl) (context.framework |>.pds_loop_calculation_retains_equation_five_formula context.lowChannel context.lowScale context.lowMomentum setupFromPremises.1 setupFromPremises.2.2.1 calculationFromPremises) · apply certifyPremiseAwareStep context .derivePDSAmplitude [.pdsSetup, .loopIntegral, .resummationCalculation] .amplitude (by decide) intro premises have setupFromPremises := atomOfPremise context [.pdsSetup, .loopIntegral, .resummationCalculation] premises .pdsSetup .pionlessPDSSetup (by simp) (by rfl) have loopFromPremises := atomOfPremise context [.pdsSetup, .loopIntegral, .resummationCalculation] premises .loopIntegral .pdsLoopIntegral (by simp) (by rfl) have calculationFromPremises := atomOfPremise context [.pdsSetup, .loopIntegral, .resummationCalculation] premises .resummationCalculation .bubbleResummationCalculation (by simp) (by rfl) exact atomClaim context .amplitude .pdsAmplitude (by rfl) (context.framework.bubble_chain_and_loop_yield_full_amplitude context.lowChannel context.lowScale context.lowMomentum setupFromPremises.2.1 setupFromPremises.2.2.2 loopFromPremises calculationFromPremises) · apply certifyPremiseAwareStep context .retainPDSAmplitudeFormula [.pdsSetup, .loopIntegral, .resummationCalculation] .amplitudeFormula (by decide) intro premises have setupFromPremises := atomOfPremise context [.pdsSetup, .loopIntegral, .resummationCalculation] premises .pdsSetup .pionlessPDSSetup (by simp) (by rfl) have loopFromPremises := atomOfPremise context [.pdsSetup, .loopIntegral, .resummationCalculation] premises .loopIntegral .pdsLoopIntegral (by simp) (by rfl) have calculationFromPremises := atomOfPremise context [.pdsSetup, .loopIntegral, .resummationCalculation] premises .resummationCalculation .bubbleResummationCalculation (by simp) (by rfl) exact atomClaim context .amplitudeFormula .pdsAmplitudeFormula (by rfl) (context.framework |>.bubble_resummation_retains_equation_six_formula context.lowChannel context.lowScale context.lowMomentum setupFromPremises.2.1 setupFromPremises.2.2.2 loopFromPremises calculationFromPremises) · apply certifyPremiseAwareStep context .deriveUnitarity [.amplitude, .amplitudeFormula, .unitarityCalculation] .unitarity (by decide) intro premises have _amplitudeFromPremises := atomOfPremise context [.amplitude, .amplitudeFormula, .unitarityCalculation] premises .amplitude .pdsAmplitude (by simp) (by rfl) have formulaFromPremises := atomOfPremise context [.amplitude, .amplitudeFormula, .unitarityCalculation] premises .amplitudeFormula .pdsAmplitudeFormula (by simp) (by rfl) have calculationFromPremises := atomOfPremise context [.amplitude, .amplitudeFormula, .unitarityCalculation] premises .unitarityCalculation .pionlessUnitarityCalculation (by simp) (by rfl) exact atomClaim context .unitarity .unitaryAmplitude (by rfl) (context.framework.pds_amplitude_has_unitary_s_wave_form context.lowChannel context.lowScale context.lowMomentum formulaFromPremises calculationFromPremises) · exact certifyPremiseFreeStep context .stateEffectiveRangeMatching .rangeMatching (by decide) rangeClaim · exact certifyPremiseFreeStep context .imposePhysicalScaleIndependence .scaleRequirement (by decide) scaleClaim · exact certifyPremiseFreeStep context .stateRGCalculation .rgCalculation (by decide) rgCalculationClaim · apply certifyPremiseAwareStep context .deriveBetaFunctions [.amplitude, .rangeMatching, .scaleRequirement, .rgCalculation] .betaFunctions (by decide) intro premises have amplitudeFromPremises := atomOfPremise context [.amplitude, .rangeMatching, .scaleRequirement, .rgCalculation] premises .amplitude .pdsAmplitude (by simp) (by rfl) have matchingFromPremises := atomOfPremise context [.amplitude, .rangeMatching, .scaleRequirement, .rgCalculation] premises .rangeMatching .effectiveRangeMatching (by simp) (by rfl) have scaleFromPremises := atomOfPremise context [.amplitude, .rangeMatching, .scaleRequirement, .rgCalculation] premises .scaleRequirement .physicalScaleIndependenceRequirement (by simp) (by rfl) have calculationFromPremises := atomOfPremise context [.amplitude, .rangeMatching, .scaleRequirement, .rgCalculation] premises .rgCalculation .pionlessRGCalculation (by simp) (by rfl) have result := context.framework |>.scale_independence_yields_running_couplings_and_rg_equations context.lowChannel context.lowScale context.lowMomentum amplitudeFromPremises matchingFromPremises scaleFromPremises calculationFromPremises exact atomClaim context .betaFunctions .exactC0C2BetaFunctions (by rfl) result.1 · apply certifyPremiseAwareStep context .deriveC0C2RGControl [.amplitude, .rangeMatching, .scaleRequirement, .rgCalculation] .c0C2RGControl (by decide) intro premises have amplitudeFromPremises := atomOfPremise context [.amplitude, .rangeMatching, .scaleRequirement, .rgCalculation] premises .amplitude .pdsAmplitude (by simp) (by rfl) have matchingFromPremises := atomOfPremise context [.amplitude, .rangeMatching, .scaleRequirement, .rgCalculation] premises .rangeMatching .effectiveRangeMatching (by simp) (by rfl) have scaleFromPremises := atomOfPremise context [.amplitude, .rangeMatching, .scaleRequirement, .rgCalculation] premises .scaleRequirement .physicalScaleIndependenceRequirement (by simp) (by rfl) have calculationFromPremises := atomOfPremise context [.amplitude, .rangeMatching, .scaleRequirement, .rgCalculation] premises .rgCalculation .pionlessRGCalculation (by simp) (by rfl) have result := context.framework |>.scale_independence_yields_running_couplings_and_rg_equations context.lowChannel context.lowScale context.lowMomentum amplitudeFromPremises matchingFromPremises scaleFromPremises calculationFromPremises exact atomClaim context .c0C2RGControl .c0C2PionlessRGControl (by rfl) ⟨result.1, result.2.1⟩ · apply certifyPremiseAwareStep context .deriveFullScaleIndependence [.amplitude, .rangeMatching, .scaleRequirement, .rgCalculation] .fullScaleIndependence (by decide) intro premises have amplitudeFromPremises := atomOfPremise context [.amplitude, .rangeMatching, .scaleRequirement, .rgCalculation] premises .amplitude .pdsAmplitude (by simp) (by rfl) have matchingFromPremises := atomOfPremise context [.amplitude, .rangeMatching, .scaleRequirement, .rgCalculation] premises .rangeMatching .effectiveRangeMatching (by simp) (by rfl) have scaleFromPremises := atomOfPremise context [.amplitude, .rangeMatching, .scaleRequirement, .rgCalculation] premises .scaleRequirement .physicalScaleIndependenceRequirement (by simp) (by rfl) have calculationFromPremises := atomOfPremise context [.amplitude, .rangeMatching, .scaleRequirement, .rgCalculation] premises .rgCalculation .pionlessRGCalculation (by simp) (by rfl) have result := context.framework |>.scale_independence_yields_running_couplings_and_rg_equations context.lowChannel context.lowScale context.lowMomentum amplitudeFromPremises matchingFromPremises scaleFromPremises calculationFromPremises exact atomClaim context .fullScaleIndependence .fullAmplitudeScaleIndependent (by rfl) result.2.2 have dependencies : routedArgument.RoutesSemanticallyCertified context.interpretAtom (routedArgument.routeDependencyIds pionlessPDSRoute) := by change routedArgument.RoutesSemanticallyCertified context.interpretAtom [] intro routeId routeMem simp at routeMem exact certifyRoute context .pionlessPDS pionlessPDSRoute (by rfl) dependencies stepsSound (by decide) (by decide) (by decide) /-- The pionless PDS inputs expose the literal printed-equation-(4) loop and equation-(5) amplitude claims independently of the named loop/amplitude outputs. The public theorem name retains the historical numbering for compatibility. -/ theorem pionless_pds_route_exposes_equations_five_and_six (context : SemanticContext Channel Scale Momentum Coupling Term Order Regime Fit) (pionless : context.framework.pionlessMomentum context.lowMomentum) (largeLength : context.framework.largeScatteringLength context.lowChannel) (pds : context.framework.pdsSubtractionAt context.lowScale) (bubble : (context.framework.pionlessLeadingContactOrderAt context.lowChannel context.lowScale context.lowMomentum = -1 ∧ context.framework.pionlessBubbleLoopOrderAt context.lowScale context.lowMomentum = 1)) (loopCalculation : context.framework.PDSLoopCalculation context.lowChannel context.lowScale context.lowMomentum) (resummationCalculation : context.framework.BubbleResummationCalculation context.lowChannel context.lowScale context.lowMomentum) : context.interpretAtom .pdsLoopFormula /\ context.interpretAtom .pdsAmplitudeFormula := by have loopFormula := context.framework |>.pds_loop_calculation_retains_equation_five_formula context.lowChannel context.lowScale context.lowMomentum pionless pds loopCalculation have loop := context.framework.pds_subtraction_yields_loop_integral context.lowChannel context.lowScale context.lowMomentum pionless pds loopCalculation have amplitudeFormula := context.framework |>.bubble_resummation_retains_equation_six_formula context.lowChannel context.lowScale context.lowMomentum largeLength bubble loop resummationCalculation exact ⟨loopFormula, amplitudeFormula⟩ theorem minimal_subtraction_scope_route_is_semantically_realized (context : SemanticContext Channel Scale Momentum Coupling Term Order Regime Fit) (natural : context.framework.naturalScatteringLength context.naturalMSChannel) (large : context.framework.largeScatteringLength context.largeLengthMSChannel) (minimalSubtraction : context.framework.minimalSubtractionAt context.msScale) (pionless : context.framework.pionlessMomentum context.msMomentum) (smallComparedWithRange : context.framework.momentumSmallComparedWithShortRangeScale context.naturalMSChannel context.msMomentum) (naturalCalculation : context.framework.NaturalMSPowerCountingCalculation context.naturalMSChannel context.msScale context.msMomentum) (largeLengthCalculation : context.framework.LargeLengthMSRestrictionCalculation context.largeLengthMSChannel context.msScale) : routedArgument.RouteSemanticallyCertified context.interpretAtom .minimalSubtractionScope := by have naturalSetupClaim := atomClaim context .naturalMSRegime .naturalMSSetup (by rfl) ⟨natural, minimalSubtraction, smallComparedWithRange⟩ have largeSetupClaim := atomClaim context .largeLengthMSRegime .largeLengthMSSetup (by rfl) ⟨large, minimalSubtraction, pionless⟩ have naturalCalculationClaim := atomClaim context .naturalMSCalculation .naturalMSPowerCountingCalculation (by rfl) naturalCalculation have largeCalculationClaim := atomClaim context .largeLengthMSCalculation .largeLengthMSRestrictionCalculation (by rfl) largeLengthCalculation have stepsSound : argument.StepsSound context.interpretAtom minimalSubtractionScopeRoute.steps := by change argument.StepsSound context.interpretAtom [.stateNaturalMSRegime, .stateLargeLengthMSRegime, .stateNaturalMSCalculation, .stateLargeLengthMSCalculation, .deriveNaturalMSValidity, .deriveLargeLengthMSWindow, .deriveLargeLengthMSRestriction] intro stepId stepMem simp at stepMem rcases stepMem with rfl | rfl | rfl | rfl | rfl | rfl | rfl · exact certifyPremiseFreeStep context .stateNaturalMSRegime .naturalMSRegime (by decide) naturalSetupClaim · exact certifyPremiseFreeStep context .stateLargeLengthMSRegime .largeLengthMSRegime (by decide) largeSetupClaim · exact certifyPremiseFreeStep context .stateNaturalMSCalculation .naturalMSCalculation (by decide) naturalCalculationClaim · exact certifyPremiseFreeStep context .stateLargeLengthMSCalculation .largeLengthMSCalculation (by decide) largeCalculationClaim · apply certifyPremiseAwareStep context .deriveNaturalMSValidity [.naturalMSRegime, .naturalMSCalculation] .naturalMSValidity (by decide) intro premises have setupFromPremises := atomOfPremise context [.naturalMSRegime, .naturalMSCalculation] premises .naturalMSRegime .naturalMSSetup (by simp) (by rfl) have calculationFromPremises := atomOfPremise context [.naturalMSRegime, .naturalMSCalculation] premises .naturalMSCalculation .naturalMSPowerCountingCalculation (by simp) (by rfl) exact atomClaim context .naturalMSValidity .naturalMSCountingValid (by rfl) (calculationFromPremises setupFromPremises.1 setupFromPremises.2.1 setupFromPremises.2.2) · apply certifyPremiseAwareStep context .deriveLargeLengthMSWindow [.largeLengthMSRegime, .largeLengthMSCalculation] .largeLengthMSWindow (by decide) intro premises have setupFromPremises := atomOfPremise context [.largeLengthMSRegime, .largeLengthMSCalculation] premises .largeLengthMSRegime .largeLengthMSSetup (by simp) (by rfl) have calculationFromPremises := atomOfPremise context [.largeLengthMSRegime, .largeLengthMSCalculation] premises .largeLengthMSCalculation .largeLengthMSRestrictionCalculation (by simp) (by rfl) exact atomClaim context .largeLengthMSWindow .largeLengthMSValidityRequiresInverseLengthWindow (by rfl) ((calculationFromPremises setupFromPremises.1 setupFromPremises.2.1).1 context.msMomentum setupFromPremises.2.2) · apply certifyPremiseAwareStep context .deriveLargeLengthMSRestriction [.largeLengthMSRegime, .largeLengthMSCalculation] .largeLengthMSRestriction (by decide) intro premises have setupFromPremises := atomOfPremise context [.largeLengthMSRegime, .largeLengthMSCalculation] premises .largeLengthMSRegime .largeLengthMSSetup (by simp) (by rfl) have calculationFromPremises := atomOfPremise context [.largeLengthMSRegime, .largeLengthMSCalculation] premises .largeLengthMSCalculation .largeLengthMSRestrictionCalculation (by simp) (by rfl) obtain ⟨necessary, excluded, inDomain, outside⟩ := calculationFromPremises setupFromPremises.1 setupFromPremises.2.1 exact atomClaim context .largeLengthMSRestriction .largeLengthMSRangeRestricted (by rfl) ⟨excluded, inDomain, fun valid => outside (necessary excluded inDomain valid)⟩ have dependencies : routedArgument.RoutesSemanticallyCertified context.interpretAtom (routedArgument.routeDependencyIds minimalSubtractionScopeRoute) := by change routedArgument.RoutesSemanticallyCertified context.interpretAtom [] intro routeId routeMem simp at routeMem exact certifyRoute context .minimalSubtractionScope minimalSubtractionScopeRoute (by rfl) dependencies stepsSound (by decide) (by decide) (by decide) theorem large_length_power_counting_route_is_semantically_realized (context : SemanticContext Channel Scale Momentum Coupling Term Order Regime Fit) (largeLength : context.framework.largeScatteringLength context.expansionChannel) (pds : context.framework.pdsSubtractionAt context.expansionScale) (comparable : context.framework.scaleComparableToMomentum context.expansionScale context.expansionMomentum) (loopScaling : context.framework.loopHasOrderMomentum context.expansionScale context.expansionMomentum) (couplingScaling : context.framework.couplingScalingEstablished context.expansionChannel context.expansionScale context.expansionMomentum) (calculation : context.framework.LargeScatteringLengthPowerCountingCalculation context.expansionChannel context.expansionScale context.expansionMomentum) : routedArgument.RouteSemanticallyCertified context.interpretAtom .largeLengthPowerCounting := by have setupClaim := atomClaim context .scalingSetup .largeLengthScalingSetup (by rfl) ⟨largeLength, pds, comparable, loopScaling, couplingScaling⟩ have calculationClaim := atomClaim context .scalingCalculation .largeLengthPowerCountingCalculation (by rfl) calculation have stepsSound : argument.StepsSound context.interpretAtom largeLengthPowerCountingRoute.steps := by change argument.StepsSound context.interpretAtom [.stateScalingSetup, .stateScalingCalculation, .deriveMixedExpansion, .deriveAmplitudeExpansion, .realizeSharedPowerCounting] intro stepId stepMem simp at stepMem rcases stepMem with rfl | rfl | rfl | rfl | rfl · exact certifyPremiseFreeStep context .stateScalingSetup .scalingSetup (by decide) setupClaim · exact certifyPremiseFreeStep context .stateScalingCalculation .scalingCalculation (by decide) calculationClaim · apply certifyPremiseAwareStep context .deriveMixedExpansion [.scalingSetup, .scalingCalculation] .mixedExpansion (by decide) intro premises have setupFromPremises := atomOfPremise context [.scalingSetup, .scalingCalculation] premises .scalingSetup .largeLengthScalingSetup (by simp) (by rfl) have calculationFromPremises := atomOfPremise context [.scalingSetup, .scalingCalculation] premises .scalingCalculation .largeLengthPowerCountingCalculation (by simp) (by rfl) exact atomClaim context .mixedExpansion .mixedKSWExpansion (by rfl) (context.framework.large_scattering_length_requires_resummed_leading_contact context.expansionChannel context.expansionScale context.expansionMomentum setupFromPremises.1 setupFromPremises.2.1 setupFromPremises.2.2.1 setupFromPremises.2.2.2.1 setupFromPremises.2.2.2.2 calculationFromPremises).1 · apply certifyPremiseAwareStep context .deriveAmplitudeExpansion [.scalingSetup, .scalingCalculation] .amplitudeExpansion (by decide) intro premises have setupFromPremises := atomOfPremise context [.scalingSetup, .scalingCalculation] premises .scalingSetup .largeLengthScalingSetup (by simp) (by rfl) have calculationFromPremises := atomOfPremise context [.scalingSetup, .scalingCalculation] premises .scalingCalculation .largeLengthPowerCountingCalculation (by simp) (by rfl) exact atomClaim context .amplitudeExpansion .kswAmplitudeExpansion (by rfl) (context.framework.large_scattering_length_requires_resummed_leading_contact context.expansionChannel context.expansionScale context.expansionMomentum setupFromPremises.1 setupFromPremises.2.1 setupFromPremises.2.2.1 setupFromPremises.2.2.2.1 setupFromPremises.2.2.2.2 calculationFromPremises).2 · apply certifyPremiseAwareStep context .realizeSharedPowerCounting [.mixedExpansion] .sharedPowerCounting (by decide) intro premises have mixedFromPremises := atomOfPremise context [.mixedExpansion] premises .mixedExpansion .mixedKSWExpansion (by simp) (by rfl) exact atomClaim context .sharedPowerCounting .resummedNonuniformPowerCounting (by rfl) (context.framework.ksw_mixed_expansion_realizes_shared_power_counting context.expansionChannel context.expansionScale context.expansionMomentum mixedFromPremises) have dependencies : routedArgument.RoutesSemanticallyCertified context.interpretAtom (routedArgument.routeDependencyIds largeLengthPowerCountingRoute) := by change routedArgument.RoutesSemanticallyCertified context.interpretAtom [] intro routeId routeMem simp at routeMem exact certifyRoute context .largeLengthPowerCounting largeLengthPowerCountingRoute (by rfl) dependencies stepsSound (by decide) (by decide) (by decide) theorem explicit_pions_route_is_semantically_realized (context : SemanticContext Channel Scale Momentum Coupling Term Order Regime Fit) (dependencies : routedArgument.RoutesSemanticallyCertified context.interpretAtom (routedArgument.routeDependencyIds explicitPionsRoute)) (pionScale : context.framework.pionScaleMomentum context.expansionMomentum) (calculation : context.framework.ExplicitPionSubleadingCalculation context.expansionChannel context.expansionScale context.expansionMomentum) : routedArgument.RouteSemanticallyCertified context.interpretAtom .explicitPions := by have calculationClaim := atomClaim context .pionCalculation .explicitPionSubleadingCalculation (by rfl) calculation have stepsSound : argument.StepsSound context.interpretAtom explicitPionsRoute.steps := by change argument.StepsSound context.interpretAtom [.statePionSetup, .statePionCalculation, .derivePotentialPionOrder, .deriveRadiationPionAbsence, .deriveLogarithmicDependence, .requireD2Counterterm, .deriveD2Unsuppressed, .derivePionInclusiveRGControl, .deriveSubleadingCompleteness, .excludeWeinbergCounting] intro stepId stepMem simp at stepMem rcases stepMem with rfl | rfl | rfl | rfl | rfl | rfl | rfl | rfl | rfl | rfl · apply certifyPremiseAwareStep context .statePionSetup [.mixedExpansion] .pionSetup (by decide) intro premises have mixedFromPremises := atomOfPremise context [.mixedExpansion] premises .mixedExpansion .mixedKSWExpansion (by simp) (by rfl) exact atomClaim context .pionSetup .pionScaleSetup (by rfl) ⟨pionScale, mixedFromPremises⟩ · exact certifyPremiseFreeStep context .statePionCalculation .pionCalculation (by decide) calculationClaim · apply certifyPremiseAwareStep context .derivePotentialPionOrder [.pionSetup, .pionCalculation] .potentialPion (by decide) intro premises have setupFromPremises := atomOfPremise context [.pionSetup, .pionCalculation] premises .pionSetup .pionScaleSetup (by simp) (by rfl) have calculationFromPremises := atomOfPremise context [.pionSetup, .pionCalculation] premises .pionCalculation .explicitPionSubleadingCalculation (by simp) (by rfl) exact atomClaim context .potentialPion .potentialPionAtSubleadingOrder (by rfl) (calculationFromPremises setupFromPremises.1 setupFromPremises.2).1 · apply certifyPremiseAwareStep context .deriveRadiationPionAbsence [.pionSetup, .pionCalculation] .radiationPionAbsence (by decide) intro premises have setupFromPremises := atomOfPremise context [.pionSetup, .pionCalculation] premises .pionSetup .pionScaleSetup (by simp) (by rfl) have calculationFromPremises := atomOfPremise context [.pionSetup, .pionCalculation] premises .pionCalculation .explicitPionSubleadingCalculation (by simp) (by rfl) exact atomClaim context .radiationPionAbsence .radiationPionsAbsentAtSubleadingOrder (by rfl) (calculationFromPremises setupFromPremises.1 setupFromPremises.2).2.1 · apply certifyPremiseAwareStep context .deriveLogarithmicDependence [.pionSetup, .pionCalculation] .logarithmicScaleDependence (by decide) intro premises have setupFromPremises := atomOfPremise context [.pionSetup, .pionCalculation] premises .pionSetup .pionScaleSetup (by simp) (by rfl) have calculationFromPremises := atomOfPremise context [.pionSetup, .pionCalculation] premises .pionCalculation .explicitPionSubleadingCalculation (by simp) (by rfl) exact atomClaim context .logarithmicScaleDependence .logarithmicSubleadingScaleDependence (by rfl) (calculationFromPremises setupFromPremises.1 setupFromPremises.2).2.2.1 · apply certifyPremiseAwareStep context .requireD2Counterterm [.pionSetup, .pionCalculation] .d2Required (by decide) intro premises have setupFromPremises := atomOfPremise context [.pionSetup, .pionCalculation] premises .pionSetup .pionScaleSetup (by simp) (by rfl) have calculationFromPremises := atomOfPremise context [.pionSetup, .pionCalculation] premises .pionCalculation .explicitPionSubleadingCalculation (by simp) (by rfl) have result := calculationFromPremises setupFromPremises.1 setupFromPremises.2 have coefficients := context.framework.pion_coefficient_family_specializes_at_momentum context.expansionChannel context.expansionMomentum result.2.2.2.1 setupFromPremises.1 exact atomClaim context .d2Required .d2CountertermRequired (by rfl) (context.framework.pion_coefficient_calculation_requires_the_mass_counterterm context.expansionChannel context.expansionMomentum coefficients) · apply certifyPremiseAwareStep context .deriveD2Unsuppressed [.pionSetup, .pionCalculation] .d2Unsuppressed (by decide) intro premises have setupFromPremises := atomOfPremise context [.pionSetup, .pionCalculation] premises .pionSetup .pionScaleSetup (by simp) (by rfl) have calculationFromPremises := atomOfPremise context [.pionSetup, .pionCalculation] premises .pionCalculation .explicitPionSubleadingCalculation (by simp) (by rfl) have result := calculationFromPremises setupFromPremises.1 setupFromPremises.2 have coefficients := context.framework.pion_coefficient_family_specializes_at_momentum context.expansionChannel context.expansionMomentum result.2.2.2.1 setupFromPremises.1 exact atomClaim context .d2Unsuppressed .d2NotSubdominantToOnePionExchange (by rfl) ⟨result.1, result.2.2.2.2.1, context.framework.pion_coefficient_calculation_exposes_a_nonzero_mass_insertion context.expansionChannel context.expansionMomentum coefficients⟩ · apply certifyPremiseAwareStep context .derivePionInclusiveRGControl [.pionSetup, .pionCalculation] .pionInclusiveRGControl (by decide) intro premises have setupFromPremises := atomOfPremise context [.pionSetup, .pionCalculation] premises .pionSetup .pionScaleSetup (by simp) (by rfl) have calculationFromPremises := atomOfPremise context [.pionSetup, .pionCalculation] premises .pionCalculation .explicitPionSubleadingCalculation (by simp) (by rfl) exact atomClaim context .pionInclusiveRGControl .pionInclusiveRGControlledCouplings (by rfl) (calculationFromPremises setupFromPremises.1 setupFromPremises.2).2.2.2.2.2.1 · apply certifyPremiseAwareStep context .deriveSubleadingCompleteness [.pionSetup, .pionCalculation] .subleadingComplete (by decide) intro premises have setupFromPremises := atomOfPremise context [.pionSetup, .pionCalculation] premises .pionSetup .pionScaleSetup (by simp) (by rfl) have calculationFromPremises := atomOfPremise context [.pionSetup, .pionCalculation] premises .pionCalculation .explicitPionSubleadingCalculation (by simp) (by rfl) exact atomClaim context .subleadingComplete .subleadingAmplitudeComplete (by rfl) (calculationFromPremises setupFromPremises.1 setupFromPremises.2).2.2.2.2.2.2.1 · apply certifyPremiseAwareStep context .excludeWeinbergCounting [.pionSetup, .d2Required, .d2Unsuppressed] .weinbergFailure (by decide) intro premises have setupFromPremises := atomOfPremise context [.pionSetup, .d2Required, .d2Unsuppressed] premises .pionSetup .pionScaleSetup (by simp) (by rfl) have requiredFromPremises := atomOfPremise context [.pionSetup, .d2Required, .d2Unsuppressed] premises .d2Required .d2CountertermRequired (by simp) (by rfl) have unsuppressedFromPremises := atomOfPremise context [.pionSetup, .d2Required, .d2Unsuppressed] premises .d2Unsuppressed .d2NotSubdominantToOnePionExchange (by simp) (by rfl) exact atomClaim context .weinbergFailure .weinbergCountingFailure (by rfl) ⟨requiredFromPremises, unsuppressedFromPremises, by intro consistent obtain ⟨evaluationScale, changed⟩ := unsuppressedFromPremises.2.2 exact changed (consistent context.expansionScale setupFromPremises.2 unsuppressedFromPremises.1 evaluationScale 1 (by omega))⟩ exact certifyRoute context .explicitPions explicitPionsRoute (by rfl) dependencies stepsSound (by decide) (by decide) (by decide) theorem scale_cancellation_route_is_semantically_realized (context : SemanticContext Channel Scale Momentum Coupling Term Order Regime Fit) (dependencies : routedArgument.RoutesSemanticallyCertified context.interpretAtom (routedArgument.routeDependencyIds scaleCancellationRoute)) (calculation : context.framework.ScaleCancellationCalculation context.expansionChannel context.expansionScale context.expansionMomentum) : routedArgument.RouteSemanticallyCertified context.interpretAtom .scaleCancellation := by have calculationClaim := atomClaim context .scaleCalculation .scaleCancellationCalculation (by rfl) calculation have stepsSound : argument.StepsSound context.interpretAtom scaleCancellationRoute.steps := by change argument.StepsSound context.interpretAtom [.stateScaleCancellation, .deriveFullPionScaleIndependence, .deriveTruncatedScaleIndependence, .deriveHigherOrderResidual] intro stepId stepMem simp at stepMem rcases stepMem with rfl | rfl | rfl | rfl · exact certifyPremiseFreeStep context .stateScaleCancellation .scaleCalculation (by decide) calculationClaim · apply certifyPremiseAwareStep context .deriveFullPionScaleIndependence [.pionInclusiveRGControl, .subleadingComplete, .scaleCalculation] .fullPionScaleIndependence (by decide) intro premises have rgFromPremises := atomOfPremise context [.pionInclusiveRGControl, .subleadingComplete, .scaleCalculation] premises .pionInclusiveRGControl .pionInclusiveRGControlledCouplings (by simp) (by rfl) have completeFromPremises := atomOfPremise context [.pionInclusiveRGControl, .subleadingComplete, .scaleCalculation] premises .subleadingComplete .subleadingAmplitudeComplete (by simp) (by rfl) have calculationFromPremises := atomOfPremise context [.pionInclusiveRGControl, .subleadingComplete, .scaleCalculation] premises .scaleCalculation .scaleCancellationCalculation (by simp) (by rfl) exact atomClaim context .fullPionScaleIndependence .fullPionAmplitudeScaleIndependent (by rfl) (calculationFromPremises rgFromPremises completeFromPremises) · apply certifyPremiseAwareStep context .deriveTruncatedScaleIndependence [.pionInclusiveRGControl, .subleadingComplete, .scaleCalculation] .truncatedScaleIndependence (by decide) intro premises have rgFromPremises := atomOfPremise context [.pionInclusiveRGControl, .subleadingComplete, .scaleCalculation] premises .pionInclusiveRGControl .pionInclusiveRGControlledCouplings (by simp) (by rfl) have completeFromPremises := atomOfPremise context [.pionInclusiveRGControl, .subleadingComplete, .scaleCalculation] premises .subleadingComplete .subleadingAmplitudeComplete (by simp) (by rfl) have calculationFromPremises := atomOfPremise context [.pionInclusiveRGControl, .subleadingComplete, .scaleCalculation] premises .scaleCalculation .scaleCancellationCalculation (by simp) (by rfl) exact atomClaim context .truncatedScaleIndependence .truncatedScaleIndependentThroughSubleading (by rfl) (context.framework.pion_inclusive_rg_control_makes_truncated_amplitude_scale_independent_through_computed_order context.expansionChannel context.expansionScale context.expansionMomentum rgFromPremises completeFromPremises calculationFromPremises).1 · apply certifyPremiseAwareStep context .deriveHigherOrderResidual [.pionInclusiveRGControl, .subleadingComplete, .scaleCalculation] .higherOrderResidual (by decide) intro premises have rgFromPremises := atomOfPremise context [.pionInclusiveRGControl, .subleadingComplete, .scaleCalculation] premises .pionInclusiveRGControl .pionInclusiveRGControlledCouplings (by simp) (by rfl) have completeFromPremises := atomOfPremise context [.pionInclusiveRGControl, .subleadingComplete, .scaleCalculation] premises .subleadingComplete .subleadingAmplitudeComplete (by simp) (by rfl) have calculationFromPremises := atomOfPremise context [.pionInclusiveRGControl, .subleadingComplete, .scaleCalculation] premises .scaleCalculation .scaleCancellationCalculation (by simp) (by rfl) exact atomClaim context .higherOrderResidual .residualScaleDependenceHigherOrder (by rfl) (context.framework.pion_inclusive_rg_control_makes_truncated_amplitude_scale_independent_through_computed_order context.expansionChannel context.expansionScale context.expansionMomentum rgFromPremises completeFromPremises calculationFromPremises).2 exact certifyRoute context .scaleCancellation scaleCancellationRoute (by rfl) dependencies stepsSound (by decide) (by decide) (by decide) theorem singlet_fit_route_is_semantically_realized (context : SemanticContext Channel Scale Momentum Coupling Term Order Regime Fit) (dependencies : routedArgument.RoutesSemanticallyCertified context.interpretAtom (routedArgument.routeDependencyIds singletFitRoute)) (usesData : context.framework.fitUsesNijmegenPhaseShifts context.singletFit context.expansionChannel) (optimized : context.framework.fitOptimizedThroughTwoHundredMeV context.singletFit) (fitCalculation : context.framework.SingletFitCalculation context.singletFit context.expansionChannel context.expansionScale context.expansionMomentum) (validityInterpretation : context.framework.FitValidityInterpretation context.singletFit context.expansionChannel) (assessment : context.framework.HighMomentumTruncationAssessment context.singletFit context.expansionChannel) : routedArgument.RouteSemanticallyCertified context.interpretAtom .singletFit := by have setupClaim := atomClaim context .fitSetup .singletFitSetup (by rfl) ⟨usesData, optimized⟩ have calculationClaim := atomClaim context .fitCalculation .singletFitCalculation (by rfl) fitCalculation have combinationInterpretationClaim := atomClaim context .c0D2Interpretation .c0D2CombinationInterpretation (by rfl) (context.framework.c0_d2_combination_interpretation_is_derived context.singletFit context.expansionChannel context.expansionScale context.expansionMomentum) have expectationClaim := atomClaim context .validityExpectation .fitValidityExpectation (by rfl) validityInterpretation have assessmentClaim := atomClaim context .truncationAssessment .highMomentumTruncationAssessment (by rfl) assessment have stepsSound : argument.StepsSound context.interpretAtom singletFitRoute.steps := by change argument.StepsSound context.interpretAtom [.stateFitSetup, .stateFitCalculation, .deriveExpectedCouplings, .deriveC0D2Combination, .stateC0D2CombinationInterpretation, .interpretC0D2IndividualValues, .derivePhaseAgreement, .stateValidityExpectation, .inferValiditySuggestion, .deriveLargeRatio, .stateTruncationAssessment, .excludeControlledNeglectedTerms] intro stepId stepMem simp at stepMem rcases stepMem with rfl | rfl | rfl | rfl | rfl | rfl | rfl | rfl | rfl | rfl | rfl | rfl · exact certifyPremiseFreeStep context .stateFitSetup .fitSetup (by decide) setupClaim · exact certifyPremiseFreeStep context .stateFitCalculation .fitCalculation (by decide) calculationClaim · apply certifyPremiseAwareStep context .deriveExpectedCouplings [.subleadingComplete, .fitSetup, .fitCalculation] .expectedCouplings (by decide) intro premises have completeFromPremises := atomOfPremise context [.subleadingComplete, .fitSetup, .fitCalculation] premises .subleadingComplete .subleadingAmplitudeComplete (by simp) (by rfl) have setupFromPremises := atomOfPremise context [.subleadingComplete, .fitSetup, .fitCalculation] premises .fitSetup .singletFitSetup (by simp) (by rfl) have calculationFromPremises := atomOfPremise context [.subleadingComplete, .fitSetup, .fitCalculation] premises .fitCalculation .singletFitCalculation (by simp) (by rfl) have result := calculationFromPremises completeFromPremises setupFromPremises.1 setupFromPremises.2 exact atomClaim context .expectedCouplings .fittedCouplingsHaveExpectedScaling (by rfl) ⟨result.1, result.2.1⟩ · apply certifyPremiseAwareStep context .deriveC0D2Combination [.subleadingComplete, .fitSetup, .fitCalculation] .c0D2Combination (by decide) intro premises have completeFromPremises := atomOfPremise context [.subleadingComplete, .fitSetup, .fitCalculation] premises .subleadingComplete .subleadingAmplitudeComplete (by simp) (by rfl) have setupFromPremises := atomOfPremise context [.subleadingComplete, .fitSetup, .fitCalculation] premises .fitSetup .singletFitSetup (by simp) (by rfl) have calculationFromPremises := atomOfPremise context [.subleadingComplete, .fitSetup, .fitCalculation] premises .fitCalculation .singletFitCalculation (by simp) (by rfl) exact atomClaim context .c0D2Combination .c0D2CombinationControlsSubleadingAmplitude (by rfl) (context.framework.singlet_fit_readback_derives_the_contact_combination context.singletFit context.expansionChannel context.expansionScale context.expansionMomentum (calculationFromPremises completeFromPremises setupFromPremises.1 setupFromPremises.2).2.2.1) · exact certifyPremiseFreeStep context .stateC0D2CombinationInterpretation .c0D2Interpretation (by decide) combinationInterpretationClaim · apply certifyPremiseAwareStep context .interpretC0D2IndividualValues [.c0D2Combination, .c0D2Interpretation] .c0D2IndividualMeaning (by decide) intro premises have combinationFromPremises := atomOfPremise context [.c0D2Combination, .c0D2Interpretation] premises .c0D2Combination .c0D2CombinationControlsSubleadingAmplitude (by simp) (by rfl) have interpretationFromPremises := atomOfPremise context [.c0D2Combination, .c0D2Interpretation] premises .c0D2Interpretation .c0D2CombinationInterpretation (by simp) (by rfl) exact atomClaim context .c0D2IndividualMeaning .individualC0D2FitValuesNotSeparatelyMeaningful (by rfl) (interpretationFromPremises combinationFromPremises) · apply certifyPremiseAwareStep context .derivePhaseAgreement [.subleadingComplete, .fitSetup, .fitCalculation] .phaseAgreement (by decide) intro premises have completeFromPremises := atomOfPremise context [.subleadingComplete, .fitSetup, .fitCalculation] premises .subleadingComplete .subleadingAmplitudeComplete (by simp) (by rfl) have setupFromPremises := atomOfPremise context [.subleadingComplete, .fitSetup, .fitCalculation] premises .fitSetup .singletFitSetup (by simp) (by rfl) have calculationFromPremises := atomOfPremise context [.subleadingComplete, .fitSetup, .fitCalculation] premises .fitCalculation .singletFitCalculation (by simp) (by rfl) exact atomClaim context .phaseAgreement .goodSingletPhaseShiftAgreement (by rfl) (calculationFromPremises completeFromPremises setupFromPremises.1 setupFromPremises.2).2.2.2.1 · exact certifyPremiseFreeStep context .stateValidityExpectation .validityExpectation (by decide) expectationClaim · apply certifyPremiseAwareStep context .inferValiditySuggestion [.expectedCouplings, .validityExpectation] .validitySuggestion (by decide) intro premises have expectedFromPremises := atomOfPremise context [.expectedCouplings, .validityExpectation] premises .expectedCouplings .fittedCouplingsHaveExpectedScaling (by simp) (by rfl) have interpretationFromPremises := atomOfPremise context [.expectedCouplings, .validityExpectation] premises .validityExpectation .fitValidityExpectation (by simp) (by rfl) exact atomClaim context .validitySuggestion .fitSuggestsExpansionValidity (by rfl) (interpretationFromPremises expectedFromPremises.1 expectedFromPremises.2) · apply certifyPremiseAwareStep context .deriveLargeRatio [.subleadingComplete, .fitSetup, .fitCalculation] .largeRatio (by decide) intro premises have completeFromPremises := atomOfPremise context [.subleadingComplete, .fitSetup, .fitCalculation] premises .subleadingComplete .subleadingAmplitudeComplete (by simp) (by rfl) have setupFromPremises := atomOfPremise context [.subleadingComplete, .fitSetup, .fitCalculation] premises .fitSetup .singletFitSetup (by simp) (by rfl) have calculationFromPremises := atomOfPremise context [.subleadingComplete, .fitSetup, .fitCalculation] premises .fitCalculation .singletFitCalculation (by simp) (by rfl) exact atomClaim context .largeRatio .largeSubleadingLeadingRatio (by rfl) (calculationFromPremises completeFromPremises setupFromPremises.1 setupFromPremises.2).2.2.2.2 · exact certifyPremiseFreeStep context .stateTruncationAssessment .truncationAssessment (by decide) assessmentClaim · apply certifyPremiseAwareStep context .excludeControlledNeglectedTerms [.largeRatio, .truncationAssessment] .uncontrolledNeglectedTerms (by decide) intro premises have ratioFromPremises := atomOfPremise context [.largeRatio, .truncationAssessment] premises .largeRatio .largeSubleadingLeadingRatio (by simp) (by rfl) have assessmentFromPremises := atomOfPremise context [.largeRatio, .truncationAssessment] premises .truncationAssessment .highMomentumTruncationAssessment (by simp) (by rfl) exact PaperArgument.claimHolds_of_formula argument context.interpretAtom .uncontrolledNeglectedTerms (.neg (.atom .neglectedQuadraticTermsControlled)) (by rfl) (assessmentFromPremises ratioFromPremises) exact certifyRoute context .singletFit singletFitRoute (by rfl) dependencies stepsSound (by decide) (by decide) (by decide) theorem coupled_channel_route_is_semantically_realized (context : SemanticContext Channel Scale Momentum Coupling Term Order Regime Fit) (largeLength : context.framework.largeScatteringLength context.coupledChannel) (analogous : context.framework.coupledPowerCountingAnalogous context.coupledChannel) (calculation : context.framework.CoupledChannelCalculation context.coupledFit context.coupledChannel) : routedArgument.RouteSemanticallyCertified context.interpretAtom .coupledChannel := by have setupClaim := atomClaim context .coupledSetup .coupledChannelSetup (by rfl) ⟨largeLength, analogous⟩ have calculationClaim := atomClaim context .coupledCalculation .coupledChannelCalculation (by rfl) calculation have stepsSound : argument.StepsSound context.interpretAtom coupledChannelRoute.steps := by change argument.StepsSound context.interpretAtom [.stateCoupledSetup, .stateCoupledCalculation, .retainCoupledSMatrixFormula, .deriveLeadingSOnly, .deriveZeroMixingAndDWave, .deriveSubleadingSPhase, .recordMixedObservableOrders, .recordDeferredCoupledFormula, .recordCoupledSFit, .deriveParameterFreePredictions] intro stepId stepMem simp at stepMem rcases stepMem with rfl | rfl | rfl | rfl | rfl | rfl | rfl | rfl | rfl | rfl · exact certifyPremiseFreeStep context .stateCoupledSetup .coupledSetup (by decide) setupClaim · exact certifyPremiseFreeStep context .stateCoupledCalculation .coupledCalculation (by decide) calculationClaim · apply certifyPremiseAwareStep context .retainCoupledSMatrixFormula [.coupledSetup, .coupledCalculation] .coupledSMatrixFormula (by decide) intro premises have setupFromPremises := atomOfPremise context [.coupledSetup, .coupledCalculation] premises .coupledSetup .coupledChannelSetup (by simp) (by rfl) have calculationFromPremises := atomOfPremise context [.coupledSetup, .coupledCalculation] premises .coupledCalculation .coupledChannelCalculation (by simp) (by rfl) exact atomClaim context .coupledSMatrixFormula .coupledSMatrixFormula (by rfl) (context.framework |>.coupled_channel_calculation_retains_displayed_s_matrix_formula context.coupledFit context.coupledChannel setupFromPremises.1 setupFromPremises.2 calculationFromPremises) · apply certifyPremiseAwareStep context .deriveLeadingSOnly [.coupledSetup, .coupledCalculation] .leadingSOnly (by decide) intro premises have setupFromPremises := atomOfPremise context [.coupledSetup, .coupledCalculation] premises .coupledSetup .coupledChannelSetup (by simp) (by rfl) have calculationFromPremises := atomOfPremise context [.coupledSetup, .coupledCalculation] premises .coupledCalculation .coupledChannelCalculation (by simp) (by rfl) exact atomClaim context .leadingSOnly .leadingCoupledAmplitudeOnlySComponent (by rfl) (calculationFromPremises setupFromPremises.1 setupFromPremises.2).1 · apply certifyPremiseAwareStep context .deriveZeroMixingAndDWave [.coupledSetup, .coupledCalculation, .coupledSMatrixFormula, .leadingSOnly] .zeroMixingAndDWave (by decide) intro premises have setupFromPremises := atomOfPremise context [.coupledSetup, .coupledCalculation, .coupledSMatrixFormula, .leadingSOnly] premises .coupledSetup .coupledChannelSetup (by simp) (by rfl) have calculationFromPremises := atomOfPremise context [.coupledSetup, .coupledCalculation, .coupledSMatrixFormula, .leadingSOnly] premises .coupledCalculation .coupledChannelCalculation (by simp) (by rfl) have formulaFromPremises := atomOfPremise context [.coupledSetup, .coupledCalculation, .coupledSMatrixFormula, .leadingSOnly] premises .coupledSMatrixFormula .coupledSMatrixFormula (by simp) (by rfl) have leadingFromPremises := atomOfPremise context [.coupledSetup, .coupledCalculation, .coupledSMatrixFormula, .leadingSOnly] premises .leadingSOnly .leadingCoupledAmplitudeOnlySComponent (by simp) (by rfl) have result := calculationFromPremises setupFromPremises.1 setupFromPremises.2 have phases := context.framework.coupledSMatrixFormulaReadout |>.zero_amplitudes_determine_phases_on_branch context.coupledChannel context.framework.leadingOrder formulaFromPremises result.2.1.2 (fun momentum => ⟨(leadingFromPremises momentum).1, (leadingFromPremises momentum).2.2⟩) exact atomClaim context .zeroMixingAndDWave .leadingMixingAndDWavePhasesZero (by rfl) ⟨fun momentum => (phases momentum).1, fun momentum => (phases momentum).2⟩ · apply certifyPremiseAwareStep context .deriveSubleadingSPhase [.coupledSetup, .coupledCalculation] .subleadingSPhase (by decide) intro premises have setupFromPremises := atomOfPremise context [.coupledSetup, .coupledCalculation] premises .coupledSetup .coupledChannelSetup (by simp) (by rfl) have calculationFromPremises := atomOfPremise context [.coupledSetup, .coupledCalculation] premises .coupledCalculation .coupledChannelCalculation (by simp) (by rfl) exact atomClaim context .subleadingSPhase .subleadingSPhaseCalculated (by rfl) (calculationFromPremises setupFromPremises.1 setupFromPremises.2).2.2.1 · apply certifyPremiseAwareStep context .recordMixedObservableOrders [.coupledSetup, .coupledCalculation] .mixedObservableOrders (by decide) intro premises have setupFromPremises := atomOfPremise context [.coupledSetup, .coupledCalculation] premises .coupledSetup .coupledChannelSetup (by simp) (by rfl) have calculationFromPremises := atomOfPremise context [.coupledSetup, .coupledCalculation] premises .coupledCalculation .coupledChannelCalculation (by simp) (by rfl) exact atomClaim context .mixedObservableOrders .mixingAndDWaveOnlyLeadingOrder (by rfl) (calculationFromPremises setupFromPremises.1 setupFromPremises.2).2.2.2.1 · apply certifyPremiseAwareStep context .recordDeferredCoupledFormula [.coupledSetup, .coupledCalculation] .deferredCoupledFormula (by decide) intro premises have setupFromPremises := atomOfPremise context [.coupledSetup, .coupledCalculation] premises .coupledSetup .coupledChannelSetup (by simp) (by rfl) have calculationFromPremises := atomOfPremise context [.coupledSetup, .coupledCalculation] premises .coupledCalculation .coupledChannelCalculation (by simp) (by rfl) exact atomClaim context .deferredCoupledFormula .analyticSubleadingCoupledFormulaDeferred (by rfl) (calculationFromPremises setupFromPremises.1 setupFromPremises.2).2.2.2.2.1 · apply certifyPremiseAwareStep context .recordCoupledSFit [.coupledSetup, .coupledCalculation] .fittedSPhase (by decide) intro premises have setupFromPremises := atomOfPremise context [.coupledSetup, .coupledCalculation] premises .coupledSetup .coupledChannelSetup (by simp) (by rfl) have calculationFromPremises := atomOfPremise context [.coupledSetup, .coupledCalculation] premises .coupledCalculation .coupledChannelCalculation (by simp) (by rfl) exact atomClaim context .fittedSPhase .coupledSPhaseFitted (by rfl) (calculationFromPremises setupFromPremises.1 setupFromPremises.2).2.2.2.2.2.1 · apply certifyPremiseAwareStep context .deriveParameterFreePredictions [.coupledSetup, .coupledCalculation, .fittedSPhase] .parameterFreePredictions (by decide) intro premises have setupFromPremises := atomOfPremise context [.coupledSetup, .coupledCalculation, .fittedSPhase] premises .coupledSetup .coupledChannelSetup (by simp) (by rfl) have calculationFromPremises := atomOfPremise context [.coupledSetup, .coupledCalculation, .fittedSPhase] premises .coupledCalculation .coupledChannelCalculation (by simp) (by rfl) have fittedFromPremises := atomOfPremise context [.coupledSetup, .coupledCalculation, .fittedSPhase] premises .fittedSPhase .coupledSPhaseFitted (by simp) (by rfl) exact atomClaim context .parameterFreePredictions .mixingAndDWaveParameterFreeAtDeclaredOrder (by rfl) ⟨fittedFromPremises, (calculationFromPremises setupFromPremises.1 setupFromPremises.2).2.2.2.2.2.2⟩ have dependencies : routedArgument.RoutesSemanticallyCertified context.interpretAtom (routedArgument.routeDependencyIds coupledChannelRoute) := by change routedArgument.RoutesSemanticallyCertified context.interpretAtom [] intro routeId routeMem simp at routeMem exact certifyRoute context .coupledChannel coupledChannelRoute (by rfl) dependencies stepsSound (by decide) (by decide) (by decide) /-- The coupled-channel route exposes KSW's displayed S-matrix formula before the zero-mixing and zero-D-wave consequence is used downstream. -/ theorem coupled_channel_route_exposes_displayed_s_matrix_formula (context : SemanticContext Channel Scale Momentum Coupling Term Order Regime Fit) (largeLength : context.framework.largeScatteringLength context.coupledChannel) (analogous : context.framework.coupledPowerCountingAnalogous context.coupledChannel) (calculation : context.framework.CoupledChannelCalculation context.coupledFit context.coupledChannel) : context.interpretAtom .coupledSMatrixFormula := context.framework |>.coupled_channel_calculation_retains_displayed_s_matrix_formula context.coupledFit context.coupledChannel largeLength analogous calculation /-- Raw paper-local inputs construct every KSW route in source order. -/ theorem all_routes_are_semantically_realizable (context : SemanticContext Channel Scale Momentum Coupling Term Order Regime Fit) (lowPionless : context.framework.pionlessMomentum context.lowMomentum) (lowLargeLength : context.framework.largeScatteringLength context.lowChannel) (lowPds : context.framework.pdsSubtractionAt context.lowScale) (lowBubble : (context.framework.pionlessLeadingContactOrderAt context.lowChannel context.lowScale context.lowMomentum = -1 ∧ context.framework.pionlessBubbleLoopOrderAt context.lowScale context.lowMomentum = 1)) (loopCalculation : context.framework.PDSLoopCalculation context.lowChannel context.lowScale context.lowMomentum) (resummationCalculation : context.framework.BubbleResummationCalculation context.lowChannel context.lowScale context.lowMomentum) (unitarityCalculation : context.framework.PionlessUnitarityCalculation context.lowChannel context.lowScale context.lowMomentum) (rangeMatching : context.framework.effectiveRangeDataMatched context.lowChannel) (scaleRequirement : context.framework.physicalAmplitudeRequiredScaleIndependent context.lowChannel context.lowMomentum) (rgCalculation : context.framework.PionlessRGCalculation context.lowChannel context.lowScale context.lowMomentum) (naturalMS : context.framework.naturalScatteringLength context.naturalMSChannel) (largeLengthMS : context.framework.largeScatteringLength context.largeLengthMSChannel) (minimalSubtraction : context.framework.minimalSubtractionAt context.msScale) (msPionless : context.framework.pionlessMomentum context.msMomentum) (smallComparedWithRange : context.framework.momentumSmallComparedWithShortRangeScale context.naturalMSChannel context.msMomentum) (naturalMSCalculation : context.framework.NaturalMSPowerCountingCalculation context.naturalMSChannel context.msScale context.msMomentum) (largeLengthMSCalculation : context.framework.LargeLengthMSRestrictionCalculation context.largeLengthMSChannel context.msScale) (expansionLargeLength : context.framework.largeScatteringLength context.expansionChannel) (expansionPds : context.framework.pdsSubtractionAt context.expansionScale) (comparable : context.framework.scaleComparableToMomentum context.expansionScale context.expansionMomentum) (loopScaling : context.framework.loopHasOrderMomentum context.expansionScale context.expansionMomentum) (couplingScaling : context.framework.couplingScalingEstablished context.expansionChannel context.expansionScale context.expansionMomentum) (powerCountingCalculation : context.framework.LargeScatteringLengthPowerCountingCalculation context.expansionChannel context.expansionScale context.expansionMomentum) (pionScale : context.framework.pionScaleMomentum context.expansionMomentum) (explicitCalculation : context.framework.ExplicitPionSubleadingCalculation context.expansionChannel context.expansionScale context.expansionMomentum) (scaleCalculation : context.framework.ScaleCancellationCalculation context.expansionChannel context.expansionScale context.expansionMomentum) (usesData : context.framework.fitUsesNijmegenPhaseShifts context.singletFit context.expansionChannel) (optimized : context.framework.fitOptimizedThroughTwoHundredMeV context.singletFit) (fitCalculation : context.framework.SingletFitCalculation context.singletFit context.expansionChannel context.expansionScale context.expansionMomentum) (validityInterpretation : context.framework.FitValidityInterpretation context.singletFit context.expansionChannel) (assessment : context.framework.HighMomentumTruncationAssessment context.singletFit context.expansionChannel) (coupledLargeLength : context.framework.largeScatteringLength context.coupledChannel) (analogous : context.framework.coupledPowerCountingAnalogous context.coupledChannel) (coupledCalculation : context.framework.CoupledChannelCalculation context.coupledFit context.coupledChannel) : routedArgument.RoutesSemanticallyCertified context.interpretAtom routedArgument.routeIds := by have pionlessCertificate := pionless_pds_route_is_semantically_realized context lowPionless lowLargeLength lowPds lowBubble loopCalculation resummationCalculation unitarityCalculation rangeMatching scaleRequirement rgCalculation have minimalCertificate := minimal_subtraction_scope_route_is_semantically_realized context naturalMS largeLengthMS minimalSubtraction msPionless smallComparedWithRange naturalMSCalculation largeLengthMSCalculation have largeCertificate := large_length_power_counting_route_is_semantically_realized context expansionLargeLength expansionPds comparable loopScaling couplingScaling powerCountingCalculation have explicitDependencies : routedArgument.RoutesSemanticallyCertified context.interpretAtom (routedArgument.routeDependencyIds explicitPionsRoute) := by change routedArgument.RoutesSemanticallyCertified context.interpretAtom [.largeLengthPowerCounting] intro routeId routeMem simp at routeMem rcases routeMem with rfl exact largeCertificate have explicitCertificate := explicit_pions_route_is_semantically_realized context explicitDependencies pionScale explicitCalculation have scaleDependencies : routedArgument.RoutesSemanticallyCertified context.interpretAtom (routedArgument.routeDependencyIds scaleCancellationRoute) := by change routedArgument.RoutesSemanticallyCertified context.interpretAtom [.explicitPions, .largeLengthPowerCounting] intro routeId routeMem simp at routeMem rcases routeMem with rfl | rfl · exact explicitCertificate · exact largeCertificate have scaleCertificate := scale_cancellation_route_is_semantically_realized context scaleDependencies scaleCalculation have fitDependencies : routedArgument.RoutesSemanticallyCertified context.interpretAtom (routedArgument.routeDependencyIds singletFitRoute) := by change routedArgument.RoutesSemanticallyCertified context.interpretAtom [.explicitPions, .largeLengthPowerCounting] intro routeId routeMem simp at routeMem rcases routeMem with rfl | rfl · exact explicitCertificate · exact largeCertificate have fitCertificate := singlet_fit_route_is_semantically_realized context fitDependencies usesData optimized fitCalculation validityInterpretation assessment have coupledCertificate := coupled_channel_route_is_semantically_realized context coupledLargeLength analogous coupledCalculation change routedArgument.RoutesSemanticallyCertified context.interpretAtom [.pionlessPDS, .minimalSubtractionScope, .largeLengthPowerCounting, .explicitPions, .scaleCancellation, .singletFit, .coupledChannel] intro routeId routeMem simp at routeMem rcases routeMem with rfl | rfl | rfl | rfl | rfl | rfl | rfl · exact pionlessCertificate · exact minimalCertificate · exact largeCertificate · exact explicitCertificate · exact scaleCertificate · exact fitCertificate · exact coupledCertificate theorem route_semantic_realization_is_exhaustive (context : SemanticContext Channel Scale Momentum Coupling Term Order Regime Fit) (lowPionless : context.framework.pionlessMomentum context.lowMomentum) (lowLargeLength : context.framework.largeScatteringLength context.lowChannel) (lowPds : context.framework.pdsSubtractionAt context.lowScale) (lowBubble : (context.framework.pionlessLeadingContactOrderAt context.lowChannel context.lowScale context.lowMomentum = -1 ∧ context.framework.pionlessBubbleLoopOrderAt context.lowScale context.lowMomentum = 1)) (loopCalculation : context.framework.PDSLoopCalculation context.lowChannel context.lowScale context.lowMomentum) (resummationCalculation : context.framework.BubbleResummationCalculation context.lowChannel context.lowScale context.lowMomentum) (unitarityCalculation : context.framework.PionlessUnitarityCalculation context.lowChannel context.lowScale context.lowMomentum) (rangeMatching : context.framework.effectiveRangeDataMatched context.lowChannel) (scaleRequirement : context.framework.physicalAmplitudeRequiredScaleIndependent context.lowChannel context.lowMomentum) (rgCalculation : context.framework.PionlessRGCalculation context.lowChannel context.lowScale context.lowMomentum) (naturalMS : context.framework.naturalScatteringLength context.naturalMSChannel) (largeLengthMS : context.framework.largeScatteringLength context.largeLengthMSChannel) (minimalSubtraction : context.framework.minimalSubtractionAt context.msScale) (msPionless : context.framework.pionlessMomentum context.msMomentum) (smallComparedWithRange : context.framework.momentumSmallComparedWithShortRangeScale context.naturalMSChannel context.msMomentum) (naturalMSCalculation : context.framework.NaturalMSPowerCountingCalculation context.naturalMSChannel context.msScale context.msMomentum) (largeLengthMSCalculation : context.framework.LargeLengthMSRestrictionCalculation context.largeLengthMSChannel context.msScale) (expansionLargeLength : context.framework.largeScatteringLength context.expansionChannel) (expansionPds : context.framework.pdsSubtractionAt context.expansionScale) (comparable : context.framework.scaleComparableToMomentum context.expansionScale context.expansionMomentum) (loopScaling : context.framework.loopHasOrderMomentum context.expansionScale context.expansionMomentum) (couplingScaling : context.framework.couplingScalingEstablished context.expansionChannel context.expansionScale context.expansionMomentum) (powerCountingCalculation : context.framework.LargeScatteringLengthPowerCountingCalculation context.expansionChannel context.expansionScale context.expansionMomentum) (pionScale : context.framework.pionScaleMomentum context.expansionMomentum) (explicitCalculation : context.framework.ExplicitPionSubleadingCalculation context.expansionChannel context.expansionScale context.expansionMomentum) (scaleCalculation : context.framework.ScaleCancellationCalculation context.expansionChannel context.expansionScale context.expansionMomentum) (usesData : context.framework.fitUsesNijmegenPhaseShifts context.singletFit context.expansionChannel) (optimized : context.framework.fitOptimizedThroughTwoHundredMeV context.singletFit) (fitCalculation : context.framework.SingletFitCalculation context.singletFit context.expansionChannel context.expansionScale context.expansionMomentum) (validityInterpretation : context.framework.FitValidityInterpretation context.singletFit context.expansionChannel) (assessment : context.framework.HighMomentumTruncationAssessment context.singletFit context.expansionChannel) (coupledLargeLength : context.framework.largeScatteringLength context.coupledChannel) (analogous : context.framework.coupledPowerCountingAnalogous context.coupledChannel) (coupledCalculation : context.framework.CoupledChannelCalculation context.coupledFit context.coupledChannel) : routedArgument.RoutesSemanticallyCertified context.interpretAtom routedArgument.routeIds := all_routes_are_semantically_realizable context lowPionless lowLargeLength lowPds lowBubble loopCalculation resummationCalculation unitarityCalculation rangeMatching scaleRequirement rgCalculation naturalMS largeLengthMS minimalSubtraction msPionless smallComparedWithRange naturalMSCalculation largeLengthMSCalculation expansionLargeLength expansionPds comparable loopScaling couplingScaling powerCountingCalculation pionScale explicitCalculation scaleCalculation usesData optimized fitCalculation validityInterpretation assessment coupledLargeLength analogous coupledCalculation end SemanticContext end PhysicsLogic.Papers.KaplanSavageWise1998