import PhysicsLogic.Logic.Route /-! # Bethe 1949 Source Map Auxiliary provenance and paper order for `PhysicsLogic.Papers.Bethe1949`. The graph records no physical premise or conclusion by itself. -/ set_option autoImplicit false namespace PhysicsLogic.Papers.Bethe1949 open PhysicsLogic.Logic inductive Atom where | neutralComparisonSetup | neutralComparisonCalculation | neutralRadialFormulaCalculation | neutralRadialFormulaReadout | exactNeutralComparison | effectiveRangeApproximationSetup | effectiveRangeReductionCalculation | effectiveRangeIdentificationBridge | neutralEffectiveRangeLaw | neutralCrossSectionSetup | neutralCrossSectionCalculation | neutralCrossSectionTruncationInterpretation | neutralCrossSectionAssessment | equationSeventeenCrossSectionFormula | higherOrderCalculation | curvatureDiagnosticInterpretation | shapeSensitivityInterpretation | accuracyAndShapeScope | tripletExtractionSetup | tripletExtractionCalculation | singletRangeDataLimitation | singletRangeBorrowingBridge | singletRangeAssessment | tripletExtractionResult | coulombComparisonSetup | coulombComparisonCalculation | coulombSourceFormula | coulombRangeReplacementCalculation | coulombIdentificationBridge | coulombEffectiveRangeLaw | coulombNeutralizationCalculation | coulombNeutralizationResult | coulombThresholdSetup | coulombThresholdRegularity | coulombThresholdResult | protonEmpiricalSetup | protonFitCalculation | highEnergyAssessment | protonEmpiricalResult | chargeComparisonSetup | chargeWeightedCalculation | chargeWeightedResult | chargeReadoutCalculation | chargeEstimateResult | chargeComparisonCalculation | chargeDependenceInterpretation | chargeComparisonResult | chargeShapeExpectation | chargeShapeErrorBudget | chargeShapeResult | paperScopeQualifications | completeScopedResult deriving DecidableEq, Repr inductive ClaimId where | neutralSetup | neutralCalculation | neutralFormulaCalculation | neutralFormulaReadout | neutralResult | approximationSetup | reductionCalculation | effectiveRangeIdentification | effectiveRangeResult | crossSectionSetup | crossSectionCalculation | crossSectionInterpretation | crossSectionResult | crossSectionFormula | correctionCalculation | curvatureDiagnostic | shapeInterpretation | accuracyResult | tripletSetup | tripletCalculation | singletLimitation | singletBorrowing | singletAssessment | tripletResult | coulombSetup | coulombCalculation | coulombSourceFormula | coulombRangeReplacement | coulombIdentification | coulombResult | coulombNeutralizationCalculation | coulombNeutralizationResult | coulombThresholdSetup | coulombThresholdRegularity | coulombThresholdResult | protonSetup | protonFit | highEnergyAssessment | protonResult | chargeSetup | chargeWeightedCalculation | chargeWeightedResult | chargeReadoutCalculation | chargeEstimateResult | chargeCalculation | chargeInterpretation | chargeResult | chargeShapeExpectation | chargeShapeErrorBudget | chargeShapeResult | scopeQualifications | completeResult deriving DecidableEq, Repr inductive StepId where | stateNeutralSetup | supplyNeutralCalculation | supplyNeutralRadialFormulaCalculation | deriveNeutralRadialFormulaReadout | deriveNeutralResult | stateApproximationSetup | supplyReductionCalculation | supplyEffectiveRangeIdentification | deriveEffectiveRangeResult | stateCrossSectionSetup | supplyCrossSectionCalculation | supplyCrossSectionInterpretation | deriveCrossSectionAssessment | deriveCrossSectionFormula | supplyCorrectionCalculation | interpretCurvatureDiagnostic | interpretShapeSensitivity | deriveAccuracyResult | stateTripletSetup | supplyTripletCalculation | deriveTripletResult | stateSingletLimitation | supplySingletBorrowing | deriveSingletAssessment | stateCoulombSetup | supplyCoulombCalculation | deriveCoulombSourceFormula | supplyCoulombRangeReplacement | supplyCoulombIdentification | deriveCoulombResult | supplyCoulombNeutralization | deriveCoulombNeutralization | stateCoulombThresholdSetup | supplyCoulombThresholdRegularity | deriveCoulombThreshold | stateProtonSetup | supplyProtonFit | assessHighEnergyData | deriveProtonResult | stateChargeSetup | supplyChargeWeightedCalculation | deriveChargeWeightedResult | supplyChargeReadoutCalculation | deriveChargeEstimate | supplyChargeCalculation | interpretChargeDependence | deriveChargeResult | stateChargeShapeExpectation | supplyChargeShapeErrorBudget | deriveChargeShapeAssessment | stateScopeQualifications | assembleCompleteResult deriving DecidableEq, Repr inductive RouteId where | neutralComparison | effectiveRangeReduction | neutralCrossSection | accuracyAndShape | tripletExtraction | singletRangeQualification | coulombComparison | coulombTheory | coulombNeutralization | coulombThreshold | protonExperiment | chargeWeightedComparison | chargeEstimate | chargeComparison | chargeShapeAssessment | completeScopedResult deriving DecidableEq, Repr inductive RouteKind where | exactFiniteRangeComparison | controlledLowEnergyReduction | sWaveCrossSectionUnitarity | higherOrderErrorAndShapeScope | boundStateDataExtraction | singletRangeDataQualification | exactChargedWaveComparison | coulombModifiedComparison | separateCoulombRemovalApproximation | nonresonantCoulombThreshold | empiricalLowAndHighEnergyAssessment | exactWeightedChargeComparison | controlledChargeReadout | counterfactualInteractionComparison | conditionalShapeExtrapolation | completePaperAssessment deriving DecidableEq, Repr def originalPaper (locator description : String) (relation : SourceRelation := .directStatement) : SourceRef := { work := "H. A. Bethe, Theory of the Effective Range in Nuclear Scattering, Physical Review 76 (1949), 38-50" locator := locator ++ ": " ++ description relation := relation } def page (number description : String) (relation : SourceRelation := .directStatement) : SourceRef := originalPaper ("journal page " ++ number) description relation def pageRange (pages description : String) (relation : SourceRelation := .directStatement) : SourceRef := originalPaper ("journal pages " ++ pages) description relation def equation (label pageNumber description : String) (relation : SourceRelation := .directStatement) : SourceRef := originalPaper ("equation " ++ label ++ ", journal page " ++ pageNumber) description relation def paperClaim (id : ClaimId) (atom : Atom) (role : ClaimRole) (sources : List SourceRef) : Claim ClaimId Atom := { id := id, formula := .atom atom, role := role, sources := sources } def claims : List (Claim ClaimId Atom) := [ paperClaim .neutralSetup .neutralComparisonSetup .setupPremise [pageRange "38-39" "select finite-range neutral S-wave scattering, normalized radial waves, and asymptotic comparison waves"], paperClaim .neutralCalculation .neutralComparisonCalculation .intermediate [pageRange "39-40" "identify the selected boundary, wave-number difference, and overlap readouts with actual phase differences and the radial integral" .reconstructedStep], paperClaim .neutralFormulaCalculation .neutralRadialFormulaCalculation .intermediate [pageRange "39-40" "supply the free comparison waves, finite-radius identities (6) and (8), convergent overlap and boundary limit, and the exact range definitions" .reconstructedStep], paperClaim .neutralFormulaReadout .neutralRadialFormulaReadout .intermediate [equation "(7), (10), (11), (13)-(14)" "39-40" "retain the normalized comparison wave and its k cot(delta) readout, exact overlap identity, zero-energy scattering length, and energy-dependent/effective-range integrals"], paperClaim .neutralResult .exactNeutralComparison .mainConclusion [equation "(10)-(13)" "39" "obtain the exact comparison identity and its zero-energy specialization"], paperClaim .approximationSetup .effectiveRangeApproximationSetup .setupPremise [page "39" "inside the finite force range, take kr small and the potential energy large compared with the scattering energy"], paperClaim .reductionCalculation .effectiveRangeReductionCalculation .intermediate [equation "(14)-(16)" "39-40" "control the actual interior-wave replacement integral; its error propagates to the two-parameter phase approximation rather than an exact phase equality" .reconstructedStep], paperClaim .effectiveRangeIdentification .effectiveRangeIdentificationBridge .intermediate [equation "(14)-(16)" "39-40" "identify the calculated two-parameter expression with the paper's neutral effective-range phase law"], paperClaim .effectiveRangeResult .neutralEffectiveRangeLaw .mainConclusion [equation "(16)" "40" "reduce the neutral phase function to scattering length plus effective range"], paperClaim .crossSectionSetup .neutralCrossSectionSetup .setupPremise [page "40" "select the classical-energy neutral triplet point with strictly positive k squared, identify k squared with the square of its actual wave number, and identify the same-energy phase function with k cot delta"], paperClaim .crossSectionCalculation .neutralCrossSectionCalculation .intermediate [equation "(17)-(18)" "40" "insert the effective-range phase law into the S-wave cross section at the same physically identified wave number and phase shift, and tie the maximum to an actually zero numerical phase-function value" .reconstructedStep], paperClaim .crossSectionInterpretation .neutralCrossSectionTruncationInterpretation .intermediate [page "40" "retain Schwinger's warning that the next term is required near the cross-section maximum to preserve the permitted bound"], paperClaim .crossSectionResult .neutralCrossSectionAssessment .mainConclusion [equation "(17)-(18)" "40" "derive both printed cross-section forms, the numerical 4 pi divided by k squared bound, saturation if and only if the physical phase-shift cosine vanishes, and strict suppression for every nonzero phase"], paperClaim .crossSectionFormula .equationSeventeenCrossSectionFormula .intermediate [equation "(17)" "40" "retain both printed neutral S-wave cross-section forms: 4 pi sin squared delta divided by k squared and 4 pi divided by k squared plus the squared k cot delta phase function"], paperClaim .correctionCalculation .higherOrderCalculation .intermediate [pageRange "42-43" "expand the comparison and exact waves and evaluate the first shape-dependent correction" .reconstructedStep], paperClaim .curvatureDiagnostic .curvatureDiagnosticInterpretation .intermediate [page "43" "upward curvature would indicate a concentrated potential and downward curvature a long-tailed potential, but present deviations are not significant"], paperClaim .shapeInterpretation .shapeSensitivityInterpretation .intermediate [pageRange "41-43" "distinguish square-well and long-tail intrinsic-range implications while retaining that single-channel energy dependence does not resolve the potential shape"], paperClaim .accuracyResult .accuracyAndShapeScope .mainConclusion [equation "(33)-(36)" "42-43" "the shape coefficient is small and the two-parameter law is accurate in the declared energy range"], paperClaim .tripletSetup .tripletExtractionSetup .evidence [pageRange "40-41" "combine deuteron binding, free-proton scattering, and parahydrogen scattering data"], paperClaim .tripletCalculation .tripletExtractionCalculation .intermediate [equation "(19)-(27)" "40-41" "specialize the equations-(10)-(11) comparison identity to k^2 = -gamma^2 and equation (15)'s exp(-gamma r) comparison wave; its actual derivative at the origin derives equation (19)'s exact alpha = gamma - (1/2) gamma^2 rho(0,-epsilon), before the separate range replacement and measured-data extraction" .reconstructedStep], paperClaim .singletLimitation .singletRangeDataLimitation .evidence [page "41" "neutron-proton singlet data do not fix the range accurately"], paperClaim .singletBorrowing .singletRangeBorrowingBridge .intermediate [page "41" "retain separately both the approximate force-equality assumption and the borrowing of the proton-proton effective range for neutron-proton singlet scattering"], paperClaim .singletAssessment .singletRangeAssessment .mainConclusion [page "41" "combine the singlet-data limitation with distinct approximate force-equality and borrowed-range assumptions"], paperClaim .tripletResult .tripletExtractionResult .mainConclusion [equation "(27)" "41" "obtain the reported neutron-proton triplet effective range with stated uncertainties after the exact equation-(19) relation and separate controlled replacement"], paperClaim .coulombSetup .coulombComparisonSetup .setupPremise [equation "(37)-(41)" "43-44" "retain the two-proton reduced mass, actual repulsive radial term, positive scattering momentum, zero-energy reference, exterior matching, and a quantified range-to-Bohr-radius hierarchy"], paperClaim .coulombCalculation .coulombComparisonCalculation .intermediate [equation "(42)-(50)" "44-45" "supply the regular/irregular Coulomb basis, equation-(42) combination, common-log derivative expansion, integrated derivative comparison, and actual range readouts; special-function and boundary calculations remain explicit inputs" .reconstructedStep], paperClaim .coulombSourceFormula .coulombSourceFormula .intermediate [equation "(42)-(43), (47a), (50)-(51)" "44-45" "derive the relative nuclear phase, actual normalization and series function, same-radius logarithmic cancellation, and dimensionless f = D[-alpha' + k^2 rho(0,E)/2] before replacing the energy-dependent range" .reconstructedStep], paperClaim .coulombRangeReplacement .coulombRangeReplacementCalculation .intermediate [equation "(52)" "45" "supply an independent L1 overlap error for replacing the charged finite-energy overlap by its charged zero-energy value" .reconstructedStep], paperClaim .coulombIdentification .coulombIdentificationBridge .intermediate [equation "(51)-(52)" "45" "identify the controlled Coulomb expression as the modified effective-range approximation"], paperClaim .coulombResult .coulombEffectiveRangeLaw .mainConclusion [equation "(51)-(52)" "45" "obtain the Coulomb-modified two-parameter phase with its explicit energy-replacement error, not an exact equality"], paperClaim .coulombNeutralizationCalculation .coulombNeutralizationCalculation .intermediate [equation "(52)" "45" "separately control removal of Coulomb distortion from the zero-energy overlap while keeping the same nuclear potential" .reconstructedStep], paperClaim .coulombNeutralizationResult .coulombNeutralizationResult .mainConclusion [equation "(52)" "45" "the charged-to-neutral range error is separate from finite-energy replacement; their budgets add in the neutralized phase approximation, without supplying section-VII logarithmically weighted comparison integrals" .reconstructedStep], paperClaim .coulombThresholdSetup .coulombThresholdSetup .setupPremise [equation "(41), (51a)" "44-45" "select the actual k = 1/(D eta) threshold family and Coulomb-relative scattering realizations for a fixed nuclear potential" .reconstructedStep], paperClaim .coulombThresholdRegularity .coulombThresholdRegularity .setupPremise [page "45" "make explicit the threshold argument's additional regularity: a finite source intercept, the imported g limit, and noncancellation between them; the small penetration factor alone supplies none of these" .reconstructedStep], paperClaim .coulombThresholdResult .coulombThresholdResult .mainConclusion [equation "(51a)" "45" "under the noncancelling threshold condition, k tends to zero and the isolated nuclear partial-wave strength vanishes; this does not assert a vanishing total Coulomb-plus-nuclear proton cross section" .reconstructedStep], paperClaim .protonSetup .protonEmpiricalSetup .evidence [page "46" "extract the selected finite S-wave phase-shift samples, keeping calibration and held-out validation data distinct", equation "(4)" "39" "calibrate the plotted laboratory energy and momentum with the nucleon mass, not the relative kinetic energy" .reconstructedStep], paperClaim .protonFit .protonFitCalculation .intermediate [pageRange "46-47" "evaluate actual dimensionless Coulomb-function residuals on finite samples and retain the qualified slope and reporting errors" .reconstructedStep, equation "(4)" "39" "retain the laboratory-energy coefficient in the slope-to-range conversion" .reconstructedStep, equation "(51), (53)" "45-46" "convert the slope to a range estimate; the fitted line is not an exact continuum law or the exact integral-defined range" .reconstructedStep], paperClaim .highEnergyAssessment .highEnergyAssessment .intermediate [pageRange "46-47" "separate Wilson's error-compatible measurements from Dearnley's upward departure; retain its excess over the square-well expectation, the excluded P-wave tensor explanation, and unresolved status"], paperClaim .protonResult .protonEmpiricalResult .mainConclusion [equation "(53)" "46" "derive the proton-proton range estimate and finite phase-residual bounds from the fitted slope, with separate uncertainty and higher-energy qualifications" .reconstructedStep], paperClaim .chargeSetup .chargeComparisonSetup .setupPremise [pageRange "47-49" "compare actual charged and neutral zero-energy waves for the same nuclear potential; keep the neutron-proton singlet separate from the triplet and retain normalized radial admissibility" .reconstructedStep], paperClaim .chargeWeightedCalculation .chargeWeightedCalculation .intermediate [equation "(57)-(58)" "48" "supply the two finite weighted integral identities, convergent weighted balance, actual boundary limit, and nonzero comparison values at a positive cutoff" .reconstructedStep], paperClaim .chargeWeightedResult .chargeWeightedResult .mainConclusion [equation "(59)-(60)" "48" "derive logarithmic-slope equality and the equivalent neutral reciprocal length from the weighted Wronskian comparison before fitting or truncating" .reconstructedStep], paperClaim .chargeReadoutCalculation .chargeReadoutCalculation .intermediate [equation "(55)-(56), (61)-(72)" "47-49" "retain explicit radius, source-intercept, wave-value, wave-slope, denominator-margin, and series-remainder controls; the printed plus-sign tail parameter is not silently equated with the minus-sign neutral reciprocal length" .reconstructedStep], paperClaim .chargeEstimateResult .chargeEstimateResult .mainConclusion [equation "(55)-(61), (71)-(72)" "47-49" "derive a controlled first-order inverse-length estimate using the same zero-energy Coulomb source; the rigorous sufficient error budgets are reconstruction inputs, not certified numerical results of the paper" .reconstructedStep], paperClaim .chargeCalculation .chargeComparisonCalculation .intermediate [pageRange "49-50" "calibrate the neutron-proton singlet measurement and require a strict error-separated gap small relative to the natural inverse-range scale" .reconstructedStep], paperClaim .chargeInterpretation .chargeDependenceInterpretation .intermediate [pageRange "49-50" "retain normalized-scattering uniqueness and the separate cited potential-depth calculation conditional on common intrinsic range and shape; failure to establish that premise does not negate it" .reconstructedStep], paperClaim .chargeResult .chargeComparisonResult .mainConclusion [page "49" "derive unequal actual inverse lengths and nonidentical nuclear potentials from error separation; a pointwise small potential difference remains conditional on the cited depth input and common range and shape" .reconstructedStep], paperClaim .chargeShapeExpectation .chargeShapeExpectation .intermediate [page "49" "the unevaluated exponential and Gaussian potentials are expected to lie between the square-well and Yukawa estimates before the finite-length corrections; preserve this author expectation separately"], paperClaim .chargeShapeErrorBudget .chargeShapeErrorBudget .setupPremise [page "49" "make explicit a sufficient calibration budget smaller than the uncorrected bracket's minimum measured gap; no such complete numerical error certificate is supplied by the original paper" .reconstructedStep], paperClaim .chargeShapeResult .chargeShapeResult .mainConclusion [pageRange "49-50" "conditional on the author bracket and actual model calibration, the additional normalized shape models retain an inverse-length gap; potential inequality additionally uses normalized-solution uniqueness" .reconstructedStep], paperClaim .scopeQualifications .paperScopeQualifications .intermediate [page "38" "defer tensor-force and deuteron photoelectric and photomagnetic extensions to subsequent work"], paperClaim .completeResult .completeScopedResult .mainConclusion [pageRange "38-50" "assemble the exact, approximate, observable cross-section, empirical, comparative, and scope-qualified conclusions" .reconstructedStep] ] def rawSteps : List (ArgumentStep StepId ClaimId) := [ { id := .stateNeutralSetup, premises := [], conclusion := .neutralSetup, inference := .introduce, justification := .physicalPrinciple }, { id := .supplyNeutralCalculation, premises := [], conclusion := .neutralCalculation, inference := .computation, justification := .paperDerivation }, { id := .supplyNeutralRadialFormulaCalculation, premises := [], conclusion := .neutralFormulaCalculation, inference := .computation, justification := .paperDerivation }, { id := .deriveNeutralRadialFormulaReadout, premises := [.neutralSetup, .neutralFormulaCalculation], conclusion := .neutralFormulaReadout, inference := .computation, justification := .paperDerivation }, { id := .deriveNeutralResult, premises := [.neutralSetup, .neutralCalculation, .neutralFormulaReadout], conclusion := .neutralResult, inference := .logicalComposition, justification := .paperDerivation }, { id := .stateApproximationSetup, premises := [], conclusion := .approximationSetup, inference := .introduce, justification := .physicalPrinciple }, { id := .supplyReductionCalculation, premises := [], conclusion := .reductionCalculation, inference := .approximation, justification := .controlledApproximation }, { id := .supplyEffectiveRangeIdentification, premises := [], conclusion := .effectiveRangeIdentification, inference := .logicalComposition, justification := .interpretiveInference }, { id := .deriveEffectiveRangeResult, premises := [.neutralResult, .approximationSetup, .reductionCalculation, .effectiveRangeIdentification], conclusion := .effectiveRangeResult, inference := .logicalComposition, justification := .controlledApproximation }, { id := .stateCrossSectionSetup, premises := [], conclusion := .crossSectionSetup, inference := .introduce, justification := .physicalPrinciple }, { id := .supplyCrossSectionCalculation, premises := [], conclusion := .crossSectionCalculation, inference := .computation, justification := .paperDerivation }, { id := .supplyCrossSectionInterpretation, premises := [], conclusion := .crossSectionInterpretation, inference := .logicalComposition, justification := .interpretiveInference }, { id := .deriveCrossSectionAssessment, premises := [.effectiveRangeResult, .crossSectionSetup, .crossSectionCalculation, .crossSectionInterpretation], conclusion := .crossSectionResult, inference := .logicalComposition, justification := .paperDerivation }, { id := .deriveCrossSectionFormula, premises := [.crossSectionResult], conclusion := .crossSectionFormula, inference := .logicalComposition, justification := .paperDerivation }, { id := .supplyCorrectionCalculation, premises := [], conclusion := .correctionCalculation, inference := .computation, justification := .paperDerivation }, { id := .interpretCurvatureDiagnostic, premises := [], conclusion := .curvatureDiagnostic, inference := .logicalComposition, justification := .interpretiveInference }, { id := .interpretShapeSensitivity, premises := [], conclusion := .shapeInterpretation, inference := .logicalComposition, justification := .interpretiveInference }, { id := .deriveAccuracyResult, premises := [.effectiveRangeResult, .correctionCalculation, .curvatureDiagnostic, .shapeInterpretation], conclusion := .accuracyResult, inference := .logicalComposition, justification := .controlledApproximation }, { id := .stateTripletSetup, premises := [], conclusion := .tripletSetup, inference := .evidentialSupport, justification := .importedResult }, { id := .supplyTripletCalculation, premises := [], conclusion := .tripletCalculation, inference := .computation, justification := .paperDerivation }, { id := .deriveTripletResult, premises := [.effectiveRangeResult, .tripletSetup, .tripletCalculation], conclusion := .tripletResult, inference := .logicalComposition, justification := .paperDerivation }, { id := .stateSingletLimitation, premises := [], conclusion := .singletLimitation, inference := .evidentialSupport, justification := .importedResult }, { id := .supplySingletBorrowing, premises := [], conclusion := .singletBorrowing, inference := .logicalComposition, justification := .interpretiveInference }, { id := .deriveSingletAssessment, premises := [.singletLimitation, .singletBorrowing], conclusion := .singletAssessment, inference := .logicalComposition, justification := .interpretiveInference }, { id := .stateCoulombSetup, premises := [], conclusion := .coulombSetup, inference := .introduce, justification := .physicalPrinciple }, { id := .supplyCoulombCalculation, premises := [], conclusion := .coulombCalculation, inference := .computation, justification := .paperDerivation }, { id := .deriveCoulombSourceFormula, premises := [.coulombSetup, .coulombCalculation], conclusion := .coulombSourceFormula, inference := .logicalComposition, justification := .paperDerivation }, { id := .supplyCoulombRangeReplacement, premises := [], conclusion := .coulombRangeReplacement, inference := .approximation, justification := .controlledApproximation }, { id := .supplyCoulombIdentification, premises := [], conclusion := .coulombIdentification, inference := .logicalComposition, justification := .interpretiveInference }, { id := .deriveCoulombResult, premises := [.coulombSourceFormula, .coulombRangeReplacement, .coulombIdentification], conclusion := .coulombResult, inference := .logicalComposition, justification := .controlledApproximation }, { id := .supplyCoulombNeutralization, premises := [], conclusion := .coulombNeutralizationCalculation, inference := .approximation, justification := .controlledApproximation }, { id := .deriveCoulombNeutralization, premises := [.coulombSourceFormula, .coulombResult, .coulombNeutralizationCalculation], conclusion := .coulombNeutralizationResult, inference := .logicalComposition, justification := .controlledApproximation }, { id := .stateCoulombThresholdSetup, premises := [], conclusion := .coulombThresholdSetup, inference := .introduce, justification := .physicalPrinciple }, { id := .supplyCoulombThresholdRegularity, premises := [], conclusion := .coulombThresholdRegularity, inference := .introduce, justification := .importedResult }, { id := .deriveCoulombThreshold, premises := [.coulombThresholdSetup, .coulombThresholdRegularity], conclusion := .coulombThresholdResult, inference := .logicalComposition, justification := .paperDerivation }, { id := .stateProtonSetup, premises := [], conclusion := .protonSetup, inference := .evidentialSupport, justification := .importedResult }, { id := .supplyProtonFit, premises := [], conclusion := .protonFit, inference := .computation, justification := .paperDerivation }, { id := .assessHighEnergyData, premises := [], conclusion := .highEnergyAssessment, inference := .logicalComposition, justification := .openObligation }, { id := .deriveProtonResult, premises := [.coulombResult, .protonSetup, .protonFit, .highEnergyAssessment], conclusion := .protonResult, inference := .logicalComposition, justification := .paperDerivation }, { id := .stateChargeSetup, premises := [], conclusion := .chargeSetup, inference := .introduce, justification := .physicalPrinciple }, { id := .supplyChargeWeightedCalculation, premises := [], conclusion := .chargeWeightedCalculation, inference := .computation, justification := .paperDerivation }, { id := .deriveChargeWeightedResult, premises := [.chargeSetup, .chargeWeightedCalculation], conclusion := .chargeWeightedResult, inference := .logicalComposition, justification := .paperDerivation }, { id := .supplyChargeReadoutCalculation, premises := [], conclusion := .chargeReadoutCalculation, inference := .approximation, justification := .controlledApproximation }, { id := .deriveChargeEstimate, premises := [.chargeWeightedResult, .coulombSourceFormula, .protonResult, .chargeReadoutCalculation], conclusion := .chargeEstimateResult, inference := .logicalComposition, justification := .controlledApproximation }, { id := .supplyChargeCalculation, premises := [], conclusion := .chargeCalculation, inference := .computation, justification := .controlledApproximation }, { id := .interpretChargeDependence, premises := [], conclusion := .chargeInterpretation, inference := .logicalComposition, justification := .interpretiveInference }, { id := .deriveChargeResult, premises := [.protonResult, .chargeEstimateResult, .singletAssessment, .chargeCalculation, .chargeInterpretation], conclusion := .chargeResult, inference := .logicalComposition, justification := .interpretiveInference }, { id := .stateChargeShapeExpectation, premises := [], conclusion := .chargeShapeExpectation, inference := .introduce, justification := .authorExpectation }, { id := .supplyChargeShapeErrorBudget, premises := [], conclusion := .chargeShapeErrorBudget, inference := .approximation, justification := .controlledApproximation }, { id := .deriveChargeShapeAssessment, premises := [.chargeShapeExpectation, .chargeShapeErrorBudget], conclusion := .chargeShapeResult, inference := .logicalComposition, justification := .paperDerivation }, { id := .stateScopeQualifications, premises := [], conclusion := .scopeQualifications, inference := .introduce, justification := .deferredCalculation }, { id := .assembleCompleteResult, premises := [.neutralResult, .effectiveRangeResult, .crossSectionResult, .accuracyResult, .tripletResult, .singletAssessment, .coulombResult, .coulombNeutralizationResult, .coulombThresholdResult, .protonResult, .chargeResult, .chargeShapeResult, .scopeQualifications], conclusion := .completeResult, inference := .logicalComposition, justification := .paperDerivation } ] def stepSources : StepId → List SourceRef | .stateNeutralSetup => [pageRange "38-39" "state the neutral finite-range setup"] | .supplyNeutralCalculation => [page "39" "identify the selected scalar readouts with the phase difference, wave-number difference, and actual integral" .reconstructedStep] | .supplyNeutralRadialFormulaCalculation => [pageRange "39-40" "supply finite-radius Wronskian identities, convergent overlap, asymptotic boundary matching, and exact range definitions before deriving (10)" .reconstructedStep] | .deriveNeutralRadialFormulaReadout => [equation "(7), (10), (11), (13)-(14)" "39-40" "derive the exact comparison identity from finite-radius subtraction and limits; retain actual normalization, origin derivative, and range integrals"] | .deriveNeutralResult => [equation "(10)-(13)" "39" "obtain the exact neutral result"] | .stateApproximationSetup => [page "39" "state the low-energy interior-wave conditions"] | .supplyReductionCalculation => [equation "(14)" "39" "supply explicit integral error control for replacing the interior waves by their zero-energy values" .reconstructedStep] | .supplyEffectiveRangeIdentification => [equation "(16)" "40" "identify the neutral effective-range law"] | .deriveEffectiveRangeResult => [equation "(14)-(16)" "39-40" "derive a phase error bound from controlled range replacement, with exact equality only when its residual vanishes" .reconstructedStep] | .stateCrossSectionSetup => [page "40" "select the neutral triplet cross-section regime"] | .supplyCrossSectionCalculation => [equation "(17)-(18)" "40" "calculate the S-wave cross section, bound, and maximum" .reconstructedStep] | .supplyCrossSectionInterpretation => [page "40" "retain the near-maximum truncation warning"] | .deriveCrossSectionAssessment => [equation "(17)-(18)" "40" "state the unitarity-scoped cross-section assessment"] | .deriveCrossSectionFormula => [equation "(17)" "40" "retain the displayed S-wave formula"] | .supplyCorrectionCalculation => [pageRange "42-44" "derive equations (29)-(36)" .reconstructedStep] | .interpretCurvatureDiagnostic => [page "44" "retain the sign-sensitive curvature diagnostic and the lack of significant deviation"] | .interpretShapeSensitivity => [page "44" "interpret the sign of resolved curvature"] | .deriveAccuracyResult => [page "44" "assess the approximation and shape information"] | .stateTripletSetup => [pageRange "40-41" "state the deuteron and scattering data"] | .supplyTripletCalculation => [pageRange "40-41" "derive equation (19) from the normalized decaying comparison's origin derivative and the bound-energy overlap identity, then use the separate controlled replacement and data for equations (20)-(27)" .reconstructedStep] | .deriveTripletResult => [equation "(27)" "41" "state the extracted triplet range"] | .stateSingletLimitation => [page "41" "state that existing neutron-proton singlet data do not fix the range"] | .supplySingletBorrowing => [page "41" "retain approximate force equality and the separate borrowed proton-proton range"] | .deriveSingletAssessment => [page "41" "assemble the qualified singlet-range assessment"] | .stateCoulombSetup => [equation "(37)-(41)" "43-44" "state the actual Coulomb radial equations, proton parameters, and distinct zero/positive-energy points"] | .supplyCoulombCalculation => [equation "(42)-(50)" "44-45" "supply the Coulomb basis and its combination, common-log derivative expansion, integrated comparison, and actual scalar identifications" .reconstructedStep] | .deriveCoulombSourceFormula => [equation "(42)-(43), (47a), (50)-(51)" "44-45" "derive the normalized relative phase and dimensionless source function after cancelling the common logarithm at the same positive radius" .reconstructedStep] | .supplyCoulombRangeReplacement => [equation "(52)" "45" "supply the charged energy-overlap replacement error separately" .reconstructedStep] | .supplyCoulombIdentification => [equation "(51)-(52)" "45" "identify the Coulomb-modified effective-range law"] | .deriveCoulombResult => [equation "(51)-(52)" "45" "derive the two-parameter phase error from the charged range replacement" .reconstructedStep] | .supplyCoulombNeutralization => [equation "(52)" "45" "control the independent removal of Coulomb distortion from the zero-energy overlap" .reconstructedStep] | .deriveCoulombNeutralization => [equation "(52)" "45" "combine the two independent errors only after the same-potential neutralization calculation" .reconstructedStep] | .stateCoulombThresholdSetup => [equation "(41), (51a)" "44-45" "select the actual zero-momentum limit with Coulomb-relative scattering realizations" .reconstructedStep] | .supplyCoulombThresholdRegularity => [page "45" "retain the finite intercept, special-function limit, and noncancellation as explicit threshold inputs" .reconstructedStep] | .deriveCoulombThreshold => [equation "(51a)" "45" "derive suppression of the nuclear partial-wave strength, not the total charged cross section" .reconstructedStep] | .stateProtonSetup => [page "46" "select finite measured phase-shift calibration and validation samples", equation "(4)" "39" "retain the actual laboratory-energy calibration" .reconstructedStep] | .supplyProtonFit => [page "46" "evaluate Figure 3 residuals and the reported slope accuracy without claiming a continuum guarantee" .reconstructedStep] | .assessHighEnergyData => [pageRange "46-47" "retain the separate error-compatible and discrepant high-energy observations, the square-well comparison, and the open explanation"] | .deriveProtonResult => [equation "(4)" "39" "use the laboratory-energy slope conversion" .reconstructedStep, equation "(51), (53)" "45-46" "derive the calibrated range fit and propagate slope and rounding errors while keeping both high-energy outcomes" .reconstructedStep] | .stateChargeSetup => [pageRange "47-48" "state the actual same-potential zero-energy radial problem and the distinct neutron-proton singlet channel" .reconstructedStep] | .supplyChargeWeightedCalculation => [equation "(57)-(58)" "48" "retain finite weighted integration, the actual asymptotic boundary limit, and weighted balance at a positive radius" .reconstructedStep] | .deriveChargeWeightedResult => [equation "(59)-(60)" "48" "derive the zero comparison Wronskian, logarithmic derivative relation, and nonzero-denominator reciprocal readout" .reconstructedStep] | .supplyChargeReadoutCalculation => [equation "(55)-(56), (61)-(72)" "47-49" "use the same empirical line intercept as Figure 3, with sufficient independent zero-energy extrapolation, radius, wave, and truncation error controls not numerically certified by the original text" .reconstructedStep] | .deriveChargeEstimate => [equation "(55)-(61)" "47-48" "propagate actual value and slope errors through the inverse readout, with the separate logarithmic-radius error and explicit rational remainder" .reconstructedStep] | .supplyChargeCalculation => [pageRange "49-50" "retain neutron-singlet calibration, strict separation, and the small inverse-range response scale" .reconstructedStep] | .interpretChargeDependence => [pageRange "49-50" "use normalized-scattering uniqueness and the separately cited depth comparison only under common range and shape" .reconstructedStep] | .deriveChargeResult => [pageRange "49-50" "derive the definite potential inequality and conditional small pointwise difference, without negating the unestablished common-shape premise" .reconstructedStep] | .stateChargeShapeExpectation => [page "49" "retain the author's uncomputed exponential/Gaussian bracket before finite-length corrections"] | .supplyChargeShapeErrorBudget => [page "49" "state a sufficient error budget for the uncorrected bracket's minimum gap" .reconstructedStep] | .deriveChargeShapeAssessment => [pageRange "49-50" "deduce a conditional actual-model comparison without upgrading author expectation or model calibration to proved calculations" .reconstructedStep] | .stateScopeQualifications => [page "38" "retain the explicitly deferred extensions"] | .assembleCompleteResult => [pageRange "38-50" "assemble the complete scoped result" .reconstructedStep] def steps : List (ArgumentStep StepId ClaimId) := rawSteps.map fun step => { step with sources := stepSources step.id } def neutralRoute : ArgumentRoute RouteId RouteKind StepId ClaimId := { id := .neutralComparison, kind := .exactFiniteRangeComparison, dependsOn := [], steps := [.stateNeutralSetup, .supplyNeutralCalculation, .supplyNeutralRadialFormulaCalculation, .deriveNeutralRadialFormulaReadout, .deriveNeutralResult], outputs := [.neutralFormulaReadout, .neutralResult] } def reductionRoute : ArgumentRoute RouteId RouteKind StepId ClaimId := { id := .effectiveRangeReduction, kind := .controlledLowEnergyReduction, dependsOn := [.neutralComparison], steps := [.stateApproximationSetup, .supplyReductionCalculation, .supplyEffectiveRangeIdentification, .deriveEffectiveRangeResult], outputs := [.effectiveRangeResult] } def crossSectionRoute : ArgumentRoute RouteId RouteKind StepId ClaimId := { id := .neutralCrossSection, kind := .sWaveCrossSectionUnitarity, dependsOn := [.effectiveRangeReduction], steps := [.stateCrossSectionSetup, .supplyCrossSectionCalculation, .supplyCrossSectionInterpretation, .deriveCrossSectionAssessment, .deriveCrossSectionFormula], outputs := [.crossSectionResult, .crossSectionFormula] } def accuracyRoute : ArgumentRoute RouteId RouteKind StepId ClaimId := { id := .accuracyAndShape, kind := .higherOrderErrorAndShapeScope, dependsOn := [.effectiveRangeReduction], steps := [.supplyCorrectionCalculation, .interpretCurvatureDiagnostic, .interpretShapeSensitivity, .deriveAccuracyResult], outputs := [.accuracyResult] } def tripletRoute : ArgumentRoute RouteId RouteKind StepId ClaimId := { id := .tripletExtraction, kind := .boundStateDataExtraction, dependsOn := [.effectiveRangeReduction], steps := [.stateTripletSetup, .supplyTripletCalculation, .deriveTripletResult], outputs := [.tripletResult] } def singletRoute : ArgumentRoute RouteId RouteKind StepId ClaimId := { id := .singletRangeQualification, kind := .singletRangeDataQualification, dependsOn := [], steps := [.stateSingletLimitation, .supplySingletBorrowing, .deriveSingletAssessment], outputs := [.singletAssessment] } def coulombComparisonRoute : ArgumentRoute RouteId RouteKind StepId ClaimId := { id := .coulombComparison, kind := .exactChargedWaveComparison, dependsOn := [], steps := [.stateCoulombSetup, .supplyCoulombCalculation, .deriveCoulombSourceFormula], outputs := [.coulombSourceFormula] } def coulombRoute : ArgumentRoute RouteId RouteKind StepId ClaimId := { id := .coulombTheory, kind := .coulombModifiedComparison, dependsOn := [.coulombComparison], steps := [.supplyCoulombRangeReplacement, .supplyCoulombIdentification, .deriveCoulombResult], outputs := [.coulombResult] } def coulombNeutralizationRoute : ArgumentRoute RouteId RouteKind StepId ClaimId := { id := .coulombNeutralization, kind := .separateCoulombRemovalApproximation, dependsOn := [.coulombComparison, .coulombTheory], steps := [.supplyCoulombNeutralization, .deriveCoulombNeutralization], outputs := [.coulombNeutralizationResult] } def coulombThresholdRoute : ArgumentRoute RouteId RouteKind StepId ClaimId := { id := .coulombThreshold, kind := .nonresonantCoulombThreshold, dependsOn := [], steps := [.stateCoulombThresholdSetup, .supplyCoulombThresholdRegularity, .deriveCoulombThreshold], outputs := [.coulombThresholdResult] } def protonRoute : ArgumentRoute RouteId RouteKind StepId ClaimId := { id := .protonExperiment, kind := .empiricalLowAndHighEnergyAssessment, dependsOn := [.coulombTheory], steps := [.stateProtonSetup, .supplyProtonFit, .assessHighEnergyData, .deriveProtonResult], outputs := [.protonResult] } def chargeWeightedRoute : ArgumentRoute RouteId RouteKind StepId ClaimId := { id := .chargeWeightedComparison, kind := .exactWeightedChargeComparison, dependsOn := [], steps := [.stateChargeSetup, .supplyChargeWeightedCalculation, .deriveChargeWeightedResult], outputs := [.chargeWeightedResult] } def chargeEstimateRoute : ArgumentRoute RouteId RouteKind StepId ClaimId := { id := .chargeEstimate, kind := .controlledChargeReadout, dependsOn := [.chargeWeightedComparison, .coulombComparison, .protonExperiment], steps := [.supplyChargeReadoutCalculation, .deriveChargeEstimate], outputs := [.chargeEstimateResult] } def chargeRoute : ArgumentRoute RouteId RouteKind StepId ClaimId := { id := .chargeComparison, kind := .counterfactualInteractionComparison, dependsOn := [.chargeEstimate, .protonExperiment, .singletRangeQualification], steps := [.supplyChargeCalculation, .interpretChargeDependence, .deriveChargeResult], outputs := [.chargeResult] } def chargeShapeRoute : ArgumentRoute RouteId RouteKind StepId ClaimId := { id := .chargeShapeAssessment, kind := .conditionalShapeExtrapolation, dependsOn := [], steps := [.stateChargeShapeExpectation, .supplyChargeShapeErrorBudget, .deriveChargeShapeAssessment], outputs := [.chargeShapeResult] } def completeRoute : ArgumentRoute RouteId RouteKind StepId ClaimId := { id := .completeScopedResult, kind := .completePaperAssessment, dependsOn := [.neutralComparison, .effectiveRangeReduction, .neutralCrossSection, .accuracyAndShape, .tripletExtraction, .singletRangeQualification, .coulombComparison, .coulombTheory, .coulombNeutralization, .coulombThreshold, .protonExperiment, .chargeWeightedComparison, .chargeEstimate, .chargeComparison, .chargeShapeAssessment], steps := [.stateScopeQualifications, .assembleCompleteResult], outputs := [.scopeQualifications, .completeResult] } def routes : List (ArgumentRoute RouteId RouteKind StepId ClaimId) := [neutralRoute, reductionRoute, crossSectionRoute, accuracyRoute, tripletRoute, singletRoute, coulombComparisonRoute, coulombRoute, coulombNeutralizationRoute, coulombThresholdRoute, protonRoute, chargeWeightedRoute, chargeEstimateRoute, chargeRoute, chargeShapeRoute, completeRoute] def argument : PaperArgument ClaimId StepId Atom := { title := "Bethe effective-range theory in nuclear scattering (1949)" sources := [originalPaper "complete paper, journal pages 38-50" "original version of record"] claims := claims steps := steps mainConclusion := .completeResult } def routedArgument : RoutedArgument ClaimId StepId Atom RouteId RouteKind := { argument := argument, routes := routes } theorem argument_wellFormed : argument.wellFormed = true := by native_decide theorem argument_auditable : argument.auditable = true := by native_decide theorem routes_wellFormed : routedArgument.wellFormed = true := by native_decide theorem routes_have_exact_predecessor_graph : neutralRoute.dependsOn = [] ∧ reductionRoute.dependsOn = [.neutralComparison] ∧ crossSectionRoute.dependsOn = [.effectiveRangeReduction] ∧ accuracyRoute.dependsOn = [.effectiveRangeReduction] ∧ tripletRoute.dependsOn = [.effectiveRangeReduction] ∧ singletRoute.dependsOn = [] ∧ coulombComparisonRoute.dependsOn = [] ∧ coulombRoute.dependsOn = [.coulombComparison] ∧ coulombNeutralizationRoute.dependsOn = [.coulombComparison, .coulombTheory] ∧ coulombThresholdRoute.dependsOn = [] ∧ protonRoute.dependsOn = [.coulombTheory] ∧ chargeWeightedRoute.dependsOn = [] ∧ chargeEstimateRoute.dependsOn = [.chargeWeightedComparison, .coulombComparison, .protonExperiment] ∧ chargeRoute.dependsOn = [.chargeEstimate, .protonExperiment, .singletRangeQualification] ∧ chargeShapeRoute.dependsOn = [] ∧ completeRoute.dependsOn = [.neutralComparison, .effectiveRangeReduction, .neutralCrossSection, .accuracyAndShape, .tripletExtraction, .singletRangeQualification, .coulombComparison, .coulombTheory, .coulombNeutralization, .coulombThreshold, .protonExperiment, .chargeWeightedComparison, .chargeEstimate, .chargeComparison, .chargeShapeAssessment] := by native_decide theorem routes_have_exact_dependency_closure : routedArgument.routeDependencyIds neutralRoute = [] ∧ routedArgument.routeDependencyIds reductionRoute = [.neutralComparison] ∧ routedArgument.routeDependencyIds crossSectionRoute = [.effectiveRangeReduction, .neutralComparison] ∧ routedArgument.routeDependencyIds accuracyRoute = [.effectiveRangeReduction, .neutralComparison] ∧ routedArgument.routeDependencyIds tripletRoute = [.effectiveRangeReduction, .neutralComparison] ∧ routedArgument.routeDependencyIds singletRoute = [] ∧ routedArgument.routeDependencyIds coulombComparisonRoute = [] ∧ routedArgument.routeDependencyIds coulombRoute = [.coulombComparison] ∧ routedArgument.routeDependencyIds coulombNeutralizationRoute = [.coulombComparison, .coulombTheory] ∧ routedArgument.routeDependencyIds coulombThresholdRoute = [] ∧ routedArgument.routeDependencyIds protonRoute = [.coulombTheory, .coulombComparison] ∧ routedArgument.routeDependencyIds chargeWeightedRoute = [] ∧ routedArgument.routeDependencyIds chargeEstimateRoute = [.chargeWeightedComparison, .coulombComparison, .protonExperiment, .coulombTheory] ∧ routedArgument.routeDependencyIds chargeRoute = [.chargeEstimate, .protonExperiment, .singletRangeQualification, .coulombTheory, .chargeWeightedComparison, .coulombComparison] ∧ routedArgument.routeDependencyIds chargeShapeRoute = [] ∧ routedArgument.routeDependencyIds completeRoute = [.neutralComparison, .effectiveRangeReduction, .neutralCrossSection, .accuracyAndShape, .tripletExtraction, .singletRangeQualification, .coulombComparison, .coulombTheory, .coulombNeutralization, .coulombThreshold, .protonExperiment, .chargeWeightedComparison, .chargeEstimate, .chargeComparison, .chargeShapeAssessment] := by native_decide theorem routes_expose_declared_dependency_outputs : neutralRoute.outputs = [.neutralFormulaReadout, .neutralResult] ∧ reductionRoute.outputs = [.effectiveRangeResult] ∧ crossSectionRoute.outputs = [.crossSectionResult, .crossSectionFormula] ∧ accuracyRoute.outputs = [.accuracyResult] ∧ tripletRoute.outputs = [.tripletResult] ∧ singletRoute.outputs = [.singletAssessment] ∧ coulombComparisonRoute.outputs = [.coulombSourceFormula] ∧ coulombRoute.outputs = [.coulombResult] ∧ coulombNeutralizationRoute.outputs = [.coulombNeutralizationResult] ∧ coulombThresholdRoute.outputs = [.coulombThresholdResult] ∧ protonRoute.outputs = [.protonResult] ∧ chargeWeightedRoute.outputs = [.chargeWeightedResult] ∧ chargeEstimateRoute.outputs = [.chargeEstimateResult] ∧ chargeRoute.outputs = [.chargeResult] ∧ chargeShapeRoute.outputs = [.chargeShapeResult] ∧ completeRoute.outputs = [.scopeQualifications, .completeResult] := by native_decide theorem local_setup_steps_do_not_claim_unearned_predecessors : argument.stepRule? .stateNeutralSetup = some ([], .neutralSetup) ∧ argument.stepRule? .stateApproximationSetup = some ([], .approximationSetup) ∧ argument.stepRule? .stateCrossSectionSetup = some ([], .crossSectionSetup) ∧ argument.stepRule? .stateTripletSetup = some ([], .tripletSetup) ∧ argument.stepRule? .stateSingletLimitation = some ([], .singletLimitation) ∧ argument.stepRule? .stateCoulombSetup = some ([], .coulombSetup) ∧ argument.stepRule? .stateCoulombThresholdSetup = some ([], .coulombThresholdSetup) ∧ argument.stepRule? .stateProtonSetup = some ([], .protonSetup) ∧ argument.stepRule? .stateChargeSetup = some ([], .chargeSetup) ∧ argument.stepRule? .stateScopeQualifications = some ([], .scopeQualifications) := by native_decide def neutral_descendant_steps_name_inherited_outputs : Prop := argument.stepRule? .deriveEffectiveRangeResult = some ([.neutralResult, .approximationSetup, .reductionCalculation, .effectiveRangeIdentification], .effectiveRangeResult) ∧ argument.stepRule? .deriveCrossSectionAssessment = some ([.effectiveRangeResult, .crossSectionSetup, .crossSectionCalculation, .crossSectionInterpretation], .crossSectionResult) ∧ argument.stepRule? .deriveCrossSectionFormula = some ([.crossSectionResult], .crossSectionFormula) ∧ argument.stepRule? .deriveAccuracyResult = some ([.effectiveRangeResult, .correctionCalculation, .curvatureDiagnostic, .shapeInterpretation], .accuracyResult) ∧ argument.stepRule? .deriveTripletResult = some ([.effectiveRangeResult, .tripletSetup, .tripletCalculation], .tripletResult) def charged_descendant_steps_name_inherited_outputs : Prop := argument.stepRule? .deriveCoulombResult = some ([.coulombSourceFormula, .coulombRangeReplacement, .coulombIdentification], .coulombResult) ∧ argument.stepRule? .deriveCoulombNeutralization = some ([.coulombSourceFormula, .coulombResult, .coulombNeutralizationCalculation], .coulombNeutralizationResult) ∧ argument.stepRule? .deriveProtonResult = some ([.coulombResult, .protonSetup, .protonFit, .highEnergyAssessment], .protonResult) ∧ argument.stepRule? .deriveChargeEstimate = some ([.chargeWeightedResult, .coulombSourceFormula, .protonResult, .chargeReadoutCalculation], .chargeEstimateResult) ∧ argument.stepRule? .deriveChargeResult = some ([.protonResult, .chargeEstimateResult, .singletAssessment, .chargeCalculation, .chargeInterpretation], .chargeResult) def complete_step_names_inherited_outputs : Prop := argument.stepRule? .assembleCompleteResult = some ([.neutralResult, .effectiveRangeResult, .crossSectionResult, .accuracyResult, .tripletResult, .singletAssessment, .coulombResult, .coulombNeutralizationResult, .coulombThresholdResult, .protonResult, .chargeResult, .chargeShapeResult, .scopeQualifications], .completeResult) private theorem neutral_descendant_steps_name_inherited_outputs_hold : neutral_descendant_steps_name_inherited_outputs := by unfold neutral_descendant_steps_name_inherited_outputs native_decide private theorem charged_descendant_steps_name_inherited_outputs_hold : charged_descendant_steps_name_inherited_outputs := by unfold charged_descendant_steps_name_inherited_outputs native_decide private theorem complete_step_names_inherited_outputs_hold : complete_step_names_inherited_outputs := by unfold complete_step_names_inherited_outputs native_decide theorem dependent_steps_name_inherited_outputs : neutral_descendant_steps_name_inherited_outputs ∧ charged_descendant_steps_name_inherited_outputs ∧ complete_step_names_inherited_outputs := by exact ⟨neutral_descendant_steps_name_inherited_outputs_hold, charged_descendant_steps_name_inherited_outputs_hold, complete_step_names_inherited_outputs_hold⟩ def calculationAndInterpretationContractSteps : List (StepId × ClaimId) := [(.supplyNeutralCalculation, .neutralCalculation), (.supplyNeutralRadialFormulaCalculation, .neutralFormulaCalculation), (.supplyReductionCalculation, .reductionCalculation), (.supplyEffectiveRangeIdentification, .effectiveRangeIdentification), (.supplyCrossSectionCalculation, .crossSectionCalculation), (.supplyCrossSectionInterpretation, .crossSectionInterpretation), (.supplyCorrectionCalculation, .correctionCalculation), (.interpretCurvatureDiagnostic, .curvatureDiagnostic), (.interpretShapeSensitivity, .shapeInterpretation), (.supplyTripletCalculation, .tripletCalculation), (.supplySingletBorrowing, .singletBorrowing), (.supplyCoulombCalculation, .coulombCalculation), (.supplyCoulombRangeReplacement, .coulombRangeReplacement), (.supplyCoulombIdentification, .coulombIdentification), (.supplyCoulombNeutralization, .coulombNeutralizationCalculation), (.supplyCoulombThresholdRegularity, .coulombThresholdRegularity), (.supplyProtonFit, .protonFit), (.assessHighEnergyData, .highEnergyAssessment), (.supplyChargeWeightedCalculation, .chargeWeightedCalculation), (.supplyChargeReadoutCalculation, .chargeReadoutCalculation), (.supplyChargeCalculation, .chargeCalculation), (.interpretChargeDependence, .chargeInterpretation), (.stateChargeShapeExpectation, .chargeShapeExpectation), (.supplyChargeShapeErrorBudget, .chargeShapeErrorBudget)] def isIndependentContract : StepId × ClaimId → Bool | (stepId, claimId) => match argument.stepRule? stepId with | some ([], conclusion) => decide (conclusion = claimId) | _ => false theorem calculation_and_interpretation_contracts_are_independent_hypotheses : calculationAndInterpretationContractSteps.all isIndependentContract = true := by native_decide theorem result_steps_apply_selected_setups_and_contracts : argument.stepRule? .deriveNeutralRadialFormulaReadout = some ([.neutralSetup, .neutralFormulaCalculation], .neutralFormulaReadout) ∧ argument.stepRule? .deriveNeutralResult = some ([.neutralSetup, .neutralCalculation, .neutralFormulaReadout], .neutralResult) ∧ argument.stepRule? .deriveEffectiveRangeResult = some ([.neutralResult, .approximationSetup, .reductionCalculation, .effectiveRangeIdentification], .effectiveRangeResult) ∧ argument.stepRule? .deriveCrossSectionAssessment = some ([.effectiveRangeResult, .crossSectionSetup, .crossSectionCalculation, .crossSectionInterpretation], .crossSectionResult) ∧ argument.stepRule? .deriveCrossSectionFormula = some ([.crossSectionResult], .crossSectionFormula) ∧ argument.stepRule? .deriveAccuracyResult = some ([.effectiveRangeResult, .correctionCalculation, .curvatureDiagnostic, .shapeInterpretation], .accuracyResult) ∧ argument.stepRule? .deriveTripletResult = some ([.effectiveRangeResult, .tripletSetup, .tripletCalculation], .tripletResult) ∧ argument.stepRule? .deriveSingletAssessment = some ([.singletLimitation, .singletBorrowing], .singletAssessment) ∧ argument.stepRule? .deriveCoulombSourceFormula = some ([.coulombSetup, .coulombCalculation], .coulombSourceFormula) ∧ argument.stepRule? .deriveCoulombResult = some ([.coulombSourceFormula, .coulombRangeReplacement, .coulombIdentification], .coulombResult) ∧ argument.stepRule? .deriveCoulombNeutralization = some ([.coulombSourceFormula, .coulombResult, .coulombNeutralizationCalculation], .coulombNeutralizationResult) ∧ argument.stepRule? .deriveCoulombThreshold = some ([.coulombThresholdSetup, .coulombThresholdRegularity], .coulombThresholdResult) ∧ argument.stepRule? .deriveProtonResult = some ([.coulombResult, .protonSetup, .protonFit, .highEnergyAssessment], .protonResult) ∧ argument.stepRule? .deriveChargeResult = some ([.protonResult, .chargeEstimateResult, .singletAssessment, .chargeCalculation, .chargeInterpretation], .chargeResult) ∧ argument.stepRule? .deriveChargeWeightedResult = some ([.chargeSetup, .chargeWeightedCalculation], .chargeWeightedResult) ∧ argument.stepRule? .deriveChargeEstimate = some ([.chargeWeightedResult, .coulombSourceFormula, .protonResult, .chargeReadoutCalculation], .chargeEstimateResult) ∧ argument.stepRule? .deriveChargeShapeAssessment = some ([.chargeShapeExpectation, .chargeShapeErrorBudget], .chargeShapeResult) := by repeat' apply And.intro all_goals rfl theorem neutral_result_depends_on_equations_7_10_11_13_and_14 : argument.stepRule? .deriveNeutralRadialFormulaReadout = some ([.neutralSetup, .neutralFormulaCalculation], .neutralFormulaReadout) ∧ argument.stepRule? .deriveNeutralResult = some ([.neutralSetup, .neutralCalculation, .neutralFormulaReadout], .neutralResult) ∧ argument.ClaimReliesOnStep .neutralResult .deriveNeutralRadialFormulaReadout := by native_decide theorem cross_section_accuracy_and_triplet_are_siblings_after_reduction : crossSectionRoute.dependsOn = [.effectiveRangeReduction] ∧ accuracyRoute.dependsOn = [.effectiveRangeReduction] ∧ tripletRoute.dependsOn = [.effectiveRangeReduction] ∧ .neutralCrossSection ∉ accuracyRoute.dependsOn ∧ .accuracyAndShape ∉ crossSectionRoute.dependsOn := by native_decide theorem singlet_borrowing_route_keeps_limitation_and_borrowing_distinct : argument.stepRule? .supplySingletBorrowing = some ([], .singletBorrowing) ∧ argument.stepRule? .deriveSingletAssessment = some ([.singletLimitation, .singletBorrowing], .singletAssessment) ∧ argument.ClaimReliesOnStep .singletAssessment .supplySingletBorrowing := by native_decide theorem accuracy_route_keeps_curvature_diagnostic_distinct : argument.stepRule? .interpretCurvatureDiagnostic = some ([], .curvatureDiagnostic) ∧ argument.stepRule? .interpretShapeSensitivity = some ([], .shapeInterpretation) ∧ argument.stepRule? .deriveAccuracyResult = some ([.effectiveRangeResult, .correctionCalculation, .curvatureDiagnostic, .shapeInterpretation], .accuracyResult) := by native_decide def neutral_descendant_routes_consume_certified_outputs : Prop := argument.ClaimReliesOnStep .effectiveRangeResult .deriveNeutralResult ∧ argument.ClaimReliesOnStep .crossSectionResult .deriveEffectiveRangeResult ∧ argument.ClaimReliesOnStep .accuracyResult .deriveEffectiveRangeResult ∧ argument.ClaimReliesOnStep .tripletResult .deriveEffectiveRangeResult def charged_descendant_routes_consume_certified_outputs : Prop := argument.ClaimReliesOnStep .coulombResult .deriveCoulombSourceFormula ∧ argument.ClaimReliesOnStep .coulombNeutralizationResult .deriveCoulombSourceFormula ∧ argument.ClaimReliesOnStep .coulombNeutralizationResult .deriveCoulombResult ∧ argument.ClaimReliesOnStep .protonResult .deriveCoulombResult ∧ argument.ClaimReliesOnStep .chargeResult .deriveProtonResult ∧ argument.ClaimReliesOnStep .chargeResult .deriveSingletAssessment ∧ argument.ClaimReliesOnStep .chargeEstimateResult .deriveChargeWeightedResult ∧ argument.ClaimReliesOnStep .chargeEstimateResult .deriveCoulombSourceFormula ∧ argument.ClaimReliesOnStep .chargeEstimateResult .deriveProtonResult ∧ argument.ClaimReliesOnStep .chargeResult .deriveChargeEstimate def complete_route_consumes_certified_outputs : Prop := argument.ClaimReliesOnStep .completeResult .deriveNeutralResult ∧ argument.ClaimReliesOnStep .completeResult .deriveEffectiveRangeResult ∧ argument.ClaimReliesOnStep .completeResult .deriveCrossSectionAssessment ∧ argument.ClaimReliesOnStep .completeResult .deriveAccuracyResult ∧ argument.ClaimReliesOnStep .completeResult .deriveTripletResult ∧ argument.ClaimReliesOnStep .completeResult .deriveSingletAssessment ∧ argument.ClaimReliesOnStep .completeResult .deriveCoulombResult ∧ argument.ClaimReliesOnStep .completeResult .deriveCoulombNeutralization ∧ argument.ClaimReliesOnStep .completeResult .deriveCoulombThreshold ∧ argument.ClaimReliesOnStep .completeResult .deriveProtonResult ∧ argument.ClaimReliesOnStep .completeResult .deriveChargeResult ∧ argument.ClaimReliesOnStep .completeResult .deriveChargeWeightedResult ∧ argument.ClaimReliesOnStep .completeResult .deriveChargeEstimate ∧ argument.ClaimReliesOnStep .completeResult .deriveChargeShapeAssessment ∧ argument.ClaimReliesOnStep .completeResult .stateScopeQualifications private theorem neutral_descendant_routes_consume_certified_outputs_hold : neutral_descendant_routes_consume_certified_outputs := by unfold neutral_descendant_routes_consume_certified_outputs native_decide private theorem charged_descendant_routes_consume_certified_outputs_hold : charged_descendant_routes_consume_certified_outputs := by unfold charged_descendant_routes_consume_certified_outputs native_decide private theorem complete_route_consumes_certified_outputs_hold : complete_route_consumes_certified_outputs := by unfold complete_route_consumes_certified_outputs native_decide theorem dependent_routes_consume_certified_predecessor_outputs : neutral_descendant_routes_consume_certified_outputs ∧ charged_descendant_routes_consume_certified_outputs ∧ complete_route_consumes_certified_outputs := by exact ⟨neutral_descendant_routes_consume_certified_outputs_hold, charged_descendant_routes_consume_certified_outputs_hold, complete_route_consumes_certified_outputs_hold⟩ theorem effective_range_result_retains_approximate_status : argument.ClaimReliesOnJustification .effectiveRangeResult .controlledApproximation := by decide theorem effective_range_result_retains_identification_bridge : argument.ClaimReliesOnJustification .effectiveRangeResult .interpretiveInference := by decide theorem cross_section_result_retains_calculation_and_truncation_warning : argument.ClaimReliesOnJustification .crossSectionResult .paperDerivation ∧ argument.ClaimReliesOnJustification .crossSectionResult .interpretiveInference := by decide theorem cross_section_route_exposes_equation_seventeen_formula : crossSectionRoute.outputs = [.crossSectionResult, .crossSectionFormula] ∧ argument.stepRule? .deriveCrossSectionFormula = some ([.crossSectionResult], .crossSectionFormula) ∧ argument.ClaimReliesOnStep .crossSectionFormula .deriveCrossSectionAssessment := by native_decide theorem accuracy_result_retains_shape_interpretation : argument.ClaimReliesOnJustification .accuracyResult .interpretiveInference := by decide theorem the_exact_coulomb_formula_does_not_use_either_range_approximation : argument.ClaimReliesOnStep .coulombSourceFormula .supplyCoulombCalculation ∧ ¬argument.ClaimReliesOnStep .coulombSourceFormula .supplyCoulombRangeReplacement ∧ ¬argument.ClaimReliesOnStep .coulombSourceFormula .supplyCoulombNeutralization ∧ argument.ClaimReliesOnStep .coulombResult .supplyCoulombRangeReplacement := by native_decide theorem neutralization_retains_two_independent_approximation_inputs : argument.ClaimReliesOnStep .coulombNeutralizationResult .supplyCoulombRangeReplacement ∧ argument.ClaimReliesOnStep .coulombNeutralizationResult .supplyCoulombNeutralization ∧ argument.ClaimReliesOnJustification .coulombNeutralizationResult .controlledApproximation ∧ ¬argument.ClaimReliesOnStep .coulombResult .supplyCoulombNeutralization := by native_decide theorem threshold_regularity_is_not_an_empirical_fit_or_range_replacement : coulombThresholdRoute.dependsOn = [] ∧ argument.ClaimReliesOnStep .coulombThresholdResult .supplyCoulombThresholdRegularity ∧ argument.ClaimReliesOnJustification .coulombThresholdResult .importedResult ∧ ¬argument.ClaimReliesOnStep .coulombThresholdResult .supplyCoulombRangeReplacement ∧ ¬argument.ClaimReliesOnStep .coulombThresholdResult .supplyProtonFit ∧ ¬argument.ClaimReliesOnStep .protonResult .deriveCoulombThreshold := by native_decide theorem proton_result_retains_empirical_status : argument.ClaimReliesOnJustification .protonResult .importedResult := by decide theorem high_energy_assessment_retains_open_status : argument.ClaimReliesOnJustification .highEnergyAssessment .openObligation := by decide theorem charge_result_retains_approximate_and_interpretive_status : argument.ClaimReliesOnJustification .chargeResult .controlledApproximation ∧ argument.ClaimReliesOnJustification .chargeResult .interpretiveInference := by decide theorem charge_route_uses_singlet_qualification_without_triplet_extraction : chargeRoute.dependsOn = [.chargeEstimate, .protonExperiment, .singletRangeQualification] ∧ .tripletExtraction ∉ chargeRoute.dependsOn := by decide theorem weighted_charge_comparison_is_independent_of_fits_and_unweighted_range_control : chargeWeightedRoute.dependsOn = [] ∧ argument.ClaimReliesOnStep .chargeWeightedResult .supplyChargeWeightedCalculation ∧ ¬argument.ClaimReliesOnStep .chargeWeightedResult .supplyProtonFit ∧ ¬argument.ClaimReliesOnStep .chargeWeightedResult .supplyCoulombNeutralization ∧ ¬argument.ClaimReliesOnStep .chargeWeightedResult .supplyChargeReadoutCalculation := by native_decide theorem charge_estimation_and_force_interpretation_retain_separate_inputs : argument.ClaimReliesOnStep .chargeEstimateResult .deriveChargeWeightedResult ∧ argument.ClaimReliesOnStep .chargeEstimateResult .deriveCoulombSourceFormula ∧ argument.ClaimReliesOnStep .chargeEstimateResult .supplyChargeReadoutCalculation ∧ argument.ClaimReliesOnStep .chargeResult .supplyChargeCalculation ∧ argument.ClaimReliesOnStep .chargeResult .interpretChargeDependence ∧ ¬argument.ClaimReliesOnStep .chargeEstimateResult .interpretChargeDependence := by native_decide theorem shape_extrapolation_is_conditional_on_an_author_expectation_not_a_computed_model : chargeShapeRoute.dependsOn = [] ∧ argument.ClaimReliesOnJustification .chargeShapeResult .authorExpectation ∧ argument.ClaimReliesOnStep .chargeShapeResult .supplyChargeShapeErrorBudget ∧ ¬argument.ClaimReliesOnStep .chargeResult .stateChargeShapeExpectation ∧ argument.ClaimReliesOnStep .completeResult .deriveChargeShapeAssessment := by native_decide theorem complete_result_retains_deferred_scope : argument.ClaimReliesOnJustification .completeResult .deferredCalculation := by decide theorem complete_result_relies_on_every_substantive_route : argument.ClaimReliesOnStep .completeResult .deriveNeutralResult ∧ argument.ClaimReliesOnStep .completeResult .deriveEffectiveRangeResult ∧ argument.ClaimReliesOnStep .completeResult .deriveCrossSectionAssessment ∧ argument.ClaimReliesOnStep .completeResult .deriveAccuracyResult ∧ argument.ClaimReliesOnStep .completeResult .deriveTripletResult ∧ argument.ClaimReliesOnStep .completeResult .deriveSingletAssessment ∧ argument.ClaimReliesOnStep .completeResult .deriveCoulombResult ∧ argument.ClaimReliesOnStep .completeResult .deriveCoulombSourceFormula ∧ argument.ClaimReliesOnStep .completeResult .deriveCoulombNeutralization ∧ argument.ClaimReliesOnStep .completeResult .deriveCoulombThreshold ∧ argument.ClaimReliesOnStep .completeResult .deriveProtonResult ∧ argument.ClaimReliesOnStep .completeResult .deriveChargeResult ∧ argument.ClaimReliesOnStep .completeResult .deriveChargeWeightedResult ∧ argument.ClaimReliesOnStep .completeResult .deriveChargeEstimate ∧ argument.ClaimReliesOnStep .completeResult .deriveChargeShapeAssessment ∧ argument.ClaimReliesOnStep .completeResult .stateScopeQualifications := by repeat' apply And.intro all_goals decide end PhysicsLogic.Papers.Bethe1949