import PhysicsLogic.Logic.Route /-! # Kaplan-Savage-Wise 1998 Source Map This module records provenance and route order in the original paper. The semantic formalization remains in `PhysicsLogic.Papers.KaplanSavageWise1998`. -/ set_option autoImplicit false namespace PhysicsLogic.Papers.KaplanSavageWise1998 open PhysicsLogic.Logic inductive Atom where | pionlessPDSSetup | pdsLoopCalculation | bubbleResummationCalculation | pionlessUnitarityCalculation | pdsLoopIntegral | pdsLoopFormula | pdsAmplitude | pdsAmplitudeFormula | unitaryAmplitude | effectiveRangeMatching | physicalScaleIndependenceRequirement | pionlessRGCalculation | exactC0C2BetaFunctions | c0C2PionlessRGControl | fullAmplitudeScaleIndependent | naturalMSSetup | largeLengthMSSetup | naturalMSPowerCountingCalculation | largeLengthMSRestrictionCalculation | naturalMSCountingValid | largeLengthMSValidityRequiresInverseLengthWindow | largeLengthMSRangeRestricted | largeLengthScalingSetup | largeLengthPowerCountingCalculation | mixedKSWExpansion | kswAmplitudeExpansion | resummedNonuniformPowerCounting | pionScaleSetup | explicitPionSubleadingCalculation | potentialPionAtSubleadingOrder | radiationPionsAbsentAtSubleadingOrder | logarithmicSubleadingScaleDependence | d2CountertermRequired | d2NotSubdominantToOnePionExchange | pionInclusiveRGControlledCouplings | subleadingAmplitudeComplete | weinbergCountingFailure | scaleCancellationCalculation | fullPionAmplitudeScaleIndependent | truncatedScaleIndependentThroughSubleading | residualScaleDependenceHigherOrder | singletFitSetup | singletFitCalculation | fittedCouplingsHaveExpectedScaling | c0D2CombinationControlsSubleadingAmplitude | c0D2CombinationInterpretation | individualC0D2FitValuesNotSeparatelyMeaningful | goodSingletPhaseShiftAgreement | fitValidityExpectation | fitSuggestsExpansionValidity | largeSubleadingLeadingRatio | highMomentumTruncationAssessment | neglectedQuadraticTermsControlled | coupledChannelSetup | coupledChannelCalculation | coupledSMatrixFormula | leadingCoupledAmplitudeOnlySComponent | leadingMixingAndDWavePhasesZero | subleadingSPhaseCalculated | mixingAndDWaveOnlyLeadingOrder | analyticSubleadingCoupledFormulaDeferred | coupledSPhaseFitted | mixingAndDWaveParameterFreeAtDeclaredOrder deriving DecidableEq, Repr inductive ClaimId where | pdsSetup | loopCalculation | resummationCalculation | unitarityCalculation | loopIntegral | loopFormula | amplitude | amplitudeFormula | unitarity | rangeMatching | scaleRequirement | rgCalculation | betaFunctions | c0C2RGControl | fullScaleIndependence | naturalMSRegime | largeLengthMSRegime | naturalMSCalculation | largeLengthMSCalculation | naturalMSValidity | largeLengthMSWindow | largeLengthMSRestriction | scalingSetup | scalingCalculation | mixedExpansion | amplitudeExpansion | sharedPowerCounting | pionSetup | pionCalculation | potentialPion | radiationPionAbsence | logarithmicScaleDependence | d2Required | d2Unsuppressed | pionInclusiveRGControl | subleadingComplete | weinbergFailure | scaleCalculation | fullPionScaleIndependence | truncatedScaleIndependence | higherOrderResidual | fitSetup | fitCalculation | expectedCouplings | c0D2Combination | c0D2Interpretation | c0D2IndividualMeaning | phaseAgreement | validityExpectation | validitySuggestion | largeRatio | truncationAssessment | uncontrolledNeglectedTerms | coupledSetup | coupledCalculation | coupledSMatrixFormula | leadingSOnly | zeroMixingAndDWave | subleadingSPhase | mixedObservableOrders | deferredCoupledFormula | fittedSPhase | parameterFreePredictions deriving DecidableEq, Repr inductive StepId where | statePDSSetup | stateLoopCalculation | stateResummationCalculation | stateUnitarityCalculation | deriveLoopIntegral | retainPDSLoopFormula | derivePDSAmplitude | retainPDSAmplitudeFormula | deriveUnitarity | stateEffectiveRangeMatching | imposePhysicalScaleIndependence | stateRGCalculation | deriveBetaFunctions | deriveC0C2RGControl | deriveFullScaleIndependence | stateNaturalMSRegime | stateLargeLengthMSRegime | stateNaturalMSCalculation | stateLargeLengthMSCalculation | deriveNaturalMSValidity | deriveLargeLengthMSWindow | deriveLargeLengthMSRestriction | stateScalingSetup | stateScalingCalculation | deriveMixedExpansion | deriveAmplitudeExpansion | realizeSharedPowerCounting | statePionSetup | statePionCalculation | derivePotentialPionOrder | deriveRadiationPionAbsence | deriveLogarithmicDependence | requireD2Counterterm | deriveD2Unsuppressed | derivePionInclusiveRGControl | deriveSubleadingCompleteness | excludeWeinbergCounting | stateScaleCancellation | deriveFullPionScaleIndependence | deriveTruncatedScaleIndependence | deriveHigherOrderResidual | stateFitSetup | stateFitCalculation | deriveExpectedCouplings | deriveC0D2Combination | stateC0D2CombinationInterpretation | interpretC0D2IndividualValues | derivePhaseAgreement | stateValidityExpectation | inferValiditySuggestion | deriveLargeRatio | stateTruncationAssessment | excludeControlledNeglectedTerms | stateCoupledSetup | stateCoupledCalculation | retainCoupledSMatrixFormula | deriveLeadingSOnly | deriveZeroMixingAndDWave | deriveSubleadingSPhase | recordMixedObservableOrders | recordDeferredCoupledFormula | recordCoupledSFit | deriveParameterFreePredictions deriving DecidableEq, Repr def originalPaper (locator : String) (relation : SourceRelation) : SourceRef := { work := "D. B. Kaplan, M. J. Savage, and M. B. Wise, A New Expansion for Nucleon-Nucleon Interactions (1998)" locator := locator relation := relation } def arxivPage (page : String) (locator : String) (relation : SourceRelation) : SourceRef := originalPaper ("arXiv:nucl-th/9801034v2 p. " ++ page ++ ", " ++ locator) relation def claims : List (Claim ClaimId Atom) := [ { id := .pdsSetup formula := .atom .pionlessPDSSetup role := .setupPremise sources := [arxivPage "2-3" "pionless low-momentum theory, large scattering length, PDS subtraction, and bubble chain" .directStatement] }, { id := .loopCalculation formula := .atom .pdsLoopCalculation role := .intermediate sources := [arxivPage "3" "PDS subtraction counterterm, printed equation (3)" .directStatement] }, { id := .resummationCalculation formula := .atom .bubbleResummationCalculation role := .intermediate sources := [arxivPage "3" "bubble-chain resummation, printed equation (5)" .directStatement] }, { id := .unitarityCalculation formula := .atom .pionlessUnitarityCalculation role := .intermediate sources := [arxivPage "3" "real elastic contact and inverse-amplitude observable normalization in printed equation (7)" .directStatement] }, { id := .loopIntegral formula := .atom .pdsLoopIntegral role := .intermediate sources := [arxivPage "3" "PDS-subtracted integral, printed equation (4)" .directStatement] }, { id := .loopFormula formula := .atom .pdsLoopFormula role := .intermediate sources := [arxivPage "3" "retain I_n^PDS = -(M E)^n (M/4 pi) (mu + i p), printed equation (4)" .directStatement] }, { id := .amplitude formula := .atom .pdsAmplitude role := .mainConclusion sources := [arxivPage "3" "all-orders bubble amplitude, printed equation (5)" .directStatement] }, { id := .amplitudeFormula formula := .atom .pdsAmplitudeFormula role := .intermediate sources := [arxivPage "3" "retain i A = -i C(p^2,mu)/(1 + M C(p^2,mu)(mu+i p)/(4 pi)), printed equation (5)" .directStatement] }, { id := .unitarity formula := .atom .unitaryAmplitude role := .mainConclusion sources := [arxivPage "3" "scalar S = 1 + i p M A/(2 pi), elastic norm one, and the nonsingular inverse-amplitude relation, printed equations (5)-(7) and footnote 2" .directStatement] }, { id := .rangeMatching formula := .atom .effectiveRangeMatching role := .setupPremise sources := [arxivPage "3-4" "p cot(delta) = -1/a + (r_0/2) p^2 + ..., printed equations (7)-(8)" .directStatement] }, { id := .scaleRequirement formula := .atom .physicalScaleIndependenceRequirement role := .setupPremise sources := [arxivPage "4" "coupling-scale dependence must cancel explicit amplitude dependence" .directStatement] }, { id := .rgCalculation formula := .atom .pionlessRGCalculation role := .intermediate sources := [arxivPage "4" "RG equations and the value-level C0(mu), C2(mu) solutions, equations (9)-(11)" .directStatement] }, { id := .betaFunctions formula := .atom .exactC0C2BetaFunctions role := .mainConclusion sources := [arxivPage "4" "mu dC0/dmu = M C0^2 mu/(4 pi) and mu dC2/dmu = M C0 C2 mu/(2 pi), equations (9)-(10); actual real-scale derivatives verified from the non-pole equation-(11) family" .directStatement] }, { id := .c0C2RGControl formula := .atom .c0C2PionlessRGControl role := .mainConclusion sources := [arxivPage "4" "C0(mu) = (4 pi/M)/(-mu + 1/a) and C2(mu) = (2 pi/M)/(-mu + 1/a)^2 r0 at non-pole scales in equation (11), together with equations (9)-(10); nonconstant C2 is not asserted when r0 vanishes" .directStatement] }, { id := .fullScaleIndependence formula := .atom .fullAmplitudeScaleIndependent role := .mainConclusion sources := [arxivPage "4" "physical amplitude is subtraction-scale independent" .directStatement] }, { id := .naturalMSRegime formula := .atom .naturalMSSetup role := .setupPremise sources := [arxivPage "4" "natural scattering length, mu=0 minimal subtraction, and p/Lambda small" .directStatement] }, { id := .largeLengthMSRegime formula := .atom .largeLengthMSSetup role := .setupPremise sources := [arxivPage "4" "unnaturally large scattering length at mu=0 in the pionless regime" .directStatement] }, { id := .naturalMSCalculation formula := .atom .naturalMSPowerCountingCalculation role := .intermediate sources := [arxivPage "4" "ordinary perturbative p/Lambda counting for natural scattering length" .directStatement] }, { id := .largeLengthMSCalculation formula := .atom .largeLengthMSRestrictionCalculation role := .intermediate sources := [arxivPage "4" "large coefficients restrict the mu=0 momentum expansion" .directStatement] }, { id := .naturalMSValidity formula := .atom .naturalMSCountingValid role := .mainConclusion sources := [arxivPage "4" "ordinary MS power counting is valid for natural scattering length and p/Lambda small" .directStatement] }, { id := .largeLengthMSWindow formula := .atom .largeLengthMSValidityRequiresInverseLengthWindow role := .mainConclusion sources := [arxivPage "4" "C_2n scaling makes p |a| the ordinary-MS expansion parameter, so validity requires p much smaller than 1/|a|" .normalizedStatement] }, { id := .largeLengthMSRestriction formula := .atom .largeLengthMSRangeRestricted role := .mainConclusion sources := [arxivPage "4" "for very large |a| and mu=0 the natural-length momentum expansion is valid only over a small range" .directStatement] }, { id := .scalingSetup formula := .atom .largeLengthScalingSetup role := .setupPremise sources := [arxivPage "4" "large scattering length, nonzero PDS scale, mu of order p, and scaling inputs" .directStatement] }, { id := .scalingCalculation formula := .atom .largeLengthPowerCountingCalculation role := .intermediate sources := [arxivPage "4-5" "C2n and loop scaling in the large-length regime" .directStatement] }, { id := .mixedExpansion formula := .atom .mixedKSWExpansion role := .mainConclusion sources := [arxivPage "4-5" "C0 is summed to all orders while higher contacts are perturbative" .directStatement] }, { id := .amplitudeExpansion formula := .atom .kswAmplitudeExpansion role := .mainConclusion sources := [arxivPage "4-5" "printed equations (12)-(13): asymptotic order assignment and actual A_-1=-C0/D, A_0=-C2 p^2/D^2 with D=1+M C0(mu+i p)/(4 pi)" .directStatement, arxivPage "3,5" "the scalar S normalization and single derivative insertion give the first-order optical theorem; exact unitarity of the truncated sum is not asserted" .reconstructedStep] }, { id := .sharedPowerCounting formula := .atom .resummedNonuniformPowerCounting role := .mainConclusion sources := [arxivPage "4-5" "systematic expansion has a resummed leading sector and is not uniformly perturbative" .normalizedStatement] }, { id := .pionSetup formula := .atom .pionScaleSetup role := .setupPremise sources := [arxivPage "5" "momenta of order pion mass with the mixed expansion" .directStatement] }, { id := .pionCalculation formula := .atom .explicitPionSubleadingCalculation role := .intermediate sources := [arxivPage "5-7" "five subleading graphs, beta functions, and counterterms" .directStatement] }, { id := .potentialPion formula := .atom .potentialPionAtSubleadingOrder role := .intermediate sources := [arxivPage "5-6" "one potential pion contributes at order p^0" .directStatement] }, { id := .radiationPionAbsence formula := .atom .radiationPionsAbsentAtSubleadingOrder role := .intermediate sources := [arxivPage "6" "radiation pions do not contribute at this order" .directStatement] }, { id := .logarithmicScaleDependence formula := .atom .logarithmicSubleadingScaleDependence role := .intermediate sources := [arxivPage "6" "A0(IV) has logarithmic subtraction-scale dependence" .directStatement] }, { id := .d2Required formula := .atom .d2CountertermRequired role := .mainConclusion sources := [arxivPage "6" "D2 m_pi^2 operator is required at subleading order" .directStatement] }, { id := .d2Unsuppressed formula := .atom .d2NotSubdominantToOnePionExchange role := .mainConclusion sources := [arxivPage "6, footnote 3" "the D2 operator is not subdominant to one-pion exchange when C0 is resummed" .directStatement] }, { id := .pionInclusiveRGControl formula := .atom .pionInclusiveRGControlledCouplings role := .mainConclusion sources := [arxivPage "7" "computed-order pion-inclusive beta functions: M(C0^2+C0 g_A^2/f^2) mu/(4 pi), M C0 C2 mu/(2 pi), and the inhomogeneous D2 equation (18); these are retained-model equations, not all-orders beta functions" .directStatement] }, { id := .subleadingComplete formula := .atom .subleadingAmplitudeComplete role := .mainConclusion sources := [arxivPage "5-7" "complete declared A0 contribution including contact and pion terms" .directStatement] }, { id := .weinbergFailure formula := .atom .weinbergCountingFailure role := .mainConclusion sources := [arxivPage "6" "D2 is required for subtraction-point independence, contributes at p^0, is not subdominant to one-pion exchange, and therefore contradicts Weinberg ordering for these systems" .directStatement] }, { id := .scaleCalculation formula := .atom .scaleCancellationCalculation role := .intermediate sources := [arxivPage "7" "running-coupling cancellation: full amplitude invariant, retained expression independent through p^0, and higher-order terms cancel its residual dependence; formal coefficients do not imply a numerical remainder bound" .directStatement] }, { id := .fullPionScaleIndependence formula := .atom .fullPionAmplitudeScaleIndependent role := .mainConclusion sources := [arxivPage "7" "the full amplitude expressed in the pion-inclusive running couplings is independent of mu" .directStatement] }, { id := .truncatedScaleIndependence formula := .atom .truncatedScaleIndependentThroughSubleading role := .mainConclusion sources := [arxivPage "7" "A_-1+A_0 is scale independent only through order p^0" .directStatement] }, { id := .higherOrderResidual formula := .atom .residualScaleDependenceHigherOrder role := .mainConclusion sources := [arxivPage "7" "remaining scale dependence is canceled by higher orders" .directStatement] }, { id := .fitSetup formula := .atom .singletFitSetup role := .setupPremise sources := [arxivPage "7" "subleading singlet amplitude fitted to Nijmegen data through 200 MeV" .directStatement] }, { id := .fitCalculation formula := .atom .singletFitCalculation role := .intermediate sources := [arxivPage "7-8" "parameter fit and phase-shift comparison" .directStatement] }, { id := .expectedCouplings formula := .atom .fittedCouplingsHaveExpectedScaling role := .evidence sources := [arxivPage "7" "C0 near its leading value and C2 of expected size" .directStatement] }, { id := .c0D2Combination formula := .atom .c0D2CombinationControlsSubleadingAmplitude role := .intermediate sources := [arxivPage "7" "through the computed order the amplitude can be written using the C0 + D2 m_pi^2 combination" .directStatement] }, { id := .c0D2Interpretation formula := .atom .c0D2CombinationInterpretation role := .setupPremise sources := [arxivPage "7" "the parenthetical interpretation of the C0 + D2 m_pi^2 combination" .directStatement] }, { id := .c0D2IndividualMeaning formula := .atom .individualC0D2FitValuesNotSeparatelyMeaningful role := .interpretation sources := [arxivPage "7" "the separately quoted C0 and D2 fit values are not particularly meaningful" .directStatement] }, { id := .phaseAgreement formula := .atom .goodSingletPhaseShiftAgreement role := .evidence sources := [arxivPage "7-8" "excellent phase-shift agreement in Figure 3" .directStatement] }, { id := .validityExpectation formula := .atom .fitValidityExpectation role := .setupPremise sources := [arxivPage "7" "authors state that the fitted sizes suggest validity in this channel" .directStatement] }, { id := .validitySuggestion formula := .atom .fitSuggestsExpansionValidity role := .interpretation sources := [arxivPage "7" "coupling sizes suggest validity in the singlet channel" .directStatement] }, { id := .largeRatio formula := .atom .largeSubleadingLeadingRatio role := .evidence sources := [arxivPage "8" "|A0/A-1| exceeds approximately one half above 100 MeV" .directStatement] }, { id := .truncationAssessment formula := .atom .highMomentumTruncationAssessment role := .intermediate sources := [arxivPage "8" "assessment of omitted terms quadratic in A0/A-1" .directStatement] }, { id := .uncontrolledNeglectedTerms formula := .neg (.atom .neglectedQuadraticTermsControlled) role := .mainConclusion sources := [arxivPage "8" "approximations are difficult to justify above 100 MeV" .directStatement] }, { id := .coupledSetup formula := .atom .coupledChannelSetup role := .setupPremise sources := [arxivPage "8-9" "large triplet scattering length and analogous power counting" .directStatement] }, { id := .coupledCalculation formula := .atom .coupledChannelCalculation role := .intermediate sources := [arxivPage "8-9" "coupled-channel leading and subleading analysis" .directStatement] }, { id := .coupledSMatrixFormula formula := .atom .coupledSMatrixFormula role := .intermediate sources := [arxivPage "8" "displayed S - 1 = i p M A / (2 pi) coupled-channel phase matrix" .directStatement] }, { id := .leadingSOnly formula := .atom .leadingCoupledAmplitudeOnlySComponent role := .mainConclusion sources := [arxivPage "8" "only A00 is nonzero at leading order" .directStatement] }, { id := .zeroMixingAndDWave formula := .atom .leadingMixingAndDWavePhasesZero role := .mainConclusion sources := [arxivPage "8" "epsilon1 and delta2 vanish at leading order" .directStatement] }, { id := .subleadingSPhase formula := .atom .subleadingSPhaseCalculated role := .mainConclusion sources := [arxivPage "8-9" "delta0 is calculated through subleading order" .directStatement] }, { id := .mixedObservableOrders formula := .atom .mixingAndDWaveOnlyLeadingOrder role := .mainConclusion sources := [arxivPage "9" "epsilon1 and delta2 are only leading-order results" .directStatement] }, { id := .deferredCoupledFormula formula := .atom .analyticSubleadingCoupledFormulaDeferred role := .mainConclusion sources := [arxivPage "8-9" "analytic order-p^0 coupled amplitudes deferred to future work" .directStatement] }, { id := .fittedSPhase formula := .atom .coupledSPhaseFitted role := .evidence sources := [arxivPage "9" "three A00 parameters fitted to delta0" .directStatement] }, { id := .parameterFreePredictions formula := .atom .mixingAndDWaveParameterFreeAtDeclaredOrder role := .mainConclusion sources := [arxivPage "9" "epsilon1 and delta2 have no free parameters after fitting delta0" .directStatement] } ] def rawSteps : List (ArgumentStep StepId ClaimId) := [ { id := .statePDSSetup, premises := [], conclusion := .pdsSetup, inference := .introduce, justification := .physicalPrinciple }, { id := .stateLoopCalculation, premises := [], conclusion := .loopCalculation, inference := .computation, justification := .deferredCalculation }, { id := .stateResummationCalculation, premises := [], conclusion := .resummationCalculation, inference := .computation, justification := .deferredCalculation }, { id := .stateUnitarityCalculation, premises := [], conclusion := .unitarityCalculation, inference := .computation, justification := .deferredCalculation }, { id := .deriveLoopIntegral, premises := [.pdsSetup, .loopCalculation], conclusion := .loopIntegral, inference := .computation, justification := .paperDerivation }, { id := .retainPDSLoopFormula, premises := [.pdsSetup, .loopCalculation], conclusion := .loopFormula, inference := .logicalComposition, justification := .paperDerivation }, { id := .derivePDSAmplitude, premises := [.pdsSetup, .loopIntegral, .resummationCalculation], conclusion := .amplitude, inference := .computation, justification := .paperDerivation }, { id := .retainPDSAmplitudeFormula, premises := [.pdsSetup, .loopIntegral, .resummationCalculation], conclusion := .amplitudeFormula, inference := .logicalComposition, justification := .paperDerivation }, { id := .deriveUnitarity, premises := [.amplitude, .amplitudeFormula, .unitarityCalculation], conclusion := .unitarity, inference := .logicalComposition, justification := .paperDerivation }, { id := .stateEffectiveRangeMatching, premises := [], conclusion := .rangeMatching, inference := .introduce, justification := .importedResult }, { id := .imposePhysicalScaleIndependence, premises := [], conclusion := .scaleRequirement, inference := .introduce, justification := .physicalPrinciple }, { id := .stateRGCalculation, premises := [], conclusion := .rgCalculation, inference := .computation, justification := .deferredCalculation }, { id := .deriveBetaFunctions, premises := [.amplitude, .rangeMatching, .scaleRequirement, .rgCalculation], conclusion := .betaFunctions, inference := .computation, justification := .paperDerivation }, { id := .deriveC0C2RGControl, premises := [.amplitude, .rangeMatching, .scaleRequirement, .rgCalculation], conclusion := .c0C2RGControl, inference := .computation, justification := .paperDerivation }, { id := .deriveFullScaleIndependence, premises := [.amplitude, .rangeMatching, .scaleRequirement, .rgCalculation], conclusion := .fullScaleIndependence, inference := .logicalComposition, justification := .paperDerivation }, { id := .stateNaturalMSRegime, premises := [], conclusion := .naturalMSRegime, inference := .introduce, justification := .controlledApproximation }, { id := .stateLargeLengthMSRegime, premises := [], conclusion := .largeLengthMSRegime, inference := .introduce, justification := .controlledApproximation }, { id := .stateNaturalMSCalculation, premises := [], conclusion := .naturalMSCalculation, inference := .computation, justification := .deferredCalculation }, { id := .stateLargeLengthMSCalculation, premises := [], conclusion := .largeLengthMSCalculation, inference := .computation, justification := .deferredCalculation }, { id := .deriveNaturalMSValidity, premises := [.naturalMSRegime, .naturalMSCalculation], conclusion := .naturalMSValidity, inference := .computation, justification := .paperDerivation }, { id := .deriveLargeLengthMSWindow, premises := [.largeLengthMSRegime, .largeLengthMSCalculation], conclusion := .largeLengthMSWindow, inference := .logicalComposition, justification := .paperDerivation }, { id := .deriveLargeLengthMSRestriction, premises := [.largeLengthMSRegime, .largeLengthMSCalculation], conclusion := .largeLengthMSRestriction, inference := .logicalComposition, justification := .paperDerivation }, { id := .stateScalingSetup, premises := [], conclusion := .scalingSetup, inference := .introduce, justification := .controlledApproximation }, { id := .stateScalingCalculation, premises := [], conclusion := .scalingCalculation, inference := .computation, justification := .deferredCalculation }, { id := .deriveMixedExpansion, premises := [.scalingSetup, .scalingCalculation], conclusion := .mixedExpansion, inference := .computation, justification := .paperDerivation }, { id := .deriveAmplitudeExpansion, premises := [.scalingSetup, .scalingCalculation], conclusion := .amplitudeExpansion, inference := .computation, justification := .paperDerivation }, { id := .realizeSharedPowerCounting, premises := [.mixedExpansion], conclusion := .sharedPowerCounting, inference := .transport, justification := .paperDerivation }, { id := .statePionSetup, premises := [.mixedExpansion], conclusion := .pionSetup, inference := .introduce, justification := .controlledApproximation }, { id := .statePionCalculation, premises := [], conclusion := .pionCalculation, inference := .computation, justification := .deferredCalculation }, { id := .derivePotentialPionOrder, premises := [.pionSetup, .pionCalculation], conclusion := .potentialPion, inference := .computation, justification := .paperDerivation }, { id := .deriveRadiationPionAbsence, premises := [.pionSetup, .pionCalculation], conclusion := .radiationPionAbsence, inference := .computation, justification := .paperDerivation }, { id := .deriveLogarithmicDependence, premises := [.pionSetup, .pionCalculation], conclusion := .logarithmicScaleDependence, inference := .computation, justification := .paperDerivation }, { id := .requireD2Counterterm, premises := [.pionSetup, .pionCalculation], conclusion := .d2Required, inference := .logicalComposition, justification := .paperDerivation }, { id := .deriveD2Unsuppressed, premises := [.pionSetup, .pionCalculation], conclusion := .d2Unsuppressed, inference := .computation, justification := .paperDerivation }, { id := .derivePionInclusiveRGControl, premises := [.pionSetup, .pionCalculation], conclusion := .pionInclusiveRGControl, inference := .computation, justification := .paperDerivation }, { id := .deriveSubleadingCompleteness, premises := [.pionSetup, .pionCalculation], conclusion := .subleadingComplete, inference := .logicalComposition, justification := .paperDerivation }, { id := .excludeWeinbergCounting, premises := [.pionSetup, .d2Required, .d2Unsuppressed], conclusion := .weinbergFailure, inference := .obstruction, justification := .paperDerivation }, { id := .stateScaleCancellation, premises := [], conclusion := .scaleCalculation, inference := .computation, justification := .deferredCalculation }, { id := .deriveFullPionScaleIndependence, premises := [.pionInclusiveRGControl, .subleadingComplete, .scaleCalculation], conclusion := .fullPionScaleIndependence, inference := .logicalComposition, justification := .paperDerivation }, { id := .deriveTruncatedScaleIndependence, premises := [.pionInclusiveRGControl, .subleadingComplete, .scaleCalculation], conclusion := .truncatedScaleIndependence, inference := .logicalComposition, justification := .paperDerivation }, { id := .deriveHigherOrderResidual, premises := [.pionInclusiveRGControl, .subleadingComplete, .scaleCalculation], conclusion := .higherOrderResidual, inference := .logicalComposition, justification := .paperDerivation }, { id := .stateFitSetup, premises := [], conclusion := .fitSetup, inference := .introduce, justification := .importedResult }, { id := .stateFitCalculation, premises := [], conclusion := .fitCalculation, inference := .computation, justification := .deferredCalculation }, { id := .deriveExpectedCouplings, premises := [.subleadingComplete, .fitSetup, .fitCalculation], conclusion := .expectedCouplings, inference := .evidentialSupport, justification := .paperDerivation }, { id := .deriveC0D2Combination, premises := [.subleadingComplete, .fitSetup, .fitCalculation], conclusion := .c0D2Combination, inference := .computation, justification := .paperDerivation }, { id := .stateC0D2CombinationInterpretation, premises := [], conclusion := .c0D2Interpretation, inference := .introduce, justification := .interpretiveInference }, { id := .interpretC0D2IndividualValues, premises := [.c0D2Combination, .c0D2Interpretation], conclusion := .c0D2IndividualMeaning, inference := .interpretation, justification := .interpretiveInference }, { id := .derivePhaseAgreement, premises := [.subleadingComplete, .fitSetup, .fitCalculation], conclusion := .phaseAgreement, inference := .evidentialSupport, justification := .paperDerivation }, { id := .stateValidityExpectation, premises := [], conclusion := .validityExpectation, inference := .introduce, justification := .authorExpectation }, { id := .inferValiditySuggestion, premises := [.expectedCouplings, .validityExpectation], conclusion := .validitySuggestion, inference := .interpretation, justification := .interpretiveInference }, { id := .deriveLargeRatio, premises := [.subleadingComplete, .fitSetup, .fitCalculation], conclusion := .largeRatio, inference := .evidentialSupport, justification := .paperDerivation }, { id := .stateTruncationAssessment, premises := [], conclusion := .truncationAssessment, inference := .obstruction, justification := .controlledApproximation }, { id := .excludeControlledNeglectedTerms, premises := [.largeRatio, .truncationAssessment], conclusion := .uncontrolledNeglectedTerms, inference := .obstruction, justification := .paperDerivation }, { id := .stateCoupledSetup, premises := [], conclusion := .coupledSetup, inference := .introduce, justification := .controlledApproximation }, { id := .stateCoupledCalculation, premises := [], conclusion := .coupledCalculation, inference := .computation, justification := .deferredCalculation }, { id := .retainCoupledSMatrixFormula, premises := [.coupledSetup, .coupledCalculation], conclusion := .coupledSMatrixFormula, inference := .logicalComposition, justification := .paperDerivation }, { id := .deriveLeadingSOnly, premises := [.coupledSetup, .coupledCalculation], conclusion := .leadingSOnly, inference := .computation, justification := .paperDerivation }, { id := .deriveZeroMixingAndDWave, premises := [.coupledSetup, .coupledCalculation, .coupledSMatrixFormula, .leadingSOnly], conclusion := .zeroMixingAndDWave, inference := .computation, justification := .paperDerivation }, { id := .deriveSubleadingSPhase, premises := [.coupledSetup, .coupledCalculation], conclusion := .subleadingSPhase, inference := .computation, justification := .paperDerivation }, { id := .recordMixedObservableOrders, premises := [.coupledSetup, .coupledCalculation], conclusion := .mixedObservableOrders, inference := .introduce, justification := .controlledApproximation }, { id := .recordDeferredCoupledFormula, premises := [.coupledSetup, .coupledCalculation], conclusion := .deferredCoupledFormula, inference := .introduce, justification := .openObligation }, { id := .recordCoupledSFit, premises := [.coupledSetup, .coupledCalculation], conclusion := .fittedSPhase, inference := .evidentialSupport, justification := .importedResult }, { id := .deriveParameterFreePredictions, premises := [.coupledSetup, .coupledCalculation, .fittedSPhase], conclusion := .parameterFreePredictions, inference := .logicalComposition, justification := .paperDerivation } ] def stepSources : StepId → List SourceRef | .statePDSSetup => [arxivPage "2-3" "choose the pionless PDS setup" .reconstructedStep] | .stateLoopCalculation => [arxivPage "3" "supply the PDS loop calculation" .reconstructedStep] | .stateResummationCalculation => [arxivPage "3" "supply the bubble-chain resummation" .reconstructedStep] | .stateUnitarityCalculation => [arxivPage "3" "supply the elastic domain and inverse-amplitude observable normalization" .reconstructedStep] | .deriveLoopIntegral => [arxivPage "3" "subtract the D=3 pole" .reconstructedStep] | .retainPDSLoopFormula => [arxivPage "3" "retain the printed equation (4) PDS loop formula" .directStatement] | .derivePDSAmplitude => [arxivPage "3" "sum the bubble chain" .reconstructedStep] | .retainPDSAmplitudeFormula => [arxivPage "3" "retain the printed equation (5) amplitude formula" .directStatement] | .deriveUnitarity => [arxivPage "3" "use the retained bubble formula to derive unitarity and the contact phase function" .reconstructedStep] | .stateEffectiveRangeMatching => [arxivPage "3-4" "interpret the finite nonzero-a effective-range expansion as a nonvacuous positive-threshold coefficient limit" .reconstructedStep] | .imposePhysicalScaleIndependence => [arxivPage "4" "require cancellation of mu dependence" .reconstructedStep] | .stateRGCalculation => [arxivPage "3-4" "calibrate contact coefficient families against the same effective-range observable behind equations (7)-(11)" .reconstructedStep] | .deriveBetaFunctions => [arxivPage "4" "identify exact beta functions" .reconstructedStep] | .deriveC0C2RGControl => [arxivPage "4" "solve equations (9)-(10) to obtain the displayed C0(mu), C2(mu) values in equation (11)" .reconstructedStep] | .deriveFullScaleIndependence => [arxivPage "4" "cancel amplitude scale dependence" .reconstructedStep] | .stateNaturalMSRegime => [arxivPage "4" "select natural scattering length, mu=0, and p/Lambda small" .reconstructedStep] | .stateLargeLengthMSRegime => [arxivPage "4" "select very large scattering length at mu=0" .reconstructedStep] | .stateNaturalMSCalculation => [arxivPage "4" "supply the ordinary p/Lambda power-counting calculation" .reconstructedStep] | .stateLargeLengthMSCalculation => [arxivPage "4" "supply the large-coefficient restriction calculation" .reconstructedStep] | .deriveNaturalMSValidity => [arxivPage "4" "obtain ordinary MS counting in the natural regime" .reconstructedStep] | .deriveLargeLengthMSWindow => [arxivPage "4" "identify p |a| as the restrictive expansion parameter" .reconstructedStep] | .deriveLargeLengthMSRestriction => [arxivPage "4" "record the small ordinary-MS momentum range" .reconstructedStep] | .stateScalingSetup => [arxivPage "4" "take large a and mu of order p; realize scale comparison with one fixed c >= 1 and p > 0, p/c <= mu <= c p" .reconstructedStep] | .stateScalingCalculation => [arxivPage "4-5" "supply loop and coupling scaling" .reconstructedStep] | .deriveMixedExpansion => [arxivPage "4-5" "separate C0 resummation from corrections" .reconstructedStep] | .deriveAmplitudeExpansion => [arxivPage "5" "derive equations (12)-(13)" .reconstructedStep] | .realizeSharedPowerCounting => [arxivPage "4-5" "transport to neutral mixed power counting" .reconstructedStep] | .statePionSetup => [arxivPage "5" "take p of order m_pi" .reconstructedStep] | .statePionCalculation => [arxivPage "5-7" "supply equations (14)-(18)" .reconstructedStep] | .derivePotentialPionOrder => [arxivPage "5" "count potential pion at p^0" .reconstructedStep] | .deriveRadiationPionAbsence => [arxivPage "6" "exclude radiation pions at p^0" .reconstructedStep] | .deriveLogarithmicDependence => [arxivPage "6" "extract logarithmic mu dependence" .reconstructedStep] | .requireD2Counterterm => [arxivPage "6" "include D2 m_pi^2" .reconstructedStep] | .deriveD2Unsuppressed => [arxivPage "6, footnote 3" "compare D2 with the one-pion-exchange contribution" .reconstructedStep] | .derivePionInclusiveRGControl => [arxivPage "7" "apply the computed-order pion-inclusive C0 and C2 beta functions and the inhomogeneous D2 equation (18), keeping the retained real flow separate from exact pionless running" .reconstructedStep] | .deriveSubleadingCompleteness => [arxivPage "5-7" "collect all five A0 subgraphs" .reconstructedStep] | .excludeWeinbergCounting => [arxivPage "6, footnote 3" "contrast the same-order unsuppressed D2 contribution with Weinberg ordering" .reconstructedStep] | .stateScaleCancellation => [arxivPage "7" "supply cancellation using the pion-inclusive RG equations" .reconstructedStep] | .deriveFullPionScaleIndependence => [arxivPage "7" "identify the full amplitude as mu independent" .reconstructedStep] | .deriveTruncatedScaleIndependence => [arxivPage "7" "truncate through p^0" .reconstructedStep] | .deriveHigherOrderResidual => [arxivPage "7" "assign residual dependence to higher orders" .reconstructedStep] | .stateFitSetup => [arxivPage "7" "fit three parameters through 200 MeV" .reconstructedStep] | .stateFitCalculation => [arxivPage "7-8" "supply the numerical fit and Figure 3" .reconstructedStep] | .deriveExpectedCouplings => [arxivPage "7" "compare fitted and expected sizes" .reconstructedStep] | .deriveC0D2Combination => [arxivPage "7" "retain the C0 + D2 m_pi^2 amplitude combination through the computed order" .reconstructedStep] | .stateC0D2CombinationInterpretation => [arxivPage "7" "retain the authors' parenthetical interpretation of that combination" .reconstructedStep] | .interpretC0D2IndividualValues => [arxivPage "7" "use the combination-only amplitude to qualify individual fit values" .reconstructedStep] | .derivePhaseAgreement => [arxivPage "7-8" "compare fitted phase shift with data" .reconstructedStep] | .stateValidityExpectation => [arxivPage "7" "retain the authors' qualified expectation" .reconstructedStep] | .inferValiditySuggestion => [arxivPage "7" "interpret the expectation as channel-scoped support" .reconstructedStep] | .deriveLargeRatio => [arxivPage "8" "evaluate A0/A-1 above 100 MeV" .reconstructedStep] | .stateTruncationAssessment => [arxivPage "8" "assess omitted quadratic corrections" .reconstructedStep] | .excludeControlledNeglectedTerms => [arxivPage "8" "record difficulty justifying the approximation" .reconstructedStep] | .stateCoupledSetup => [arxivPage "8-9" "select the triplet coupled channel" .reconstructedStep] | .stateCoupledCalculation => [arxivPage "8-9" "supply the stated coupled-channel outputs" .reconstructedStep] | .retainCoupledSMatrixFormula => [arxivPage "8" "retain the printed S - 1 = i p M A / (2 pi) phase matrix" .directStatement] | .deriveLeadingSOnly => [arxivPage "8" "set A02, A20, and A22 to zero" .reconstructedStep] | .deriveZeroMixingAndDWave => [arxivPage "8" "apply the displayed S-matrix relation to infer epsilon1=delta2=0" .reconstructedStep] | .deriveSubleadingSPhase => [arxivPage "9" "retain subleading order for delta0" .reconstructedStep] | .recordMixedObservableOrders => [arxivPage "9" "retain leading order for epsilon1 and delta2" .reconstructedStep] | .recordDeferredCoupledFormula => [arxivPage "8-9" "record future-publication status" .reconstructedStep] | .recordCoupledSFit => [arxivPage "9" "fit A00 parameters to delta0" .reconstructedStep] | .deriveParameterFreePredictions => [arxivPage "9" "remove further parameters from epsilon1 and delta2" .reconstructedStep] def steps : List (ArgumentStep StepId ClaimId) := rawSteps.map fun step => { step with sources := stepSources step.id } inductive RouteId where | pionlessPDS | minimalSubtractionScope | largeLengthPowerCounting | explicitPions | scaleCancellation | singletFit | coupledChannel deriving DecidableEq, Repr inductive RouteKind where | exactPionlessConstruction | minimalSubtractionScopeContrast | mixedPowerCounting | subleadingPionCalculation | renormalizationScaleAccounting | empiricalFitWithValidityWarning | mixedOrderCoupledPrediction deriving DecidableEq, Repr def pionlessPDSRoute : ArgumentRoute RouteId RouteKind StepId ClaimId := { id := .pionlessPDS kind := .exactPionlessConstruction dependsOn := [] steps := [.statePDSSetup, .stateLoopCalculation, .stateResummationCalculation, .stateUnitarityCalculation, .deriveLoopIntegral, .retainPDSLoopFormula, .derivePDSAmplitude, .retainPDSAmplitudeFormula, .deriveUnitarity, .stateEffectiveRangeMatching, .imposePhysicalScaleIndependence, .stateRGCalculation, .deriveBetaFunctions, .deriveC0C2RGControl, .deriveFullScaleIndependence] outputs := [.loopFormula, .amplitudeFormula, .amplitude, .unitarity, .betaFunctions, .c0C2RGControl, .fullScaleIndependence] } def minimalSubtractionScopeRoute : ArgumentRoute RouteId RouteKind StepId ClaimId := { id := .minimalSubtractionScope kind := .minimalSubtractionScopeContrast dependsOn := [] steps := [.stateNaturalMSRegime, .stateLargeLengthMSRegime, .stateNaturalMSCalculation, .stateLargeLengthMSCalculation, .deriveNaturalMSValidity, .deriveLargeLengthMSWindow, .deriveLargeLengthMSRestriction] outputs := [.naturalMSValidity, .largeLengthMSWindow, .largeLengthMSRestriction] } def largeLengthPowerCountingRoute : ArgumentRoute RouteId RouteKind StepId ClaimId := { id := .largeLengthPowerCounting kind := .mixedPowerCounting dependsOn := [] steps := [.stateScalingSetup, .stateScalingCalculation, .deriveMixedExpansion, .deriveAmplitudeExpansion, .realizeSharedPowerCounting] outputs := [.mixedExpansion, .amplitudeExpansion, .sharedPowerCounting] } def explicitPionsRoute : ArgumentRoute RouteId RouteKind StepId ClaimId := { id := .explicitPions kind := .subleadingPionCalculation dependsOn := [.largeLengthPowerCounting] steps := [.statePionSetup, .statePionCalculation, .derivePotentialPionOrder, .deriveRadiationPionAbsence, .deriveLogarithmicDependence, .requireD2Counterterm, .deriveD2Unsuppressed, .derivePionInclusiveRGControl, .deriveSubleadingCompleteness, .excludeWeinbergCounting] outputs := [.potentialPion, .radiationPionAbsence, .logarithmicScaleDependence, .d2Required, .d2Unsuppressed, .pionInclusiveRGControl, .subleadingComplete, .weinbergFailure] } def scaleCancellationRoute : ArgumentRoute RouteId RouteKind StepId ClaimId := { id := .scaleCancellation kind := .renormalizationScaleAccounting dependsOn := [.explicitPions] steps := [.stateScaleCancellation, .deriveFullPionScaleIndependence, .deriveTruncatedScaleIndependence, .deriveHigherOrderResidual] outputs := [.fullPionScaleIndependence, .truncatedScaleIndependence, .higherOrderResidual] } def singletFitRoute : ArgumentRoute RouteId RouteKind StepId ClaimId := { id := .singletFit kind := .empiricalFitWithValidityWarning dependsOn := [.explicitPions] steps := [.stateFitSetup, .stateFitCalculation, .deriveExpectedCouplings, .deriveC0D2Combination, .stateC0D2CombinationInterpretation, .interpretC0D2IndividualValues, .derivePhaseAgreement, .stateValidityExpectation, .inferValiditySuggestion, .deriveLargeRatio, .stateTruncationAssessment, .excludeControlledNeglectedTerms] outputs := [.expectedCouplings, .c0D2Combination, .c0D2IndividualMeaning, .phaseAgreement, .validitySuggestion, .largeRatio, .uncontrolledNeglectedTerms] } def coupledChannelRoute : ArgumentRoute RouteId RouteKind StepId ClaimId := { id := .coupledChannel kind := .mixedOrderCoupledPrediction dependsOn := [] steps := [.stateCoupledSetup, .stateCoupledCalculation, .retainCoupledSMatrixFormula, .deriveLeadingSOnly, .deriveZeroMixingAndDWave, .deriveSubleadingSPhase, .recordMixedObservableOrders, .recordDeferredCoupledFormula, .recordCoupledSFit, .deriveParameterFreePredictions] outputs := [.coupledSMatrixFormula, .leadingSOnly, .zeroMixingAndDWave, .subleadingSPhase, .mixedObservableOrders, .deferredCoupledFormula, .parameterFreePredictions] } def routes : List (ArgumentRoute RouteId RouteKind StepId ClaimId) := [pionlessPDSRoute, minimalSubtractionScopeRoute, largeLengthPowerCountingRoute, explicitPionsRoute, scaleCancellationRoute, singletFitRoute, coupledChannelRoute] def argument : PaperArgument ClaimId StepId Atom := { title := "Kaplan, Savage, and Wise's new expansion for NN interactions (1998)" sources := [originalPaper "complete original article, arXiv v2 pp. 1-10" .directStatement] claims := claims steps := steps mainConclusion := .mixedExpansion } def routedArgument : RoutedArgument ClaimId StepId Atom RouteId RouteKind := { argument := argument routes := routes } theorem argument_wellFormed : argument.wellFormed = true := by rfl theorem argument_auditable : argument.auditable = true := by rfl theorem routes_wellFormed : routedArgument.wellFormed = true := by rfl theorem routes_have_exact_predecessor_graph : pionlessPDSRoute.dependsOn = [] ∧ minimalSubtractionScopeRoute.dependsOn = [] ∧ largeLengthPowerCountingRoute.dependsOn = [] ∧ explicitPionsRoute.dependsOn = [.largeLengthPowerCounting] ∧ scaleCancellationRoute.dependsOn = [.explicitPions] ∧ singletFitRoute.dependsOn = [.explicitPions] ∧ coupledChannelRoute.dependsOn = [] := by repeat' constructor /-- These source-graph nodes have no predecessor claims. This does not assert logical independence or require each node as an external physical hypothesis; the C0/D2 interpretation is realized by a derived conditional theorem. -/ theorem calculation_and_interpretation_contracts_have_no_source_predecessors : argument.stepRule? .stateLoopCalculation = some ([], .loopCalculation) ∧ argument.stepRule? .stateResummationCalculation = some ([], .resummationCalculation) ∧ argument.stepRule? .stateUnitarityCalculation = some ([], .unitarityCalculation) ∧ argument.stepRule? .stateRGCalculation = some ([], .rgCalculation) ∧ argument.stepRule? .stateNaturalMSCalculation = some ([], .naturalMSCalculation) ∧ argument.stepRule? .stateLargeLengthMSCalculation = some ([], .largeLengthMSCalculation) ∧ argument.stepRule? .stateScalingCalculation = some ([], .scalingCalculation) ∧ argument.stepRule? .statePionCalculation = some ([], .pionCalculation) ∧ argument.stepRule? .stateScaleCancellation = some ([], .scaleCalculation) ∧ argument.stepRule? .stateFitSetup = some ([], .fitSetup) ∧ argument.stepRule? .stateFitCalculation = some ([], .fitCalculation) ∧ argument.stepRule? .stateC0D2CombinationInterpretation = some ([], .c0D2Interpretation) ∧ argument.stepRule? .stateValidityExpectation = some ([], .validityExpectation) ∧ argument.stepRule? .stateTruncationAssessment = some ([], .truncationAssessment) ∧ argument.stepRule? .stateCoupledCalculation = some ([], .coupledCalculation) := by repeat' constructor theorem dependent_result_steps_apply_exact_semantic_inputs : argument.stepRule? .deriveLoopIntegral = some ([.pdsSetup, .loopCalculation], .loopIntegral) ∧ argument.stepRule? .retainPDSLoopFormula = some ([.pdsSetup, .loopCalculation], .loopFormula) ∧ argument.stepRule? .derivePDSAmplitude = some ([.pdsSetup, .loopIntegral, .resummationCalculation], .amplitude) ∧ argument.stepRule? .retainPDSAmplitudeFormula = some ([.pdsSetup, .loopIntegral, .resummationCalculation], .amplitudeFormula) ∧ argument.stepRule? .deriveUnitarity = some ([.amplitude, .amplitudeFormula, .unitarityCalculation], .unitarity) ∧ argument.stepRule? .deriveBetaFunctions = some ([.amplitude, .rangeMatching, .scaleRequirement, .rgCalculation], .betaFunctions) ∧ argument.stepRule? .statePionSetup = some ([.mixedExpansion], .pionSetup) ∧ argument.stepRule? .excludeWeinbergCounting = some ([.pionSetup, .d2Required, .d2Unsuppressed], .weinbergFailure) ∧ argument.stepRule? .deriveFullPionScaleIndependence = some ([.pionInclusiveRGControl, .subleadingComplete, .scaleCalculation], .fullPionScaleIndependence) ∧ argument.stepRule? .deriveExpectedCouplings = some ([.subleadingComplete, .fitSetup, .fitCalculation], .expectedCouplings) ∧ argument.stepRule? .interpretC0D2IndividualValues = some ([.c0D2Combination, .c0D2Interpretation], .c0D2IndividualMeaning) ∧ argument.stepRule? .inferValiditySuggestion = some ([.expectedCouplings, .validityExpectation], .validitySuggestion) ∧ argument.stepRule? .excludeControlledNeglectedTerms = some ([.largeRatio, .truncationAssessment], .uncontrolledNeglectedTerms) ∧ argument.stepRule? .retainCoupledSMatrixFormula = some ([.coupledSetup, .coupledCalculation], .coupledSMatrixFormula) ∧ argument.stepRule? .deriveZeroMixingAndDWave = some ([.coupledSetup, .coupledCalculation, .coupledSMatrixFormula, .leadingSOnly], .zeroMixingAndDWave) ∧ argument.stepRule? .deriveParameterFreePredictions = some ([.coupledSetup, .coupledCalculation, .fittedSPhase], .parameterFreePredictions) := by repeat' constructor theorem mixed_expansion_retains_controlled_regime_and_deferred_scaling : argument.ClaimReliesOnJustification .mixedExpansion .controlledApproximation ∧ argument.ClaimReliesOnJustification .mixedExpansion .deferredCalculation := by decide theorem large_length_ms_restriction_retains_scope_and_calculation : argument.ClaimReliesOnJustification .largeLengthMSRestriction .controlledApproximation ∧ argument.ClaimReliesOnJustification .largeLengthMSRestriction .deferredCalculation ∧ argument.ClaimReliesOnStep .largeLengthMSWindow .stateLargeLengthMSCalculation := by decide theorem fit_validity_retains_author_expectation : argument.ClaimReliesOnJustification .validitySuggestion .authorExpectation := by decide theorem fit_validity_uses_expected_couplings_and_interpretive_bridge : argument.ClaimReliesOnStep .validitySuggestion .deriveExpectedCouplings ∧ argument.ClaimReliesOnStep .validitySuggestion .stateValidityExpectation := by decide theorem fit_c0_d2_meaning_depends_on_combination_scope : argument.ClaimReliesOnStep .c0D2IndividualMeaning .deriveC0D2Combination ∧ argument.ClaimReliesOnStep .c0D2IndividualMeaning .stateFitCalculation ∧ argument.ClaimReliesOnJustification .c0D2IndividualMeaning .interpretiveInference := by decide theorem high_momentum_warning_retains_approximation_assessment : argument.ClaimReliesOnJustification .uncontrolledNeglectedTerms .controlledApproximation := by decide theorem weinberg_failure_depends_on_required_same_order_d2 : argument.ClaimReliesOnStep .weinbergFailure .requireD2Counterterm ∧ argument.ClaimReliesOnStep .weinbergFailure .deriveD2Unsuppressed := by decide theorem scale_cancellation_depends_on_pion_inclusive_rg_control : argument.ClaimReliesOnStep .fullPionScaleIndependence .derivePionInclusiveRGControl ∧ argument.ClaimReliesOnStep .truncatedScaleIndependence .derivePionInclusiveRGControl ∧ argument.ClaimReliesOnStep .higherOrderResidual .derivePionInclusiveRGControl := by decide theorem coupled_predictions_retain_deferred_and_mixed_order_status : argument.ClaimReliesOnJustification .deferredCoupledFormula .openObligation ∧ argument.ClaimReliesOnJustification .parameterFreePredictions .deferredCalculation := by decide theorem coupled_zero_phases_depend_on_displayed_s_matrix_formula : argument.ClaimReliesOnStep .zeroMixingAndDWave .retainCoupledSMatrixFormula ∧ argument.ClaimReliesOnStep .zeroMixingAndDWave .deriveLeadingSOnly := by decide end PhysicsLogic.Papers.KaplanSavageWise1998