Formal reconstruction · Large scattering length, PDS resummation, explicit pions, renormalization-scale cancellation, fits, and coupled channels
A New Expansion for Nucleon-Nucleon Interactions
Why an unnaturally large scattering length requires a resummed leading contact, how pion and counterterm effects enter at subleading order, and where empirical success ceases to certify truncation control
Definitions, structures, and assumptions
Structures, classes, and inductive alternatives
- structureA description together with the calibration used to fix its selected input.
- structureSource-sensitive structural-explanation constraint for one selected large-length resummation. It keeps the proof-free physical source description, one typed paper derivation, and its proposition-valued realization relation, but no resummation or recovery output.
- structureThe selected large-length two-body description before target recovery.
- structureProof-free semantics selected by one large-scattering-length resummation argument. Besides the five selected physical objects, the model retains every relation family used by the shared route. It stores no proof that the regime is controlled, resummation is required, or the target amplitude is recovered.
- inductive
- structureShared semantics for the repeated large-length route. Validity is scoped to the selected system-momentum pair. The exact meaning of the resummed object and recovered target remains paper-local.
- structure
- structure
- structure
- structureValue-bearing boundary data for separating an established post-calibration prediction from empirical agreement. Calibration and target-calculation residuals remain distinct from the predicted/observed target values, observation tolerance, and admitted truncation uncertainty.
- inductive
- structureProof-free constraint selecting one exact post-calibration prediction model. It stores no route-applicability, target-calculation, or prediction proof.
- structureShared semantics for a target predicted only after a distinct calibration. Each paper supplies the physical meanings of descriptions, calibrations, targets, regimes, and all five relation families.
- structureSource-sensitive constraint pairing the exact selected model with one typed paper-local derivation and its proposition-valued realization relation. It contains no proof that the derivation or shared route obtains.
- structureExplicit interpretation of one technical prediction model in a containing theory and represented physical system.
- structureProof-free data selected from one post-calibration prediction argument. The model retains all four selected indices and all five proposition-valued relation families used by the shared route. It stores no proof that the description is valid, that the calibration fixes an input, or that the target is predicted.
- structureThe situated calibrated-description/uncalibrated-target phenomenon explained by the shared route. Its four selected objects are data, not predictions.
- structure
- structure
- inductiveThe target and scale-dependent effective descriptions remain distinct from the physical system they may represent.
- structureExact proof-free semantics selected by one renormalized-prediction route. Every field is data, a function, or a proposition-valued relation. No field stores a setup proof, calculation result, bridge, or desired conclusion.
- inductiveEvery proposition retained by the shared technical and empirical routes.
- structureProof-free constraint selecting one exact renormalized-prediction model. It stores no route applicability, calculation result, or established endpoint.
- structurePaper-local vocabulary and the exact physical indices selected for one route. The context determines a unique proof-free calculation model below.
- structureThe selected model constraint together with one typed paper-local derivation. The proposition-valued source relation stores no proof and keeps distinct renormalization arguments from collapsing into one anonymous calculation.
- structurePaper-local empirical interpretation. Matching two predictions does not by itself assert that either description represents a physical system.
- structureThe situated system/target/sector phenomenon explained by a renormalization route. Its fields are selected physical data, not prediction proofs.
- structureThe containing theory is distinct from its selected calculation model.
- structurePaper-local meanings for theory use, world representation, and claims.
- structureThe represented physical world is distinct from model and theory.
- structureThe resummed object together with the low-energy behavior it recovers.
- structureProof-free handoff from a selected nonperturbative two-body sector to a later renormalized prediction. The two system types, selected regimes, and output descriptions need not coincide: KSW extends a pionless PDS sector to a pion-inclusive amplitude, while BHvK inserts a dressed two-boson propagator into a cutoff-sensitive three-body problem.
- structure
- structure
- structure
- inductive
- inductive
- inductive
- structure
- inductive
- structure
- structureA selected claim must depend on exactly these source-map steps.
- structureA selected claim must retain exactly these epistemic statuses.
- structureA selected route must name exactly these immediate predecessor routes.
- structure
- structure
- inductive
- inductive
- inductive
- structureValue-level content of KSW's displayed coupled-channel S-matrix relation. The readout keeps the momentum-dependent amplitude matrix, `S - 1` matrix, and the three real phase observables separate. Its formula below retains the printed complex matrix literally. Phase extraction below is derived from it on an explicit zero-centered branch, not supplied as a desired conclusion.
- inductiveTyped name for KSW's pionless PDS resummation derivation.
- inductiveTyped name for KSW's coupled-channel post-calibration prediction route.
- inductiveTyped name for KSW's pion-inclusive running-plus-matching route.
- inductiveTyped name for the paper's actual pionless-to-pion-inclusive handoff.
- structure
- structure
- structure
- structure
- structureA named equation-(11) running-solution output does not itself supply the two displayed coupling values. This blocks replacing the value-level formulas by an uninspected label.
- inductive
- inductive
- inductive
- inductive
- inductive
- inductive
- structureSeven real data: M,gA,f and the four scale functions c,s,r,d. The existing coupling record is reused as data only, not as an assertion of its nominal beta equations.
- structureFormal coefficients, indexed by power n - 1. In particular indices 0 and 1 retain p^-1 and p^0. This is not a convergent series or a remainder bound.
- structure
- inductive
- structureRunning couplings in the retained pion-inclusive calculation. These are not identified with an all-orders physical flow.
- structureThe physical scattering problem selected by the shared RG route.
- structureThe two pionless terms in printed equation (13), p. 5. The author TeX uses label `14`; it is not the printed equation number. No pion contribution or convergence of the full asymptotic expansion is asserted by this readout.
- structureValue-level content of the original pionless PDS equations (4) and (5). The readout keeps the on-shell energy, subtraction scale, momentum, contact polynomial, PDS loop family, and resummed amplitude distinct. Complex-valued formulae are retained literally; loop integration, analytic continuation, and bubble summation remain imported calculations rather than fake Lean proofs of the paper's analysis. The legacy API names EquationFivePDSLoopAt and EquationSixPDSAmplitudeAt are retained for compatibility; their printed v2 source numbers are (4) and (5), not their historical Lean identifiers.
- structureThe two-nucleon channel and PDS subtraction scale selected by the pionless resummation route. The count distinguishes the paper's NN problem from an anonymous channel-scale pair while the scale remains explicit calculation data rather than being hidden in a closure.
- structureReal subtraction-scale families for the pionless equations (9)-(11). The inverse scattering length is primitive, as in the contact-chain argument: zero denotes the unitary limit, not zero scattering length. No derivative, beta equation, or selected solution is stored as a proof field.
- structure
- structure
- structure
- inductive
- inductive
- inductive
- inductive
- inductive
- structure
- structure
- structureA physical interpretation of a prediction context. `describes` and `obtains` are relations, not proof fields asserting that a chosen description is adequate.
- structurePredictions made by descriptions in regimes. `predicts` is relational so the signature can represent deterministic values, sets of allowed values, or probabilistic outputs without choosing among them.
- structure
Definitions and domain choices
- definition
- definition
- definitionThe quadratic limit also determines the constant coefficient on the positive-momentum approach. No value at zero or extra continuity is required.
- definition
- definition
- definitionThe interference term in the elastic optical theorem, at first order in an amplitude correction. It is not exact unitarity of their sum.
- definitionThe positive-momentum finite real inverse-amplitude chart. Unitarity is derived from this formula, not supplied as a second physical restriction. The zero amplitude is outside this chart; the contact formula includes it.
- definition
- definitionA real contact coefficient in a subtraction scheme can vanish. Its amplitude therefore has a separate nonsingular formula instead of forcing the inverse-amplitude parameterization through a zero of the amplitude.
- definitionOne derivative contact, dressed on both sides by the leading bubble chain. The coefficient includes its selected powers of external momentum.
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definitionThe selected derivational reduction uses the same physical specification as the nonvacuous resummation result. The equivalence below reconstructs the universal bridge, actual realization, support, and recovered behavior; they are not separately maintained physical conditions.
- definitionSource-sensitive reduction adds realization of the selected derivation to the shared physical result, without duplicating the realization adapter.
- definitionThe actual selected large-length setup at one proof-free model. This is model-native rather than implication-valued: validity and the anomalously large two-body length both hold at the model's own selected data.
- definitionThe complete realized large-scattering-length resummation result at one proof-free model. This direct proposition is stronger than the implication-valued calculation contracts: the selected system-momentum pair is actually valid in the selected large-length regime, all-order resummation is actually required for the selected description, that description is actually obtained, and it actually recovers the selected low-energy target.
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definitionSource-sensitive structural constraint selected by this model.
- definitionThe exact source-side description selected by this resummation model.
- definitionThe resummed behavior whose recovery is established by the route.
- definition
- definition
- definition
- definition
- definitionSource-sensitive structural explanation of one selected resummation.
- definitionOrdinary structural explanation of one selected resummation route.
- definitionThe selected direct result. Calculation contracts are reconstructed from the realized requirement, obtained description, and recovered target rather than stored in this endpoint.
- definitionThe selected route viewed as a nonvacuous derivational reduction.
- definition
- definition
- definition
- definition
- definition
- definitionThe complete raw route at one exact model. This model-native form prevents a candidate with copied index fields but changed relation families from borrowing the route of the context-owned selected model.
- definitionExact selected semantics together with the inhabited pre-calculation setup.
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definitionThe unique model fixed by the context's five selected physical objects.
- definition
- definition
- definition
- definition
- definitionSource-sensitive structural semantics for one selected resummation route. The source constraint adds a typed paper-local derivation and its raw realization relation without storing an established endpoint, ordinary explanation, or derivational-reduction result.
- definitionOrdinary structural semantics for one selected large-length resummation route. Satisfaction retains the proof-free physical source description and complete raw route; the explained phenomenon is the actually recovered resummed low-energy behavior. This is distinct from the derivational reduction relation below.
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definitionThe selected calibration and the separate target calculation both close.
- definitionAgreement of the predicted and observed target within explicitly retained measurement and truncation allowances.
- definitionA completed prediction whose discrepancy exceeds both admitted allowances.
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definitionThe established result is output-led: it retains exact selected semantics and the direct inhabited calibration-and-prediction endpoint. The implication-valued calculation and complete route can be reconstructed from that endpoint, but are not stored as premises of the result.
- definition
- definition
- definitionThe selected model retains the context-owned objects and exactly all five proposition-valued relation families.
- definitionThe pre-calibration boundary for interpreting a post-calibration model in a theory and represented world. It fixes the exact context-selected model and requires that its paper-local description be valid in the selected regime, without assuming a completed fit, target exclusion, parameter freedom, or the target prediction.
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definitionThe unique model fixed by the context's four selected physical objects.
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definitionThe selected calibrated description makes an actual target prediction.
- definitionThe empirical readout retains the exact selected description, calibration, target, and regime and is tied to the inhabited validity, calibration, target-exclusion, no-extra-input, and target-prediction facts of one model. No observational agreement is included in this bridge.
- definitionDirect physical content of one post-calibration prediction. Unlike the implication-valued target calculation, this proposition requires the valid description, completed calibration, excluded target, no-additional-calibration claim, and target prediction to hold together at one actual model.
- definition
- definitionThe target calculation is implication-valued so imported mathematics can remain an explicit theorem parameter. It becomes usable only together with the complete setup.
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definitionThe selected description together with the input-fixing calibration.
- definitionThe exact proof-free constraint selected by this prediction model.
- definitionThe selected source-sensitive version of the prediction constraint.
- definitionThe exact situated phenomenon selected by this prediction model.
- definitionThe singleton observable sector containing the selected prediction target.
- definition
- definition
- definition
- definitionNeutral prediction semantics for one completed post-calibration route. The target is in the active sector only when the description is valid, the selected calibration is completed, the target was not used in that calibration, and no additional calibration is required. The prediction relation separately requires the actual paper-local target calculation.
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definitionDirect physical content of one renormalized prediction. Unlike the implication-valued calculation bridges, this proposition requires the selected setup, both paper-local calculations, an actual target prediction, running parameters, all-scale matching, and a witnessed scale-independent effective prediction to hold together at one model.
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definitionThe proof-free constraint selected by one calculation model.
- definitionThe selected constraint plus one typed paper-local derivation relation.
- definitionThe proof-free situated phenomenon selected by one calculation model.
- definition
- definition
- definition
- definition
- definition
- definition
- definitionInterpret the matching calculation as agreement at every selected scale.
- definition
- definitionSource-sensitive structural explanation of one selected renormalized prediction. The source relation is independent of the completed endpoint.
- definitionOrdinary structural explanation of one selected renormalized prediction.
- definition
- definitionEmpirical grounding is independent of the technical calculations.
- definitionThe stronger result retains the complete technical route and the independent empirical grounding route, then establishes adequacy at every selected scale and physically grounded scale independence.
- definitionDirect established content; implication-valued bridges are reconstructed.
- definition
- definitionInterpret the paper-local flow calculation as nonconstant parameters.
- definition
- definitionThe scale-independent prediction is physically grounded only after the target is empirically adequate and every effective description represents the same system and is empirically adequate there.
- definition
- definition
- definition
- definition
- definitionExact selected semantics together with the inhabited pre-calculation setup.
- definition
- definition
- definition
- definition
- definitionThe complete proof-free model fixed by this context.
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definitionAn actually composed EFT route retains the direct two-body result, the independent subsystem/calculation handoff, and the direct renormalized prediction. Neither completed endpoint alone identifies the intermediate paper-local physics.
- definitionThe selected two-body sector is relevant to the later prediction system.
- definitionActual paper-local use of the obtained two-body description and recovered low-energy target in the separate renormalization calculation.
- definitionThe actual two-body and scale-independent results coexist with all three independent source derivations and exact selection of both child contexts.
- definitionBoth exact child contexts retain their independent paper-local source explanations. A third derivation separately establishes how the obtained two-body input enters the selected renormalization calculation.
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definitionImmediate predecessor routes. Claims established by their transitive predecessors are inherited by the dependency closure.
- definition
- definition
- definition
- definition
- definition
- definitionTemporary reductio-introduction steps discharged by this inference. Discharge removes only those exact origins from the conclusion's epistemic basis; it does not assert the temporary hypotheses globally.
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definitionA source-mapped claim holds when its declared formula evaluates under the given paper-local semantic interpretation.
- definition
- definition
- definition
- definition
- definitionEvery claim in the supplied identifier list holds.
- definitionA source-mapped step is semantically sound when the interpreted premises imply the interpreted conclusion. Physical principles and imported calculations therefore remain explicit hypotheses of paper-specific certificates rather than acquiring truth from their source-map labels. A reductio hypothesis is different: it introduces a temporary assumption into a subargument and therefore is not required to hold globally. Its later uses remain ordinary premise-sensitive steps, and discharging it into a negated conclusion remains an ordinary semantic obligation.
- definitionEvery step in the supplied identifier list is semantically sound.
- definition
- definition
- definition
- definition
- definition
- definitionThe formula declared for a claim identifier, when that claim is present.
- definition
- definitionEvery source-mapped step whose justification contributes to the claim through declared premise-to-conclusion steps.
- definitionAll justification statuses contributed by the exact source-mapped origins of a claim. This records epistemic provenance; it does not assert any paper claim or discharge any physical assumption.
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definitionThe declared argument step with the requested identifier, when present.
- definition
- definitionThe premise list and conclusion attached to a declared step identifier.
- definition
- definition
- definition
- definition
- definitionThe complete Lean-side fidelity certificate. The first conjunct is computed from source-map data; the second is supplied by checked route semantics; the third requires each declared independence boundary to have a countermodel.
- definition
- definition
- definition
- definition
- definitionA typed countermodel matrix avoids string-keyed audit rows. Each index selects one proposition-valued separation obligation.
- definition
- definitionEvery route actually declared in the source map has a semantic certificate under the paper-local interpretation.
- definition
- definition
- definitionOne countermodel row retains a weaker proposition while rejecting a stronger upgrade. This is a proposition, not a structure carrying proof fields.
- definition
- definition
- definitionIndependent dependency and epistemic ledgers must review the same actual source claims, including every public conclusion and the selected paper conclusion. Empty, duplicated, nonexistent, or one-sided entries are invalid.
- definitionEvery actually declared source route must have exactly one independently reviewed predecessor row. Correct rows for a selected subset are insufficient.
- definitionThe declared main conclusion must be exposed by at least one public route output, rather than existing only as an unexported source-map claim.
- definition
- definition
- definitionTwo finite lists describe the same dependency set. Duplicate expected entries are rejected so a ledger cannot pass by repeating a label.
- definitionEvery paper-level, claim-level, and step-level source reference is present and has a nonempty work and locator. PaperArgument.auditable separately checks that every claim and step carries at least one source.
- definitionA source reference is usable for review only when both the work and its locator are nonempty.
- definitionStatic fidelity checks that can be evaluated from a paper's source map alone. They do not assert the truth of any physical premise.
- definitionEvery declared output of a named source route holds under the semantic interpretation. This is the proof obligation discharged by paper-specific Lean theorems.
- definition
- definitionA route is fully certified only when both its individual steps and its declared outputs are semantically checked.
- definitionEvery source-mapped inference step in a named route is semantically sound.
- definitionEvery route named in the supplied identifier list is semantically certified.
- definition
- definition
- definition
- definition
- definition
- definitionThe source-mapped route with the requested identifier, when present.
- definition
- definitionThe public semantic interface inherited from predecessor routes. Descendants receive only declared route outputs, not every internal intermediate claim. Outputs still carrying a temporary reductio origin are excluded.
- definitionAll direct and inherited route dependencies. The route-order check separately ensures that the declared graph is acyclic and topologically ordered.
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definitionThe reduced amplitude of one ordered chain after the PDS loop calculation. The physical domain and the exclusion of the empty list are theorem premises.
- definitionThe shared treatment API generated by the retained chain sector, rather than supplied as independent flags. An index labels an allowed interaction, including one whose coefficient vanishes. The supplied coefficient jet ends at last: contribution, retention and treatment do not certify unsupported indices. Required chains contain only supplied indices. A false predicate outside this scope is not a physical classification of that interaction. Contribution and retention are scoped through the first correction. Suppression compares the calculated resummed leading term and once-inserted correction, not bare vertices or every pair of higher interactions. Its numerical validity is proved below. The derivative grade is justified by the actual chain identity and matching bounds above; it is not an assertion of exact nonzero asymptotic orders. Source: the pionless expansion between author TeX labels 11 and 14.
- definitionInterpretation of the existing treatment API through order p^0. A contact's contribution grade is the order of its vertex C_(2n) p^(2n), not every order of a chain containing it. The latter would assign C0 both grades -1 and 0 when it dresses C2 and confuse an interaction with a graph. Retention instead asks whether a chain containing the contact is required at the requested order, restricted to q <= 0. No interpretation of higher-order API labels is required: all higher contacts still occur in the chain test and are excluded at this retained order by enhanced counting. Resummed means unbounded required occurrences, while perturbative means a finite insertion bound. These are order-completeness meanings, not numerical convergence, actual evaluation of a sum, or error control. Order comparison and physical suppression in the broader API are deliberately not asserted here.
- definitionOrder of the vertex product and k-1 loops of a nonempty contact chain. The empty list is not a physical chain; physical statements exclude it.
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definitionFirst allowed phase degree in the expansion around the resummed S-wave background. Degree n corresponds to amplitude order p^(n-1), not a Taylor expansion in momentum at fixed pion mass. Mixing and D-wave phases vanish at degree zero; their leading prediction requires degree one. Coefficients may still vanish. This is relative accuracy, not the amplitude's order label.
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definitionA positive-momentum phase readout can retain the complete printed phase matrix, including the symmetric off-diagonal entries, while failing to bind that matrix to the scattering-amplitude normalization. A phase-output label therefore cannot replace the full coupled S-matrix relation.
- definition
- definitionAuthor TeX lines 495-501: `S - 1 = i p M A / (2 pi)` equals the displayed two-by-two phase-shift matrix. The equality is retained componentwise over the momentum family for the selected coupled channel and declared order.
- definition
- definitionA sufficient local choice of real phase representatives for the leading zero-phase statement in author TeX lines 504-510. The source does not specify these intervals: they expose our convention, not an extra quoted source claim. No restriction on the S-wave phase or division by momentum is needed.
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definitionThe four entries on the right-hand side of KSW's displayed matrix: `exp(2 i delta_0) cos(2 epsilon_1) - 1`, `i exp(i(delta_0 + delta_2)) sin(2 epsilon_1)`, its symmetric partner, and `exp(2 i delta_2) cos(2 epsilon_1) - 1`.
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definitionPrinted equation (5), author TeX label 6: sum the required bubble chain using the PDS-subtracted loop.
- definitionKSW's parenthetical after the numerical fit does not identify the two quoted couplings separately. Through the computed order, the amplitude can instead be written using the `C0 + D2 m_pi^2` combination; this is the explicit bridge to the paper's non-separate-meaning qualification.
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definitionKSW's displayed coupled-channel S-matrix formula, retained at the selected coupled channel and declared order before it is used to extract leading phase zeros.
- definition
- definition
- definitionThe explicit-pion calculation at momentum of order the pion mass. The D2 operator is required at the same order as one-pion exchange. The retained coefficient formulas and their interpretation are supplied; their with/without scale-invariance verdicts and nonzero retained insertion are derived downstream. The same contact values serve the whole declared pion-scale momentum family; they cannot be selected afresh for the momentum at this source-route call. The two abstract order assignments remain explicit interpretation inputs.
- definitionThe authors interpret the expected fitted coupling sizes as channel-scoped support for the expansion. This bridge is distinct from the numerical fit.
- definition
- definitionRaw paper-local inputs constituting KSW's pionless PDS derivation. The token retains the low-momentum and large-length setup, PDS subtraction, the selected leading-contact and loop exponents, loop calculation, bubble sum, and unitarity recovery. Unbounded leading bubble content is derived from the two exponents; their physical scaling interpretation is still an input. No shared endpoint or independently assignable bubble requirement is stored.
- definition
- definitionFor an unnaturally large scattering length at `mu = 0`, the source requires the narrower window `p << 1 / |a|`; it does not supply a converse theorem of full EFT accuracy. The range calculation supplies a necessary condition over the selected pionless domain and an actual momentum outside that window. The excluded-validity conclusion is then derived by contraposition.
- definitionThe enhanced-regime inputs now identify the contact/order labels with the explicit diagram interpretation and supply the two displayed amplitude formulas as a separate bubble-sum calculation. The mixed treatment conclusion is no longer an imported output. The API interpretation is required only through the first correction, not at every higher order. It commits to assigned enhanced orders; validity of higher-contact scaling and quantitative omitted terms are not derived by this contract.
- definitionThe displayed coupled-channel S-matrix and a sufficient local phase convention. The amplitude-zero to phase-zero implication is derived, not assumed here.
- definitionFor a natural scattering length, ordinary minimal subtraction supports the usual perturbative momentum expansion when `p / Lambda` is small.
- definitionPrinted equations (3)-(4): subtract the three-dimensional pole and retain the PDS-subtracted loop formula. Its zero-power instance is derived downstream. The channel index is retained for the source-route API; the imported formula already quantifies over all channels in the selected readout.
- definitionCompatibility statement for the former agreement input. Agreement is now derived from the coefficients, so this statement needs no extra input.
- definitionThe four observed retained coefficients of the projected printed-equation-(15) calculation. This does not choose a different jet at each momentum.
- definitionIdentification of nominal graph V, separate from the formal coefficient condition used for computed-order scale cancellation.
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definitionPointwise identification of the singlet formal coefficients with the projected printed-equation-(15) calculation. The nominal running couplings are not equated with their leading grades. The scale domain is the actual image of the framework's scale map, not a second freely chosen set. Its open connected extent remains an input; a one-point sample cannot satisfy this contract. Only four graded contact values at the interacting witness scale are chosen. Their running is reconstructed, with the pole excluded on the actual scale image; the physical constants come from the existing framework.
- definitionOne EFT uses one reference scale and one set of graded contact values throughout its declared pion-scale momentum family. The existential choice is outside the momentum quantifier. This is stronger than separately valid pointwise calculations; no all-momentum EFT validity is asserted.
- definitionContact calibration and its physical readout on a realized momentum family. mu is held fixed while p approaches zero. The same sampled observable is used for all mu; its ERE coefficients are supplied by the separate, nonvacuous `effectiveRangeDataMatched` input, not a free remainder. The normalized contact is the canonical -1/(K+mu), not a second freely selected family. Its threshold coefficients identify the actual couplings; the final clause identifies the physical contact readout with this function. Pionless coupling samples are evaluations of the real functions, not additional data identified with pion-inclusive couplings. No running-solution formula or beta equation occurs here. The observable coefficient condition and nonzero scattering length reside in `effectiveRangeDataMatched`. At each nonpole scale they also imply an eventually nonzero contact denominator, so neither condition is duplicated here. This contact-only contract must not substitute for observable matching. No uniform EFT error or naturalness bound is asserted.
- definitionThe mass, subtraction scale and momentum are the existing selected values by construction, not independent data with equality obligations. The two remaining interpretation obligations concern the energy and contact interaction. The loop and PDS amplitude are the concrete complex-valued readouts, without abstract mirrors. Numerical agreement does not discharge the remaining physical identifications or establish applicability to a nuclear system.
- definitionThe effective-range matching and RG calculation following equations (7)-(11). It supplies observable/contact families rather than the desired equation-(11) values. Those values and actual derivatives are derived from the families. Full-amplitude scale independence remains an imported output: a threshold identity alone does not constrain an arbitrary prediction momentum. There is no parallel abstract beta or running-solution output to supply independently.
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definitionThe source's elastic-channel and observable normalization, consuming the previously obtained bubble formula. The real observable is the finite phase function p cot(delta), with its inverse-amplitude identification imported from printed equation (7). Its contact expression and scalar unitarity are derived, not supplied again. The inverse readout is restricted to nonzero contact.
- definitionAdditional evidence for a nonconstant source-parameter family: two positive sampled scales give different real values of one of C0, C2, D2. This is separate from satisfying the retained equations.
- definitionThe full-amplitude scale-independence claim remains an imported physics input. Completeness already states equality of the retained coefficients with the full ones, so the low-order residual is no longer supplied again.
- definition
- definition
- definitionIdentify the fitted retained model, its reported contact values at one subtraction scale, and its formal coefficient readout. This does not equate nominal and graded RG trajectories or assert an all-momentum error bound. The displayed C0 value is c+s at this scale, not c alone.
- definition
- definition
- definitionPrinted source equations (5)-(7), with an actual scalar S-matrix. The inverse amplitude is used only away from a zero of the contact polynomial.
- definition
- definitionActual first two pionless terms of the source expansion, rather than an independently assignable expansion label. Order assignments remain in KSWMixedExpansionAt; no infinite-series convergence or exact truncation is asserted.
- definition
- definitionEqual subleading contact combinations give equal complete retained coefficients, with the other fitted data fixed. This is a computed model property, not a stored fit verdict.
- definitionEquality of every formal amplitude coefficient through the selected index. Index zero denotes p^-1 and index one denotes p^0 in the pion expansion. This does not compare evaluated amplitudes or bound the tail.
- definition
- definitionThe paper does not provide a complete analytic order-`p⁰` formula for every entry of the coupled amplitude matrix.
- definitionNo finite loop cutoff contains every leading C0 chain at this selected channel, subtraction scale and momentum. The exponents are assigned counting data; identifying them with actual scaling is a separate physical input. This is not a convergence or truncation-error claim.
- definition
- definition
- definition
- definition
- definitionCumulative calculation coverage includes every degree up to the requested one, including known zero coefficients. Individual availability remains source input; this definition does not validate their values.
- definitionAvailability at one common formal phase degree. This is epistemic input, not a claim of nonzero value or independently certified accuracy.
- definition
- definitionOne amplitude family determines the normalized S - 1 family. Matching its entries to the selected real phase observables remains a separate requirement; neither phase branches nor nuclear applicability are derived.
- definition
- definitionThe source's enhanced assigned coupling orders for every contact. This is an explicit physical input, not a consequence of large scattering length alone, nor a lower bound, convergence claim, or estimate of omitted terms.
- definition
- definition
- definition
- definition
- definition
- definitionThe actual threshold coefficients of the selected observable. A sampling family realizes positive momenta near zero; the error condition applies to every sufficiently small momentum in the selected physical domain, not only one chosen family. The finite-length chart requires a nonzero scattering length; the standalone inverse-length model separately allows the unitary limit. The uniform radius is selected after the tolerance and before the momentum. No value at zero, analyticity, quartic bound or error estimate at a fixed prediction momentum is asserted. This corrects the former free-remainder identity, which alone did not identify either coefficient. It is not equivalent to that weaker input.
- definitionThe exact residual is determined by the observable and the two selected coefficients. Defining it supplies no smallness, threshold matching or error bound (author TeX labels 8-9).
- definitionExact reconstruction, including the residual, not a two-term approximation or a physical matching assertion.
- definitionAuthor TeX equation (11): the leading pionless contact is fixed by the scattering length and PDS subtraction scale. The denominator condition keeps the displayed inverse away from its pole; the positive mass and nonzero scattering length retain the physical domain used in the paper.
- definitionAuthor TeX equation (11): the first derivative contact carries the same PDS pole squared and one factor of the effective range.
- definitionEquation (11) is retained as the actual `C₀(μ)` and `C₂(μ)` value family at every non-pole subtraction scale, not merely as an opaque selected-running-solution label. The observable-family contract below now derives these formulas; applicability of that family remains imported physics.
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definitionThe source normalization fixes S - 1 from the selected amplitude, mass and momentum (author TeX lines 495-501). It does not fix phase representatives or assert that a truncated amplitude is exactly unitary.
- definition
- definitionThe separate pion-inclusive amplitude family agrees with its designated physical target. No identification with the pionless amplitude is imposed.
- definition
- definitionThe paper's selected subleading amplitude, high-momentum fit, and omitted-term assessment interpreted in the shared truncation vocabulary. Exact equalities keep the context scoped to the channel, scale, momentum, regime, and order chosen here.
- definitionDistinct numerical C0 and D2 values at the selected fit scale give the same retained prediction curve. The replacements are local fit parameters, not constant RG trajectories or a claim of indistinguishability beyond p^0.
- definition
- definitionKSW's typed source relation keeps the pion-inclusive RG-controlled couplings and scale-independent full amplitude distinct from the later shared renormalized-prediction endpoint.
- definitionThe joining derivation retains the PDS loop, nonperturbative bubble sum, and unitarity recovery together with the mixed pion-inclusive expansion and its independent RG cancellation. Its pionless target is not identified with the later full-amplitude target.
- definition
- definition
- definitionAt order `p⁻¹`, only the `S -> S` matrix component may be nonzero.
- definition
- definition
- definition
- definition
- definitionThe explicit printed-equation-(15) two-loop formula uses the same scale, momentum and running couplings as the source RG route.
- definitionPrinted equation (15) identifies the nominal order-p^0 graph on the finite massive-pion domain. Its running couplings can contain higher-order effects; this is not equality to a formal expansion coefficient. The final witness asserts a nonzero explicit log coefficient, not variation of the whole running graph. The latter also involves the running prefactor and the nonlogarithmic terms.
- definitionThe selected loop has assigned soft order one. Its dependence on the subtraction scale must not be replaced by a momentum-only validity flag.
- definition
- definitionIn this PDS parametrization, the source identifies MS with mu=0 (author TeX after label 11). It is not a second independent scheme flag.
- definitionThe ordinary-MS validity domain excludes an actual momentum in the selected pionless domain. This is a domain statement, not an independent flag attached to an arbitrarily selected momentum.
- definition
- definitionAfter fitting the `S`-wave phase, the leading mixing-angle and `D`-wave predictions require no additional fit parameters.
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definitionThe actual source quotient for the full pionless contact polynomial. This is not the C0-only leading term, nor the later pion-inclusive amplitude. The physical pole restriction belongs to pdsAmplitudeObtained below.
- definition
- definitionThe zero-derivative PDS loop with the selected mass, scale and momentum. It is derived from the imported all-power formula, not supplied as an independent equality between two abstract loop values.
- definition
- definition
- definition
- definition
- definitionThe omitted coefficient is the full-minus-retained residual, not an independently selected family. This identity does not assert its order, size, convergence, or relation to an unexpanded physical remainder.
- definition
- definitionThe coefficient argument's complete data projection at one channel. No new data are chosen. The channel's singlet identity remains an explicit condition in the paper contracts, not a property inferred from coefficients.
- definitionBuild a graded jet from the paper's one set of physical constants and four independently selected contact functions. These functions are not the nominal RG trajectories; the same construction also serves fitted jets.
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definitionCompatibility name for the retained-model equation, not an exact all-orders physical beta function.
- definitionThe retained equations hold on a neighborhood of each represented positive scale, with at least one such scale. This is a local differential claim, not just a fitted derivative at one point or a global continuation through every positive real scale. No nonconstant-running hypothesis or connectedness of separate scale neighborhoods is asserted.
- definition
- definitionThe pion-inclusive beta-function display and the D2 equation: the actual scale-weighted derivative equals the retained-model beta formula at each positive sampled scale. The intrinsic contact index avoids interpreting an unrelated coupling label as a second numerical beta-function family. These computed-order equations differ from the pionless equations and do not identify an exact all-orders physical flow.
- definitionThe nominal pion flow uses the same nucleon mass as the other paper readouts. Its five other inputs remain independent data. This does not identify nominal running couplings with formal expansion coefficients.
- definition
- definition
- definitionScale independence of the actual full-contact pionless amplitude. The threshold coefficient limits alone do not imply this all-scale claim.
- definition
- definitionSelect the actual mass, momentum, scale, C0, C2, and two pionless terms. The later pion-inclusive subleading amplitude is a distinct object.
- definition
- definition
- definition
- definition
- definition
- definitionC0 uses index zero of the same order family used for derivative contacts. The values are assigned counting data, not numerical bounds on couplings.
- definition
- definitionTotal center-of-mass energy in the selected leading nonrelativistic model, not the energy of one nucleon. Positive mass and physical identification are separate requirements of the formula contracts.
- definition
- definitionThe source uses one M, mu and p in the interaction, loop and bubble amplitude (author TeX equations (1)-(5)). These are selected from the same framework, not copied into a second freely chosen readout. The on-shell energy is derived from M and p. The interaction polynomial, evaluated loop and amplitude remain explicit data; their physical interpretation and calculation are not established here.
- definition
- definitionThe selected channel's real-scale coupling family, shared by its sampled and continuous equation-(11) interfaces. Different channels need not share couplings or effective-range data (source: equation (11) and Fig. 3).
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definitionAt the selected resummed regime both terms are assigned order p^0, and graph V actually changes a first retained coefficient at a represented scale. This is a formal-order statement, not a numerical lower bound on its size relative to pion exchange at every subtraction scale.
- definitionThe `D₂ m_π²` interaction is required precisely when including it restores subtraction-point independence through order `p⁰`, while omitting it does not.
- definitionRadiation-pion contribution, with coefficient index n representing formal momentum power n-1. Its physical graph identification is external.
- definitionRadiation pions contribute neither retained grade. The source excludes them from the leading bubble sum and from the first correction. This is not the assertion that their entire amplitude vanishes.
- definition
- definition
- definition
- definition
- definition
- definitionA fixed multiplicative window realizes the source's choice mu ~ p (author TeX before label 14). The same dimensionless factor applies to all selected scale/momentum pairs; choosing a new factor at each pair would not control a family of scales. Positive momentum and c >= 1 imply positive mu. This finite-window interpretation does not supply contact orders, exclude the contact pole, or control the omitted EFT terms.
- definition
- definition
- definitionKSW's full-contact pionless PDS amplitude enters the mixed expansion underlying the later pion-inclusive scale-independent prediction. The selected two-nucleon PDS record is not identified with the pion-inclusive scattering record, and the recovered pionless amplitude is not identified with the physical all-orders target.
- definition
- definition
- definition
- definition
- definitionThe fit uses the framework's existing physical constants. Only its four graded contact functions are selected separately; these are not identified with the full nominal RG trajectories.
- definition
- definitionCompleteness through the two retained grades means that the computed and full coefficients agree throughout the represented scale family. The source-route scale argument is retained for API compatibility, not as a restriction to one subtraction point. Higher coefficients, convergence and finite-momentum accuracy remain unrestricted.
- definition
- definition
- definition
- definition
- definitionNominal complex value of graph IV in printed equation (15), author-TeX label 17.
- definitionNominal complex value of graph V, separate from formal coefficients.
- definition
- definition
- definitionKSW's designated physical amplitude supplies the physical outcome relation for the selected channel and momentum. The target and each scale-indexed full-amplitude calculation remain distinct descriptions of that one scattering problem.
- definitionShared large-scattering-length view of KSW's pionless PDS route. The named two-nucleon PDS system retains the channel and subtraction scale. The resummed object is the scale-indexed full amplitude, and the low-energy target is the paper's PDS formula value together with the independent unitarity check.
- definition
- definition
- definition
- definitionShared technical view of KSW's running-coupling and invariant-amplitude renormalization route. The selected full-amplitude family and every relation used by the shared inference are retained in one exact proof-free model. Actual variation of the selected source couplings is additional sampled evidence, not a consequence assumed inside the retained beta equations.
- definition
- definition
- definition
- definition
- definitionThe counterterm truncation claim tested by footnote 3: graph V can be omitted through the first correction throughout the subtraction-scale domain, with all other data fixed. This is not a claim about every version of Weinberg counting or a reparametrization that moves D2 into C0.
- definitionThe printed II/III formulas are used at p>0, not evaluated by totalized division at threshold. The denominator is then nonzero by reality, not an extra input. Graph IV/V separately retain their larger threshold domain.
- definition
- definitionThe retained grades of the printed beta equations. The inhomogeneous C0 term runs s, not c. No equation for omitted grades is supplied.
- definition
- definition
- definition
- definition
- definition
- definitionCoefficient of Q^0 in A: the first C0 correction to the resummed leading graph, derivative contact I, and pion graphs II through V.
- definitionPrinted equation (20)'s local first phase increment. Its reality is a derived property, not a real-part projection or a choice of leading phase branch.
- definitionReconstruct the four graded contact functions from one reference scale. The logarithm is a ratio of scales; values at poles or nonpositive scales are totalized Lean expressions, not assertions of physical validity.
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definitionPrinted equation (20)'s readout of (A_{-1}, A_0): the leading elastic S-matrix and its local first phase increment. It selects no global logarithm branch and does not treat a truncated amplitude as exactly unitary.
- definitionCompare subleading contact values at a fixed subtraction scale. The leading contact, derivative contact and physical constants are unchanged. The constant replacements are not asserted to be RG trajectories.
- definitionRemove only graph V. All other data and their scale dependence stay fixed.
- definitionA nonzero unitary-limit leading flow with its logarithmically generated mass contact. It satisfies the graded equations, not the full nominal beta0.
- definition
- definition
- definitionThe subleading C0 piece is s. This is not the source's nominal A0 evaluated with the full C0: it includes the first variation of A_-1.
- definition
- definition
- definition
- definition
- definition
- definition
- definitionAlgebraic normal form of all five nominal A0 graphs after common soft scaling; the constants retain their explicit source readbacks above.
- definitionThis family realizes C0=c/Q+s, C2=r/Q^2 and D2=d/Q^2 while transforming the subtraction coordinate itself by Q. It is not an exact solution of the full nominal beta system at every Q.
- definitionc0 is the leading coupling coefficient, s its subleading correction; the source's nominal flow with both already combined is not substituted here. Graphs II/III use the printed p > 0 formulas. Their p = 0 limits must not be read from Lean's totalized divisions in this algebraic helper.
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definitionThe original continuous-domain contract, retained for the differential running equivalence. These topological clauses are not needed after calibration.
- definitionOne reference-scale choice before the momentum quantifier.
- definitionOne global calibration of the sampled coefficients. The sampled scales need not form a continuum; positivity and the excluded contact pole remain.
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definitionFinite, massive-pion formula domain. Threshold p=0 is allowed when the dressed denominator is nonzero; the chiral limit needs a separate limit.
- definitionLiteral beta equations for the retained model, at positive subtraction scale. No bound or equality for omitted beta contributions is asserted.
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definitionThe dressed mass insertion A_0^(V), with its coupling value exposed so its response to a counterterm shift can be checked.
- definition
- definition
- definition
- definition
- definition
- definition
- definitionThe common C0 dressing in printed equation (15), with the paper's PDS sign.
- definition
- definition
- definition
- definition
- definitionThe two-loop pion graph A_0^(IV), including its finite PDS convention. This formula is not an assertion that an arbitrary loop readout equals it.
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definitionConvenient units with M/(4 pi) = 1. These are exact source-formula controls, not experimental values of the nuclear couplings.
- definitionThe scalar PDS scattering residual through derivative grade one. The formal variable counts insertions, not loops or numerical momentum. The two local equations and printed equation (13) are derived below; no infinite-series convergence or omitted-term estimate is asserted.
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definitionA positive-scale PDS loop output with an on-shell energy and a nonsingular bubble denominator still need not provide the resummed amplitude. This keeps the actual equation-(4) loop family and the physical domain, rather than treating a calculation name as evidence for printed equations (4) and (5).
- definition
- definition
- definition
- definitionReal contact couplings describe the selected elastic channel. A complex absorptive contact is not silently treated as a unitary one-channel theory.
- definitionPrinted v2 equation (4): `I_n^PDS = -(M E)^n (M / 4 pi) (mu + i p)`. The equation is retained for every loop power. The selected bubble-chain route uses its actual zero-power member, not a parallel abstract loop value.
- definitionPrinted v2 equation (5), author TeX label `6`: `i A = -i C(p^2, mu) / (1 + M C(p^2, mu) (mu + i p) / (4 pi))`. The denominator condition is explicit because the printed quotient is not a totalized physical amplitude at its pole.
- definition
- definitionThe displayed loop formula is evaluated on the center-of-mass shell `M E = p^2`, the relation used when the paper passes from the dimensionally regulated integral to the PDS expression.
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definitionThe literal scalar normalization in printed source equation (6).
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definitionTwo smooth candidate flows agree with the printed contacts at mu = 0; their first derivatives there are different.
- definition
- definitionThe actual ordinary derivatives underlying the scale-weighted equations. For nonzero inverse scattering length the non-pole solution also fixes the derivative at mu = 0, where multiplying a putative equation by mu would lose that information. At zero inverse length, mu = 0 is excluded instead.
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definitionThe soundness law has at least one strict contribution comparison.
- definitionSound power counting with a concrete strict order comparison. The witness prevents the universal suppression law from being satisfied on an empty or comparison-free contribution scope.
- definitionThe order assignment is physically meaningful in a regime when a term at a strictly later order is suppressed relative to one at an earlier order.
- definitionA selected pair of contributions occupies a strict order comparison in the declared regime. This proposition records the applicability premises of the universal soundness law without presupposing its suppression conclusion.
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definitionTwo distinct scales share one effective prediction in the sector.
- definition
- definitionCross-scale agreement with a concrete prediction at two distinct scales.
- definitionVariation of the selected parameter coordinates, not a beta equation or an assertion that the physical theory is away from an RG fixed point. Scale-dependent changes of units can change this proposition while leaving all predictions unchanged. The choice of parameter coordinates is therefore part of its interpretation.
- definitionExtensional prediction agreement across scales. This low-level law may hold when the selected sector has no prediction or when there is only one scale; `NonvacuousScaleIndependentPredictionsAt` adds a witnessed comparison.
- definitionThe target makes at least one prediction in the selected sector.
- definition
- definition
- definition
- definition
- definition
- definition
- definitionAn empirically adequate description represents the system, makes at least one selected prediction, and agrees with physical outcomes throughout the sector. The active prediction and agreement jointly ensure at least one realized prediction rather than merely a vacuous universal statement.
- definition
- definition
- definition
- definitionA selected observable sector.
- definitionA description makes at least one prediction in the selected sector.
- definition
- definition
- definitionA model-to-world interpretation law. It does not assert that the model has produced a conclusion; use `GroundedModelConclusionAt` for that.
- definitionA model-to-theory interpretation law. It does not assert that the model has produced a conclusion; use `GroundedModelConclusionAt` for that.
- definition
- definition
- definition
- definition
- definition
- definitionBuild the epistemic dependency basis in paper order. A conclusion inherits the justification origin of its own step and every origin already attached to its premises.
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definitionExpand a set of route identifiers by one dependency edge, iterated with enough fuel to traverse any acyclic graph on the declared routes.
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
Selected instances and coercions
- instance
- instance
- instance
- instance
- instance
- instance
- instance
- instance
- instance
- instance
- instance
- instance
- instance
- instance
- instance
- instance
- instance
- instance
- instance
- instance
- instance
- instance
- instance
- instance
- instance
- instance
- instance
- instance
- instance
- instance
- instance
- instance
- instance
- instance
- instance
- instance
- instance
- instance
- instance
- instance
- instance
- instance
- instance
- instance
- instance
- instance
- instance
- instance
- instance
Source mappings and interpretation choices
- inductive
- definition
- instance
- constructor
- definition
- checked statement
- constructor
- definition
- checked statement
- constructor
- definition
- checked statement
- constructor
- definition
- checked statement
- constructor
- definition
- checked statement
- definition
- constructor
- definition
- checked statement
- constructor
- definition
- checked statement
- constructor
- definition
- checked statement
- constructor
- definition
- checked statement
- definition
- definition
- definition
- constructor
- definition
- checked statement
- constructor
- definition
- checked statement
- constructor
- definition
- checked statement
- constructor
- definition
- checked statement
- constructor
- definition
- checked statement
- constructor
- definition
- checked statement
- constructor
- definition
- checked statement
- constructor
- definition
- checked statement
- constructor
- definition
- checked statement
- constructor
- definition
- checked statement
- constructor
- definition
- checked statement
- constructor
- definition
- checked statement
- constructor
- definition
- checked statement
- constructor
- definition
- checked statement
- constructor
- definition
- checked statement
- constructor
- definition
- checked statement
- constructor
- definition
- checked statement
- constructor
- definition
- checked statement
- constructor
- definition
- checked statement
- constructor
- definition
- checked statement
- constructor
- definition
- checked statement
- constructor
- definition
- checked statement
- constructor
- definition
- checked statement
- constructor
- definition
- checked statement
- constructor
- definition
- checked statement
- constructor
- definition
- checked statement
- constructor
- definition
- checked statement
- constructor
- definition
- checked statement
- constructor
- definition
- checked statement
- constructor
- definition
- checked statement
- constructor
- definition
- checked statement
- definition
- definition
- definition
- checked statement
- constructor
- definition
- checked statement
- constructor
- definition
- checked statement
- constructor
- definition
- checked statement
- constructor
- definition
- checked statement
- constructor
- definition
- checked statement
- constructor
- definition
- checked statement
- constructor
- definition
- checked statement
- constructor
- definition
- checked statement
- constructor
- definition
- checked statement
- constructor
- definition
- checked statement
- constructor
- definition
- checked statement
- constructor
- definition
- checked statement
- constructor
- definition
- checked statement
- recursor
- definition
- constructor
- definition
- checked statement
- constructor
- definition
- checked statement
- constructor
- definition
- checked statement
- constructor
- definition
- checked statement
- constructor
- definition
- checked statement
- constructor
- definition
- checked statement
- constructor
- definition
- checked statement
- definition
- constructor
- definition
- checked statement
- constructor
- definition
- checked statement
- constructor
- definition
- checked statement
- inductive
- definition
- instance
- constructor
- definition
- checked statement
- constructor
- definition
- checked statement
- constructor
- definition
- checked statement
- constructor
- definition
- checked statement
- constructor
- definition
- checked statement
- constructor
- definition
- checked statement
- constructor
- definition
- checked statement
- constructor
- definition
- checked statement
- definition
- constructor
- definition
- checked statement
- constructor
- definition
- checked statement
- constructor
- definition
- checked statement
- definition
- definition
- definition
- constructor
- definition
- checked statement
- constructor
- definition
- checked statement
- constructor
- definition
- checked statement
- constructor
- definition
- checked statement
- constructor
- definition
- checked statement
- constructor
- definition
- checked statement
- constructor
- definition
- checked statement
- constructor
- definition
- checked statement
- constructor
- definition
- checked statement
- constructor
- definition
- checked statement
- constructor
- definition
- checked statement
- constructor
- definition
- checked statement
- constructor
- definition
- checked statement
- constructor
- definition
- checked statement
- constructor
- definition
- checked statement
- constructor
- definition
- checked statement
- constructor
- definition
- checked statement
- constructor
- definition
- checked statement
- constructor
- definition
- checked statement
- constructor
- definition
- checked statement
- constructor
- definition
- checked statement
- constructor
- definition
- checked statement
- constructor
- definition
- checked statement
- constructor
- definition
- checked statement
- constructor
- definition
- checked statement
- definition
- definition
- definition
- checked statement
- constructor
- definition
- checked statement
- constructor
- definition
- checked statement
- constructor
- definition
- checked statement
- constructor
- definition
- checked statement
- constructor
- definition
- checked statement
- constructor
- definition
- checked statement
- constructor
- definition
- checked statement
- constructor
- definition
- checked statement
- constructor
- definition
- checked statement
- recursor
- definition
- constructor
- definition
- checked statement
- constructor
- definition
- checked statement
- constructor
- definition
- checked statement
- constructor
- definition
- checked statement
- constructor
- definition
- checked statement
- constructor
- definition
- checked statement
- constructor
- definition
- checked statement
- constructor
- definition
- checked statement
- constructor
- definition
- checked statement
- definition
- constructor
- definition
- checked statement
- constructor
- definition
- checked statement
- constructor
- definition
- checked statement
- constructor
- definition
- checked statement
- constructor
- definition
- checked statement
- constructor
- definition
- checked statement
- constructor
- definition
- checked statement
- constructor
- definition
- checked statement
- constructor
- definition
- checked statement
- inductive
- definition
- instance
- constructor
- definition
- checked statement
- definition
- constructor
- definition
- checked statement
- constructor
- definition
- checked statement
- constructor
- definition
- checked statement
- constructor
- definition
- checked statement
- definition
- definition
- definition
- constructor
- definition
- checked statement
- constructor
- definition
- checked statement
- constructor
- definition
- checked statement
- constructor
- definition
- checked statement
- constructor
- definition
- checked statement
- constructor
- definition
- checked statement
- constructor
- definition
- checked statement
- constructor
- definition
- checked statement
- definition
- definition
- constructor
- definition
- checked statement
- constructor
- definition
- checked statement
- definition
- checked statement
- constructor
- definition
- checked statement
- constructor
- definition
- checked statement
- constructor
- definition
- checked statement
- constructor
- definition
- checked statement
- constructor
- definition
- checked statement
- recursor
- definition
- constructor
- definition
- checked statement
- constructor
- definition
- checked statement
- constructor
- definition
- checked statement
- definition
- constructor
- definition
- checked statement
- constructor
- definition
- checked statement
- constructor
- definition
- checked statement
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- checked statement
- checked statement
- checked statement
- checked statement
- checked statement
- checked statement
- definition
- definition
- definition
- definition
- definition
- checked statement
- definition
- definition
- definition
- definition
- instance
- checked statement
- checked statement
- instance
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- checked statement
- checked statement
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- inductive
- definition
- instance
- definition
- constructor
- definition
- checked statement
- definition
- definition
- definition
- constructor
- definition
- checked statement
- constructor
- definition
- checked statement
- constructor
- definition
- checked statement
- definition
- definition
- definition
- checked statement
- constructor
- definition
- checked statement
- recursor
- definition
- constructor
- definition
- checked statement
- constructor
- definition
- checked statement
- definition
- inductive
- definition
- instance
- definition
- definition
- definition
- definition
- constructor
- definition
- checked statement
- constructor
- definition
- checked statement
- constructor
- definition
- checked statement
- constructor
- definition
- checked statement
- constructor
- definition
- checked statement
- definition
- definition
- definition
- checked statement
- recursor
- definition
- constructor
- definition
- checked statement
- constructor
- definition
- checked statement
- definition
- structure
- definition
- instance
- checked statementRaw paper-local inputs construct every KSW route in source order.
- definition
- checked statement
- checked statement
- checked statementCompose the actual outputs of the observable/RG and mixed-interaction routes for the same channel. The first fixes C0 and C2; the second fixes the two actual source amplitudes. No independent amplitude, matching equation or contact-order assignment is supplied to this deduction. The inherited route inputs remain part of its review scope. Positive mu is not restricted to p. The quantitative window and range-size bound are explicit additional physical inputs. Two-sided leading-contact bounds, the derivative correction and the finite loop error have different meanings: none bounds the omitted physical amplitude, and raw loop failure is asserted only under its stated ratio test. Source: author TeX labels 8, 9, 11 and 14.
- definition
- definition
- checked statementThe coupled-channel route exposes KSW's displayed S-matrix formula before the zero-mixing and zero-D-wave consequence is used downstream.
- checked statement
- definition
- checked statement
- definition
- definition
- definition
- checked statement
- checked statement
- definition
- definition
- definition
- definition
- definition
- checked statement
- definition
- checked statement
- definition
- definition
- definition
- checked statement
- constructor
- definition
- checked statement
- checked statement
- definition
- checked statement
- definition
- definition
- definition
- definition
- definition
- checked statementThe pionless PDS inputs expose the literal printed-equation-(4) loop and equation-(5) amplitude claims independently of the named loop/amplitude outputs. The public theorem name retains the historical numbering for compatibility.
- checked statement
- recursor
- definition
- checked statement
- checked statement
- definition
- checked statement
- checked statement
- inductive
- definition
- instance
- definition
- definition
- definition
- definition
- constructor
- definition
- checked statement
- constructor
- definition
- checked statement
- constructor
- definition
- checked statement
- constructor
- definition
- checked statement
- constructor
- definition
- checked statement
- constructor
- definition
- checked statement
- constructor
- definition
- checked statement
- constructor
- definition
- checked statement
- constructor
- definition
- checked statement
- constructor
- definition
- checked statement
- constructor
- definition
- checked statement
- constructor
- definition
- checked statement
- constructor
- definition
- checked statement
- constructor
- definition
- checked statement
- constructor
- definition
- checked statement
- constructor
- definition
- checked statement
- constructor
- definition
- checked statement
- constructor
- definition
- checked statement
- constructor
- definition
- checked statement
- constructor
- definition
- checked statement
- constructor
- definition
- checked statement
- constructor
- definition
- checked statement
- constructor
- definition
- checked statement
- constructor
- definition
- checked statement
- constructor
- definition
- checked statement
- constructor
- definition
- checked statement
- constructor
- definition
- checked statement
- constructor
- definition
- checked statement
- constructor
- definition
- checked statement
- constructor
- definition
- checked statement
- constructor
- definition
- checked statement
- constructor
- definition
- checked statement
- constructor
- definition
- checked statement
- definition
- definition
- definition
- checked statement
- constructor
- definition
- checked statement
- recursor
- definition
- constructor
- definition
- checked statement
- constructor
- definition
- checked statement
- constructor
- definition
- checked statement
- constructor
- definition
- checked statement
- constructor
- definition
- checked statement
- constructor
- definition
- checked statement
- constructor
- definition
- checked statement
- constructor
- definition
- checked statement
- constructor
- definition
- checked statement
- constructor
- definition
- checked statement
- constructor
- definition
- checked statement
- constructor
- definition
- checked statement
- constructor
- definition
- checked statement
- constructor
- definition
- checked statement
- constructor
- definition
- checked statement
- constructor
- definition
- checked statement
- constructor
- definition
- checked statement
- constructor
- definition
- checked statement
- constructor
- definition
- checked statement
- constructor
- definition
- checked statement
- constructor
- definition
- checked statement
- constructor
- definition
- checked statement
- constructor
- definition
- checked statement
- constructor
- definition
- checked statement
- constructor
- definition
- checked statement
- constructor
- definition
- checked statement
- constructor
- definition
- checked statement
- constructor
- definition
- checked statement
- constructor
- definition
- checked statement
- definition
- definition
- checked statement
- checked statement
- definition
- checked statementThese 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.
- definition
- definition
- checked statement
- checked statement
- checked statement
- definition
- checked statement
- checked statement
- checked statement
- checked statement
- instance
- checked statement
- checked statement
- instance
- checked statement
- checked statement
- instance
- checked statement
- checked statement
- instance
- checked statement
- checked statement
- instance
- checked statement
- checked statement
- instance
- definition
- definition
- instance
- definition
- definition
- instance
- definition
- definition
- instance
- definition
- definition
- instance
- definition
- definition
- definition
- checked statement
- definition
- checked statement
- definition
- definition
- definition
- definition
- definition
- checked statement
- checked statement
- definition
- checked statement
- definition
- definition
- definition
- checked statement
- checked statement
- checked statement
- checked statement
- checked statement
- checked statement
Checked statements: parameters, hypotheses, and interpretation
- checked statement
- checked statement
- checked statement
- checked statement
- checked statement
- checked statement
- checked statement
- checked statement
- checked statement
- checked statement
- checked statement
- checked statementA complete characterization on physical, nonempty chains by the tree vertex and the effect of adjoining one PDS bubble and vertex. The original source supplies the scalar on-shell vertex and subtracted loop rules; this checks their composition for every chain. The empty-list value is unconstrained, and these finite rules do not evaluate an infinite bubble sum.
- checked statementThe source's mu~p regime as one quantitative window: c, rho, the effective-range coefficients and their naturalness bound are fixed before both scale and momentum quantifiers. All evaluated finite chains have the conservative derivative-degree bound, while every finite loop cutoff omits a nonzero leading chain with a window-uniform lower bound. No assigned exponents, exact nonzero derivative orders or physical remainder estimate are inputs or conclusions. Constants may grow with chain length; the nonempty coefficient window alone is not an EFT applicability claim.
- checked statementA finite contact bound transfers to every chain built from those contacts. The prefactor depends on chain length; this is not a bound on the infinite sum.
- checked statementA loop cutoff misses a nonzero leading chain with a quantitative lower bound, not merely a chain labelled leading by an ordinal convention.
- checked statementError of the actual finite leading bubble sum against the imported resummed amplitude, not the magnitude of an individual omitted diagram. No convergence of the geometric series is needed for this finite identity.
- checked statementThe finite leading-contact sum at an arbitrary real subtraction scale. This is the same PDS loop and source amplitude, with no choice mu=p and no assumption that the geometric series converges.
- checked statement
- checked statementAll treatment information is generated by chain membership and insertion counts. The only numerical soundness obligation is the actual relative size of the two calculated terms. No freely assigned coupling orders, treatment predicates or interpretation certificate are premises.
- checked statement
- checked statement
- checked statement
- checked statement
- checked statement
- checked statement
- checked statementExact readable reduction of the complete generated treatment output. All chain-based API conclusions are derived; the only remaining numerical condition is already a conclusion of the value argument. This does not validate the context's field meanings or any unsupplied higher coefficient. Source: the pionless counting discussion between author TeX labels 11 and 14.
- checked statement
- checked statementThe quantitative argument on one nonempty matching window. All physical coefficients and bounding constants are fixed before the momentum quantifier. The finite-jet bound and nonzero omitted leading chains are actual amplitude statements; the last clause classifies the conservative derivative degree. It does not assert that an allowed derivative chain is nonzero, that the infinite chain sum converges, or that these bounds control the physical remainder after resummation.
- checked statement
- checked statementThe grading of an actual evaluated chain is the sum of its derivative indices. Each vertex contributes X^n and each leading PDS loop degree zero. The coefficient multiplying that monomial is exactly the existing numerical chain amplitude. Its p/Lambda interpretation requires the matching bounds above; this algebra alone does not assign physical scaling exponents.
- checked statementCoefficient extraction from the single scalar PDS scattering equation. The formal variable counts derivative degree after enhanced counting, not loops or the numerical momentum. Arbitrary higher coefficients cannot enter these two equations. This is not evaluation of an infinite series. Source: the expansion and two terms following author TeX label 11, before label 14.
- checked statement
- checked statement
- checked statementEvery additional leading bubble multiplies the normalized magnitude by the same dimensionless factor. No p/Lambda factor is gained from the loop.
- checked statementLeading matching gives a lower bound as well as an upper bound. This rules out a vanishing C0 and needs no effective-range naturalness premise.
- checked statementSubstitute an affine interaction and amplitude into the scalar scattering equation. Removing its explicit quadratic term leaves precisely the two local leading/single-insertion equations. The parameter counts insertions, not powers of momentum. This is an exact polynomial identity, not an error bound against the unknown physical amplitude or a claim that the residual vanishes at one.
- checked statementAlgebraic reconstruction of the leading bubble sum and one dressed derivative insertion from the local interaction equations. The insertion is allowed on either side of a leading bubble, but never twice. These equations are equivalent to the source's two closed formulas, including their nonpole domain; no convergence of an infinite graph sum is asserted.
- checked statement
- checked statement
- checked statement
- checked statement
- checked statement
- checked statement
- checked statement
- checked statementA complete conditional pionless power-counting argument at a selected positive momentum with mu=p. Matching and naturalness bound the actual finite chains. The local leading and single-insertion equations determine the two source amplitudes. The exact error of every finite leading loop sum is derived; on the stated deeper window it is at least the leading amplitude's norm. In contrast, the norm implication controls the first resummed derivative correction. The final identity identifies the exact quadratic residual in the scalar contact equation, with a parameter counting insertions rather than powers of momentum. The observable and contact limits at fixed mu=p derive the first two matching equations. Only coefficients from degree two through last remain imported as a finite inverse-amplitude jet. The limit variable q is not the prediction momentum p. No higher coefficient follows from the first two limits, and no condition on omitted coefficients or convergence is imposed. The local equations are an algebraic reconstruction of the source graph rules, not a convergent-series assertion. The conclusion concerns the selected two terms, not the error against the unknown full physical amplitude. All higher contact bounds remain restricted to the supplied finite matching jet. Positivity of the cutoff and nonnegativity of the bound follow from the momentum domain and the retained first naturalness bound, respectively. Source: author TeX labels 6, 8, 9, 11 and 14.
- checked statement
- checked statement
- checked statement
- checked statement
- checked statementFinite effective-range matching bounds actual PDS chains. No coupling or loop exponent assignment is a hypothesis. Only contacts through last occur.
- checked statementAll finite leading chains have two-sided bounds with constants depending on loop count and the fixed window ratio, not on p/Lambda. This does not assert convergence, nor a lower bound on a sum where cancellation may occur.
- checked statementThe complete value argument with its jet-scoped shared treatment API. The exact API readback proves that it adds no physical condition beyond the already established strict correction bound. Source: author TeX labels 6, 8, 9, 11 and 14. Unsupplied higher contacts remain outside this client.
- checked statementOn this sufficient large-length window, no finite leading bubble sum is even within the leading amplitude's own norm of the resummed answer. The extra window bound is explicit; nonzero omitted diagrams alone do not imply this conclusion. This is failure of raw loop truncation, not of the EFT's resummed derivative expansion.
- checked statementIn minimal subtraction, matching fixes alpha*g=1 and the evaluated loop factor is i*p. The same resummed observable has a raw C0 loop-series radius p<|alpha|=1/|a|, irrespective of the short-distance scale. This is a statement about that leading series, not a sufficient criterion for full EFT validity. The finite coefficient does not exist at alpha=0. Source: author TeX after label 11, together with the loop and amplitude formulas before label 8.
- checked statementA diagnostic real inverse-amplitude function with the same first two threshold coefficients as the leading model. Its leading MS sum converges, and its full positive-momentum amplitude is elastic-unitary, but the unchecked quartic shape term produces a 200% error at p=1/2. This is not a nuclear model or a counterexample to a theorem with bounds on all higher shape coefficients.
- checked statement
- checked statementThe former equal-scale identity is preserved exactly as a specialization.
- checked statementExact rescaling with the actual subtraction scale retained. The source chooses mu comparable to p, not necessarily equal to p. The derivative degree comes from the same evaluated vertex and loop factors, not an assigned label.
- checked statement
- checked statement
- checked statement
- checked statement
- checked statement
- checked statement
- checked statement
- checked statement
- checked statementThe first-order physical distinction needs only the first two threshold coefficients, not an arbitrary higher matching jet. Original author TeX labels 8, 9, 11 and 14 fix K=q cot(delta), G=M C/(4 pi), g0=M C0/(4 pi), g1=M C2/(4 pi), k1=r0/2 and f=M A/(4 pi). Here mu=p is held fixed while q approaches zero. The two local equations encode the imported PDS interaction rule and zero/one derivative insertion; they are not an infinite-series limit. The literal finite geometric sum is the leading bubble truncation. Its error can stay large while the first derivative correction is small. The sufficient rho window is our deduction, not a numerical source claim. This theorem says nothing about omitted physical terms, nuclear applicability, or higher contact coefficients. The separate full-chain theorem retains those finite-jet inputs. Each supplied quadratic limit also derives its constant limit; they are not four independently requested threshold conditions. For every finite MS coupling matched to the same inverse length, the last clause gives the exact raw MS loop error and proves it exceeds the resummed amplitude on this window. No new physical predicate or premise is introduced. At alpha=0 no such finite MS coupling exists; the PDS conclusions still hold.
- checked statement
- checked statementOne fixed effective-range jet and naturalness constant control a whole nonempty scale window. The coupling family may run with mu; the physical matching coefficients, rho and bound may not be chosen again at each scale. This is still a finite-jet upper estimate, not a convergence assertion.
- checked statementWith the observable ERE fixed, coefficient extraction from the canonical contact germ imposes exactly two algebraic identifications. It adds no analyticity or separate contact regularity assumption. This is a local threshold statement at a nonpole scale, not a formula for the full physical amplitude or a bound on its omitted terms. Source: author TeX labels 8--11.
- checked statementThe source relation `p cot(delta) = -1/G - mu`, together with its effective-range jet, gives `G * (1/a - mu - sum k_j z^j) = 1` through the retained order in `z = p^2`, with mu fixed during coefficient extraction. Formal series here only collect coefficients: no evaluation at a momentum, convergence, or bound on a remainder is asserted. The shift leaves k_0 unused. The equivalence includes last=0 and does not independently assume a nonzero denominator.
- checked statement
- checked statement
- checked statement
- checked statementA finite matching jet and a finite naturalness bound control every retained normalized contact. No exponent assignment for those contacts is assumed.
- checked statement
- checked statement
- checked statement
- checked statement
- checked statementAll retained dimensional contacts have the enhanced upper power count, provided their effective-range matching coefficients obey the stated bound. The cutoff is the short-distance momentum scale, not a loop regulator here. The order-dependent prefactor is explicit and no lower bound is asserted.
- checked statementIn the source's positive-threshold domain, the quadratic coefficient limit already determines the constant coefficient. This is an exact logical characterization, not an extra regularity or physical naturalness assumption.
- checked statementFixing C0 and C2 does not bound C4 without the next effective-range coefficient. This finite-a matching family is an algebraic diagnostic, not a fitted nuclear potential or a violation of the naturalness premise.
- checked statementThe first two coefficient equations uniquely recover the two normalized contacts printed in equation (11). Nonpole is the necessary algebraic domain.
- checked statement
- checked statement
- checked statement
- checked statement
- checked statement
- checked statement
- checked statement
- checked statementThe inverse-amplitude relation has no independent contact-germ choice. This equivalence preserves arbitrary threshold neighborhoods and does not identify the functions at zero or away from threshold.
- checked statementThe imported inverse-amplitude identity uniquely fixes the contact near threshold, not its value at zero or at arbitrary prediction momenta. The nonzero denominator follows from the identity and is not supplied.
- checked statementThe change to dimensionless coefficients is checked against the original finite matching equations. Here g contains M/(4 pi), while k contains the coefficients of p cot(delta); its first entry is r0/2, not C2.
- checked statement
- checked statement
- checked statement
- checked statement
- checked statement
- checked statement
- checked statement
- checked statement
- checked statement
- checked statement
- checked statement
- checked statementThe source ERE is a coefficient statement, not an arbitrary decomposition with a free remainder. Only R/p^2 -> 0 along positive momenta is needed for the first two coefficients. A quartic bound is sufficient but not required.
- checked statementFixed-scale source identity (K+mu)G=-1 transfers the actual observable coefficients to the same normalized contact family. The positive approach excludes a single-point fit and does not assume values at p=0 or analyticity.
- checked statementEvery positive-derivative contact has finitely many allowed insertions through order zero. The bound concerns insertions, not the number of C0 bubbles dressing them, and makes no numerical convergence assertion.
- checked statementThe shared treatment claims follow from actual insertion bounds. Only the two retained contacts have fixed assigned orders; higher vertices need only lie beyond order zero. The exact sector characterization proves these are necessary and sufficient. Numerical scaling, convergence and remainder control are not inferred from this diagram-order interpretation.
- checked statement
- checked statementThe physical scaling inputs force an unbounded leading bubble sector and select precisely the leading chains plus one dressed C2 insertion through order p^0. Neither conclusion is an input. The topology and the interpretation of the assigned orders are exposed above; convergence, remainder bounds and derivation of the coupling exponents remain separate.
- checked statement
- checked statement
- checked statementAt order p^0 there is exactly one C2 p^2 vertex, with any number of C0 vertices on either side. In particular this is not a C0+C2 resummation.
- checked statement
- checked statementExact assumptions for the complete leading/first-correction chain sector. The source's all-order equality is sufficient but unnecessarily strong here: only the two retained contacts have fixed orders. Every higher vertex merely has to lie beyond order zero. These are assigned diagram orders, not numerical amplitude bounds, nonzero coefficients, or a physical remainder estimate.
- checked statement
- checked statement
- checked statement
- checked statement
- checked statementAt a fixed assigned order, derivative degree is bounded even though the number of leading bubbles is unbounded. No estimate of omitted terms follows.
- checked statement
- checked statementThe literal order of a chain with only leading contacts. No assignment to the derivative contacts is needed to decide this sector.
- checked statementNo finite bound on the number of C0 vertices retains every chain through the first correction. This is a statement about required diagram content.
- checked statementAt leading order every allowed chain contains C0 only. There is no restriction on its loop count. This is an order-selection statement, not the evaluation or convergence of the infinite bubble sum.
- checked statement
- checked statementThe same minimal criterion in the source-shaped language: arbitrarily many leading bubbles and exactly one dressed derivative insertion through the first correction. No exact order for an excluded higher contact is needed.
- checked statement
- checked statement
- checked statementUnlike enhanced counting, natural counting admits only finitely many loops at each fixed nonnegative momentum order.
- checked statement
- checked statement
- checked statementEvery finite loop cutoff omits a chain still assigned leading order. This obstructs order-completeness of a finite loop truncation, not numerical convergence of a geometric series at a particular momentum.
- checked statementA single perturbative C2 insertion can be dressed by arbitrarily many leading loops. A finite insertion bound must not be read as a loop bound.
- checked statementComplete diagram selection through the first correction, conditional on the stated PDS scaling assignment and the contact-chain topology.
- checked statement
- checked statementResumming C2 along with C0 includes diagrams outside the first correction. The two-insertion chain is admitted as a diagram, but has order p^1, not p^0.
- checked statementIn this chain topology, unbounded loop count at assigned order -1 is equivalent to the source's leading-contact and loop exponents. It concerns order completeness, not failure of numerical convergence of a bubble sum.
- checked statement
- checked statement
- checked statement
- checked statement
- checked statement
- checked statement
- checked statement
- checked statement
- checked statement
- checked statement
- checked statement
- checked statement
- checked statement
- checked statement
- checked statement
- checked statement
- checked statement
- checked statement
- checked statement
- checked statement
- checked statement
- checked statement
- checked statement
- checked statement
- checked statement
- checked statement
- checked statementFirst variation of the printed phase matrix about an unmixed S-wave background. The real parameter is a formal expansion-family parameter, not necessarily momentum. Vanishing background mixing and D-wave phases leave independent first-order terms; they do not make those predictions zero.
- checked statementThe displayed matrix determines the leading mixing and D-wave phases on the declared branch. The vanishing amplitudes are calculation input; the phase-zero consequence is not.
- checked statement
- checked statement
- checked statement
- checked statement
- checked statement
- checked statement
- checked statement
- checked statement
- checked statement
- checked statement
- checked statement
- checked statement
- checked statement
- checked statement
- checked statement
- checked statement
- checked statement
- checked statement
- checked statement
- checked statement
- checked statement
- checked statement
- checked statement
- checked statement
- checked statement
- checked statement
- checked statement
- checked statement
- checked statement
- checked statement
- checked statement
- checked statement
- checked statement
- checked statement
- checked statement
- checked statement
- checked statement
- checked statement
- checked statement
- checked statement
- checked statement
- checked statement
- checked statement
- checked statement
- checked statement
- checked statement
- checked statement
- checked statement
- checked statement
- checked statement
- checked statement
- checked statement
- checked statement
- checked statement
- checked statement
- checked statementKSW v2 pp. 8-9: fitting the coupled S-wave leaves the mixing/D-wave target parameter-free at its lower calculated order. This establishes a prediction, not agreement with an independently supplied target value or uniform subleading completion.
- checked statement
- checked statement
- checked statement
- checked statement
- checked statement
- checked statement
- checked statement
- checked statement
- checked statement
- checked statement
- checked statement
- checked statement
- checked statement
- checked statement
- checked statementLow momentum relative to the interaction range does not make ordinary MS uniformly valid in the large-scattering-length regime. The additional `p << 1 / |a|` window can still exclude a pionless momentum.
- checked statement
- checked statement
- checked statementA fixed-scale diagnostic in chosen numerical units, using the complete retained amplitude. At m=mu=1 the reported (C0,D2)=(-3/2,1) and alternative (-5/2,2) give the same curve. These replacements are not RG trajectories or a fit to nuclear data.
- checked statement
- checked statement
- checked statementThe same interacting amplitude needs graph V for retained-order RG cancellation, although that insertion is small relative to the leading Q^(-1) term as Q tends to zero from above. This compares it with the leading contact amplitude, not with the other Q^0 pion terms. The reconstructed retained grades are used, not a claim about the full EFT error.
- checked statement
- checked statement
- checked statement
- checked statement
- checked statement
- checked statement
- checked statement
- checked statement
- checked statement
- checked statement
- checked statement
- checked statement
- checked statement
- checked statement
- checked statement
- checked statement
- checked statement
- checked statement
- checked statement
- checked statement
- checked statement
- checked statement
- checked statement
- checked statementThe paper adapter uses the same two exposed exponents as the concrete chain argument, rather than an independently assignable resummation flag.
- checked statement
- checked statementThe interpretation bridge follows from the actual fitted amplitude invariance and calibrated readout. It is not an additional source input.
- checked statement
- checked statement
- checked statement
- checked statementThe missing next-order mixing and D-wave calculations concern degree two, not the already supplied background or degree-one terms. Missing calculation is not a statement that either physical coefficient vanishes.
- checked statementThe amplitude through order p^0 supplies common phase degree one. That is next-to-leading for delta_0 but only leading for epsilon_1 and delta_2. It must not be confused with the earlier zero-mixing background.
- checked statement
- checked statementThe first correction relative to the S-wave background is supplied, but not the first correction relative to each other observable's leading term. All three observables can still share common phase degree one.
- checked statementThe completed coupled-channel route retains KSW's literal displayed S-matrix relation rather than only its named zero-phase consequence.
- checked statement
- checked statement
- checked statement
- checked statementReading an old cumulative predicate as the pointwise input preserves every degree exactly when that old predicate was downward closed. Arbitrary old flags with holes do not have the intended cumulative meaning.
- checked statement
- checked statement
- checked statement
- checked statement
- checked statement
- checked statementThe raw coupled-channel route structurally explains the selected post-calibration mixing-angle prediction without consuming the established shared endpoint.
- checked statement
- checked statementKSW's selected coupled-channel route directly realizes the shared post-calibration prediction at its named model: the large-length description, S-wave fit, excluded mixing-angle target, no-additional-fit result, and declared-order prediction hold together. Primary-source anchors: arXiv v2 pp. 8-9, especially the coupled 3S1-3D1 discussion, the fit of the three A00 parameters, and the statement that epsilon-one and delta-two have no free parameters after fitting delta-zero.
- checked statementThe selected coupled-channel target forms an active neutral prediction sector.
- checked statement
- checked statementThe v2 abstract and coupled-channel discussion select the large scattering length EFT and analogous power counting before the S-wave fit or mixing-angle prediction. Those validity facts ground the model independently of the fit and prediction route.
- checked statementFull readout preservation, not merely preservation of a phase-zero consequence. The former independent S - 1 family is fixed exactly by its normalization once the other four data selections agree.
- checked statementThe original coupled S-wave fit and parameter-free mixing prediction realize the source-sensitive shared explanation without consuming the established endpoint or ordinary explanation.
- checked statementThe generated normalization discharges only the duplicate matrix readout. Positive mass and agreement with the entire phase matrix remain.
- checked statementThe derived residual retains the former sampled little-o obligation. This follows from actual threshold matching; exact reconstruction by itself would not imply this limit.
- checked statement
- checked statement
- checked statement
- checked statement
- checked statement
- checked statement
- checked statement
- checked statementMatching identifies the coefficients on every admissible physical sampling family. This is the input consumed by the actual RG/amplitude argument; the residual reconstruction identity is not used as calibration.
- checked statementEliminating a separately chosen residual preserves the entire uniform threshold condition exactly, when that residual reconstructs the observable on the physical domain. No equality is asserted outside that domain. The uniform small-residual condition is essential; the identity alone does not calibrate the two coefficients.
- checked statement
- checked statement
- checked statement
- checked statement
- checked statement
- checked statement
- checked statement
- checked statement
- checked statementOne set of assigned exponents determines both the required bubble sector and the derivative insertions retained through the first correction. The two source routes cannot choose their leading-contact orders separately.
- checked statement
- checked statement
- checked statement
- checked statement
- checked statementThe nominal source contract supplies a genuinely nonzero explicit-log response, without claiming a total scale derivative or nominal RG invariance.
- checked statement
- checked statement
- checked statement
- checked statement
- checked statement
- checked statementThe former two-scale graph contract is recovered by retaining its extra variation witness. The explicit-log contract alone does not supply it.
- checked statement
- checked statement
- checked statement
- checked statement
- checked statement
- checked statement
- checked statement
- checked statement
- checked statement
- checked statement
- checked statement
- checked statement
- checked statement
- checked statementKSW's typed source derivation reconstructs the raw shared route rather than storing an established post-calibration prediction.
- checked statementPrinted v2 eqs. (5)-(13) compose the actual pionless bubble sum and its mixed expansion with the independent pion-inclusive RG cancellation. No equality between the full-contact PDS amplitude and the full physical target is assumed.
- checked statementThe original PDS resummation, pion-inclusive RG cancellation, and mixed expansion remain three independently visible source derivations. Exact selection of both shared child contexts prevents the later full amplitude from silently replacing the paper's pionless two-nucleon result.
- checked statement
- checked statement
- checked statement
- checked statement
- checked statement
- checked statement
- checked statement
- checked statementThe actual observable/contact family fixes the two pionless source terms. The coefficient matches are derived from that family, not independently supplied. The displayed graph calculation and range naturalness remain inputs. These two terms agree at every other nonpole scale at which the same graph formula holds; no full-amplitude invariance or physical remainder bound is assumed or concluded.
- checked statementThe actual observable family now determines equation (11), instead of assuming it as the output of the RG calculation. The imported obligations are the ERE remainder, the contact coefficients and their physical readout.
- checked statementExact accounting for the old contract: the new normalization contract is equivalent only after retaining the upstream supply of the bubble formula. This removes a duplicate supplier, not an independent physical assumption.
- checked statementPreservation on one source channel/order does not require global normalization of an old readout outside that selected slice.
- checked statement
- checked statement
- checked statement
- checked statement
- checked statement
- checked statementComplete readout preservation on the already selected nonrelativistic shell. The independent old energy family is replaced, not its physical interpretation, loop values, contact interaction or amplitude. Equality transports every formula claim, including all loop powers.
- checked statement
- checked statement
- checked statement
- checked statement
- checked statement
- checked statementA former readout with the same full and retained coefficients equals the generated one exactly when its bookkeeping identity holds. The entire omitted family is fixed; no order or smallness assumption is discharged.
- checked statementExact coefficient bookkeeping, not the physical truncation claim.
- checked statementExact correspondence of the whole pointwise contract, shared-family contract and counterterm endpoint. Singlet identification is not discarded.
- checked statement
- checked statement
- checked statement
- checked statement
- checked statement
- checked statementThe scale-cancellation argument forces a nonzero retained insertion somewhere in the represented scale domain. It does not require nonzero D2 at each scale: the finite contact value can vanish at a chosen subtraction point while its inhomogeneous running is still essential.
- checked statementExact recovery of the previous whole-jet contract. Its domain, interacting witness, running equations and all four readouts are retained.
- checked statementExact preservation of the former separately chosen scale-domain contract. The two coverage clauses force that domain to be the image of the scale map; the interacting real witness therefore has an abstract scale representative.
- checked statementThe with/without conclusion is derived from the same graded calculation, not supplied by a pair of scale-independence hypotheses.
- checked statementReference values and a single running jet give exactly the same momentum-family contract. A member is needed to establish the physical domain when reconstructing the common flow, not to choose new couplings.
- checked statement
- checked statementThe reconstruction preserves the entire calibrated jet, including all four functions, not merely its amplitude at a chosen subtraction point.
- checked statementEquality of the entire former flow, not merely selected sample values. Any property of a calibrated old flow is preserved by this reconstruction.
- checked statementThe mass calibration formerly supplied alongside the numerical coupling readout is now definitional; the complete previous contract is retained.
- checked statement
- checked statement
- checked statement
- checked statement
- checked statement
- checked statement
- checked statement
- checked statement
- checked statement
- checked statementThe direct shared endpoint uses the paper's exact full-amplitude equality. Residual subtraction-scale dependence of an order-truncated amplitude remains in the paper-local finite-order route.
- checked statement
- checked statement
- checked statementThe original pion-inclusive running-and-matching route realizes a source-sensitive shared explanation without consuming the established shared prediction. Primary-source anchors: original arXiv v2 pp. 5-7, especially equations (13)-(18) and the scale-independent full-amplitude conclusion.
- checked statement
- checked statementThe former all-positive-scales contract is recovered when every positive scale is represented. Without this coverage, equations outside the selected neighborhoods are not part of the source contract.
- checked statement
- checked statement
- checked statement
- checked statement
- checked statementObservable matching constrains the same contact that produced the bubble amplitude. This is pointwise, with the entire ERE remainder retained; no coefficient identity, naturalness, or remainder bound follows from it alone.
- checked statementUnder the separate observable matching input, exact elimination of the former independently selected contact family and duplicate nonzero clauses. The coefficient limit keeps the denominator nonzero near threshold at each fixed nonpole scale. No uniform neighborhood, value at zero, or off-domain contact equality is inferred. Without observable matching the reduced contact-only contract is weaker, not equivalent.
- checked statement
- checked statement
- checked statementKSW's raw PDS loop, bubble-chain, and unitarity inputs realize the ordinary structural explanation of the selected resummed low-energy behavior without consuming an established endpoint or derivational-reduction result.
- checked statement
- checked statementThe PDS loop, all-orders bubble sum, and unitary-amplitude recovery realize the shared derivational reduction without consuming an established resummation endpoint.
- checked statement
- checked statementKSW's typed PDS derivation realizes the source-sensitive structural explanation while keeping its loop-and-bubble provenance distinct from the dressed-dibaryon route.
- checked statement
- checked statement
- checked statement
- checked statement
- checked statementThe source RG route supplies a real family, not only an opaque beta label.
- checked statementThe completed pionless RG route retains KSW's displayed equation-(11) couplings instead of forgetting them behind a named running-solution output.
- checked statementKSW's typed PDS derivation reconstructs the model-native raw resummation route without storing an established endpoint or ordinary explanation.
- checked statementKSW's raw PDS inputs realize a source-sensitive large-length derivational reduction without identifying the PDS loop-and-bubble construction with the dressed-dibaryon route of Bedaque, Hammer, and van Kolck. Primary-source anchors: original arXiv v2 pp. 2-5, especially eqs. (4)-(7) for PDS subtraction, the bubble sum, and unitarity, and printed eq. (13) with the preceding all-orders `C₀` power-counting argument.
- checked statement
- checked statement
- checked statement
- checked statementThe counterterm conclusion means equality of both retained coefficients with D2 and a coefficient mismatch without D2. The graded calculation below derives this witness from explicit formula/readout identifications.
- checked statement
- checked statement
- checked statement
- checked statement
- checked statement
- checked statement
- checked statement
- checked statementKernel-checked literal readback of the consolidated sampled formulas.
- checked statement
- checked statementThe former output pair is recovered only after the old completeness marker is identified with the actual coefficient condition. Arbitrary uninterpreted verdicts are not preserved by this semantic repair.
- checked statement
- checked statementThe scale choice is precisely a bounded dimensionless ratio, with a single factor fixed in the framework rather than quantified after p and mu.
- checked statement
- checked statement
- checked statement
- checked statementChanges to the rest of the paper adapter cannot change these complete singlet coefficient contracts when the nine projected data agree. This is a sufficient footprint, not a claim that its fields are independent or minimal. Only the two retained coefficients must agree; higher orders can differ.
- checked statementReconstruction preserves the entire old jet exactly when its constants are calibrated and its four contact functions are the selected functions. This preserves every property of that jet, not only one amplitude sample.
- checked statement
- checked statementThe three quoted fit values do not make `C0` and `D2` separately interpretable at order `p^0`. The same fit calculation retains the combination-only amplitude statement, and the paper's parenthetical interpretation consumes that statement before returning the qualification.
- checked statement
- checked statement
- checked statement
- checked statement
- checked statement
- checked statement
- checked statement
- checked statement
- checked statement
- checked statement
- checked statement
- checked statement
- checked statement
- checked statementBoth momenta support interacting RG trajectories on the positive scale domain, but these two amplitude readouts cannot belong to a single contact family. Momentumwise existential choices therefore lose physical content.
- checked statement
- checked statement
- checked statement
- checked statement
- checked statement
- checked statement
- checked statement
- checked statement
- checked statementAbsorbing D2 does not eliminate its mass-dependent running. This is the RG equation of s+d*m^2, not the original mass-independent equation for s.
- checked statementAt one fixed mass, the entire retained formula can hide graph V in the subleading contact. This changes s, unlike withoutMassInsertion. The literal identity does not evaluate the separate physical threshold limits of II/III.
- checked statementThe former explicit denominator restriction was redundant on this positive-momentum domain. This equivalence preserves its entire contract.
- checked statement
- checked statement
- checked statement
- checked statementThe short source specification and the algebraic normal form agree; there are not two independently chosen amplitude definitions.
- checked statement
- checked statement
- checked statement
- checked statement
- checked statementExact replacement of the four differential equations on the complete open connected domain by their reference-scale reconstruction. Values and derivatives outside that domain remain unconstrained.
- checked statementAll four running functions are fixed on the physical domain by their values at one interacting reference scale. No values outside that domain are identified, and no all-orders nominal trajectory is asserted.
- checked statement
- checked statement
- checked statement
- checked statement
- checked statement
- checked statement
- checked statement
- checked statement
- checked statement
- checked statement
- checked statementAt a fixed positive momentum and subtraction point the leading amplitude identifies the real contact. No choice of subleading contacts can conceal a different leading interaction.
- checked statement
- checked statementAt fixed real dressing, momentum and scale, the explicit logarithmic coefficient cannot be canceled at two masses by a single mass-independent constant/derivative contact shift. The quantified a,b are shared between the masses. This tests the retained operator basis, not arbitrary scheme changes or the chiral identification of m_pi^2 with quark masses.
- checked statement
- checked statementThe same finite-PDS prediction, with a compensating subleading C0 shift. This is not an exact finite shift of the full nominal C0.
- checked statement
- checked statement
- checked statement
- checked statementOnce the four reference values are fixed, scale cancellation is an algebraic identity at every positive regular scale. No open or connected set of sampled scales is needed for this direction of the argument.
- checked statement
- checked statement
- checked statement
- checked statement
- checked statement
- checked statement
- checked statement
- checked statementThe leading amplitude fixes the running contact at every scale in the connected domain. In particular, an interacting solution cannot cross zero or its reconstruction pole inside that domain.
- checked statementTwo distinct positive regular scales already distinguish the omitted counterterm prediction. They need not form an open or connected set.
- checked statementThe uncanceled scale dependence is the source's logarithmic prefactor times log(mu/reference), with every other calibrated datum held fixed.
- checked statement
- checked statement
- checked statement
- checked statement
- checked statement
- checked statement
- checked statement
- checked statement
- checked statement
- checked statement
- checked statement
- checked statement
- checked statement
- checked statement
- checked statement
- checked statement
- checked statement
- checked statement
- checked statement
- checked statementRetained predictions use the constants and contact values at the selected scale, not unobserved choices of functions outside that scale.
- checked statementComplete retained-order counterterm argument. With the mass insertion both coefficients are scale independent; removing that graph changes a first-order prediction arbitrarily near an interacting admissible scale. The other coupling data are held fixed. Absorbing D2 into s at one mass is a different operation, whose prediction and modified RG law are given below.
- checked statementOn a regular leading S-matrix, the source normalization loses neither retained coefficient. Zero momentum and a zero leading S-matrix are not covered by this equivalence.
- checked statement
- checked statement
- checked statementThe same complete coefficient, not a separate fit relation: at fixed c,r,M,gA,f, one positive momentum already distinguishes different s+d*m^2. Conversely, equal combinations give equal predictions at every positive p.
- checked statement
- checked statement
- checked statement
- checked statement
- checked statement
- checked statement
- checked statement
- checked statement
- checked statement
- checked statement
- checked statement
- checked statement
- checked statement
- checked statement
- checked statement
- checked statement
- checked statement
- checked statement
- checked statement
- checked statement
- checked statement
- checked statement
- checked statement
- checked statement
- checked statement
- checked statement
- checked statement
- checked statement
- checked statement
- checked statementRescaling the printed beta0 by Q exposes the leading and subleading C0 equations and an explicit higher-order remainder.
- checked statement
- checked statement
- checked statement
- checked statement
- checked statement
- checked statement
- checked statement
- checked statement
- checked statement
- checked statement
- checked statement
- checked statement
- checked statement
- checked statement
- checked statement
- checked statement
- checked statement
- checked statement
- checked statement
- checked statement
- checked statement
- checked statement
- checked statement
- checked statement
- checked statement
- checked statement
- checked statement
- checked statement
- checked statementAt a fixed mass, shifting the subleading part of C0 against D2 leaves the entire first coefficient unchanged, including all the pion graphs.
- checked statement
- checked statement
- checked statement
- checked statement
- checked statement
- checked statement
- checked statement
- checked statement
- checked statement
- checked statement
- checked statement
- checked statementA dressed insertion separates its homogeneous running from the source. This helper covers C2, D2, and the subleading part of C0.
- checked statement
- checked statement
- checked statement
- checked statement
- checked statement
- checked statement
- checked statement
- checked statement
- checked statement
- checked statement
- checked statement
- checked statement
- checked statement
- checked statement
- checked statement
- checked statement
- checked statement
- checked statement
- checked statement
- checked statement
- checked statement
- checked statement
- checked statement
- checked statement
- checked statement
- checked statement
- checked statement
- checked statement
- checked statement
- checked statement
- checked statement
- checked statement
- checked statementThe source's first phase correction alpha*p*A1/(1+2*i*alpha*p*A_-1) is real. This does not choose a branch for the leading phase shift.
- checked statement
- checked statement
- checked statement
- checked statement
- checked statementThe source-level omission uses the same leading and derivative contacts, not an independently selected amplitude family.
- checked statement
- checked statement
- checked statement
- checked statement
- checked statement
- checked statement
- checked statement
- checked statement
- checked statement
- checked statement
- checked statement
- checked statement
- checked statement
- checked statement
- checked statement
- checked statement
- checked statement
- checked statement
- checked statement
- checked statement
- checked statement
- checked statement
- checked statement
- checked statement
- checked statement
- checked statement
- checked statement
- checked statement
- checked statement
- checked statement
- checked statement
- checked statement
- checked statement
- checked statement
- checked statementThe complete readout-level inference uses the actual coefficient/RG calculation, including a nonzero interacting witness and the sampled domain.
- checked statementCompatibility with the original open, connected source contract. The deduction uses only its calibration and the existence of distinct scales.
- checked statementCalibration already ensures the retained prediction is constant with graph V. Two distinct sampled scale values are necessary and sufficient to detect its omission; openness and connectedness supply no additional content.
- checked statementThe same coefficient calculation has a unitary leading elastic value and real local phase increments. Removing graph V preserves the leading value but makes the first phase increment depend on subtraction scale. No extra phase data, branch choice, fit or truncation bound is assumed.
- checked statementAn exact change of readout, not a separately assigned phase-invariance predicate. The normalization and regular leading S-matrices are explicit; the calculation below derives these conditions on its physical domain.
- checked statement
- checked statement
- checked statement
- checked statement
- checked statement
- checked statement
- checked statement
- checked statement
- checked statement
- checked statement
- checked statement
- checked statement
- checked statement
- checked statement
- checked statement
- checked statement
- checked statement
- checked statement
- checked statement
- checked statement
- checked statement
- checked statement
- checked statementResponse of the explicit log term alone. The prefactor is evaluated at mu and held fixed; this is not the total derivative of the running graph.
- checked statement
- checked statement
- checked statement
- checked statement
- checked statement
- checked statement
- checked statement
- checked statement
- checked statement
- checked statement
- checked statementCancellation of the explicit logarithm by the mass insertion at fixed C0 dressing. Other scale-dependent terms and running of that dressing are separate parts of the full RG calculation.
- checked statement
- checked statement
- checked statementOn the finite massive domain, a logarithmic term is present exactly when both interactions entering its prefactor are nonzero.
- checked statement
- checked statement
- checked statementReality of the contact and positive momentum exclude a zero complex dressing. The separate threshold case does not have this guarantee.
- checked statement
- checked statement
- checked statement
- checked statement
- checked statement
- checked statement
- checked statement
- checked statement
- checked statement
- checked statement
- checked statement
- checked statement
- checked statementThe C2 equation is homogeneous. Setting C2 to zero preserves all three retained equations without changing the C0 or D2 family, the mass, or either pion parameter. Thus those equations do not require every coupling to vary.
- checked statement
- checked statement
- checked statement
- checked statement
- checked statement
- checked statement
- checked statement
- checked statement
- checked statement
- checked statement
- checked statement
- checked statement
- checked statement
- checked statement
- checked statement
- checked statement
- checked statement
- checked statement
- checked statement
- checked statement
- checked statement
- checked statement
- checked statement
- checked statement
- checked statement
- checked statement
- checked statement
- checked statement
- checked statement
- checked statement
- checked statement
- checked statementThe source expansion solves the scalar contact scattering equation through first order in a real insertion-counting parameter. The remaining quadratic term is explicit. This characterization does not claim that the truncated sum solves the full equation at parameter one.
- checked statementArbitrary higher interaction and amplitude tails do not alter the two retained equations. This is equality of formal coefficients only: their numerical value at insertion parameter one need not be small or even defined.
- checked statementExact preservation of the former two-equation specification, including mass and zero-momentum domains. The single-insertion equation is coefficient one of the same residual as the leading equation, not an extra chosen rule.
- checked statementKernel-checked preservation of the previous reduced specification. The nonpole condition follows from the leading equation, even at zero momentum.
- checked statementExact readback of printed equation (13). This equivalence includes the old mass, zero-momentum and nonpole domain: normalization is invertible only because the mass is positive. No running or effective-range matching is required, and a zero leading contact remains allowed.
- checked statement
- checked statement
- checked statement
- checked statement
- checked statement
- checked statement
- checked statement
- checked statement
- checked statement
- checked statement
- checked statement
- checked statement
- checked statement
- checked statement
- checked statement
- checked statement
- checked statement
- checked statement
- checked statement
- checked statement
- checked statement
- checked statement
- checked statement
- checked statement
- checked statement
- checked statement
- checked statement
- checked statement
- checked statement
- checked statement
- checked statementThe phase-function remainder is a separate quantitative input. The inverse readout in printed equation (7) transfers it only with the selected positive-momentum stability scale; the PDS formula alone is not an error bound.
- checked statement
- checked statement
- checked statement
- checked statement
- checked statement
- checked statement
- checked statementThe chosen nonrelativistic shell determines the entire energy family. This is not a derivation of the shell from relativistic nucleon dynamics; the source neglects energy-momentum corrections after author TeX label 1 and in the footnote preceding label 6.
- checked statement
- checked statement
- checked statement
- checked statement
- checked statement
- checked statement
- checked statement
- checked statement
- checked statement
- checked statement
- checked statement
- checked statement
- checked statement
- checked statement
- checked statement
- checked statement
- checked statementFor every fixed finite nonzero scattering length, sufficiently small positive momentum leaves the enhanced-counting window.
- checked statementEven mu = p > 0 can hit the pole for a positive scattering length. Comparability alone cannot replace the inverse-length window premise.
- checked statement
- checked statement
- checked statement
- checked statement
- checked statement
- checked statement
- checked statement
- checked statement
- checked statement
- checked statement
- checked statement
- checked statementEquation (11) implies nonconstant C0 on positive non-pole scales. C2 varies there exactly when the effective range is nonzero. Values at the excluded pole cannot witness running, and no coverage of an abstract sampled scale type is assumed.
- checked statement
- checked statement
- checked statement
- checked statement
- checked statement
- checked statement
- checked statement
- checked statement
- checked statementThe first derivative contact is fixed by the same running solution and the effective range. No independent C2 scaling premise is needed. Zero or negative effective range is retained; no natural-size bound is inferred.
- checked statementEquation (11) is exactly the first two finite matching equations, with g_n = M C_(2n)/(4 pi) and k_1 = r0/2. The higher matching hierarchy therefore extends these same coefficients rather than an unrelated scaling model.
- checked statement
- checked statement
- checked statement
- checked statement
- checked statement
- checked statement
- checked statement
- checked statement
- checked statement
- checked statementComplete quantitative resummation argument after observable matching has fixed the running contacts (source labels 11 and 14). The mass, inverse length, range and two running functions are the only model data. The two local interaction equations refer to these same contacts and actual amplitudes. The scale window derives the nonpole domain and two-sided leading-contact bounds. The range-size input bounds the first derivative correction. Exact finite-loop errors show why raw loop truncation and derivative truncation are different questions. The subtraction scale is not specialized to momentum. These conclusions do not control omitted physical terms, validate assigned orders, or establish nuclear applicability. No source-map interpretation or other sector of the paper is an input.
- checked statement
- checked statement
- checked statement
- checked statementThe observable-to-prediction argument without the full paper adapter. The five flow fields, one phase family and one contact family determine the running values and derivatives. At any nonpole scale, the two explicit local scattering equations then determine the reduced amplitudes. The same output formulas at every scale imply their scale independence. No full-amplitude invariance, independently supplied coefficient matches or assigned orders are inputs. The prediction momentum is distinct from the threshold-limit variable. Naturalness bounds this first correction, not the omitted physical remainder. Source: author TeX labels 8, 9, 11 and 14 (printed two-term equation (13)).
- checked statementSource labels 8, 9 and 11: a single observable family, independent of mu, fixes both running contacts through its actual low-momentum coefficients. Contact coefficients are limits of the same function in the inverse-amplitude identity, not assigned orders or a separately supplied solution.
- checked statementOriginal author TeX labels 8, 9, 11 and 14: one scale-independent observable germ fixes the same running contacts used in the interaction calculation. Its normalized contact germ is explicitly -1/(K+mu), not a second freely chosen function with a separate inverse-amplitude premise. The conclusion combines running, actual beta derivatives, the resummed amplitudes, first-order unitarity and raw-loop error. Its entire statement uses the five flow fields and explicit mathematical expressions; no assigned order, validity flag or independently supplied running solution occurs. The prediction momentum is not the threshold variable. The two local equations remain imported PDS calculations. Naturalness is a separate input. The scale-window bounds do not assert a fixed-a infrared limit, and neither the optical defect nor the small first insertion bounds the omitted physical terms. This is the complete first-order value argument, not the higher-contact counting, explicit-pion or empirical-fit routes.
- checked statementA nonempty, jointly controlled first-order PDS window, not just separate conditional loop and range estimates. The dimensionless c, rho and epsilon are fixed before p and mu. The scale separation makes the open interval |alpha|/rho < p < epsilon*Lambda/(B+1) inhabited. Throughout it, every comparable scale gives a raw leading-loop error at least as large as the leading term, while the dressed first correction is smaller than epsilon times that term. The two local equations have a unique numerical solution; their identification with the physical PDS calculation remains external. These are sufficient estimates derived here from author TeX labels 8, 9, 11 and 14, not source error bars. The result retains running, beta derivatives, leading and linearized unitarity, the exact optical defect and every finite loop error. It assumes no assigned contact orders, controls no unsupplied higher contact or physical remainder, and does not establish nuclear applicability. Infinite scattering length alpha=0 is allowed. For fixed nonzero alpha the interval does not reach p=0.
- checked statement
- checked statementThe running values derived by the observable route determine the actual two terms supplied by the interaction route. All scales use the same mass, couplings and range; no assigned counting order is needed for this bound.
- checked statementQuantitative C0 and C2 power counting on the same finite scale window. The two-sided C2 estimate degenerates correctly when r0 = 0. To interpret the derivative insertion as suppressed one still needs a natural-range and low-momentum condition; higher contacts are not covered by (11).
- checked statementOn a scale window with |1/a| <= rho * mu and rho < 1, the subtraction scale stays away from the contact pole. Equation (11), rather than an independently assigned exponent, bounds the dimensionless leading contact. Setting mu = p gives two-sided p^(-1) counting on that window; this is not the limit p -> 0 at fixed nonzero a. Nonnegative rho follows from the window; the bound is the same normalized matching bound used for actual chains.
- checked statement
- checked statement
- checked statement
- checked statement
- checked statement
- checked statement
- checked statement
- checked statement
- checked statement
- checked statement
- checked statementThe complete pointwise implication of printed v2 equations (5)-(6). The bubble sum is an explicit input, not a proved loop calculation. Positive mass and nonnegative momentum delimit the source's nonrelativistic channel; the algebra also holds beyond those inequalities. Reality of the contact, the nonpole condition, and the source normalization are not hidden predicates. No error estimate, potential realization, or relativistic extension follows.
- checked statement
- checked statement
- checked statement
- checked statement
- checked statement
- checked statement
- checked statement
- checked statement
- checked statement
- checked statement
- checked statement
- checked statement
- checked statement
- checked statement
- checked statement
- checked statement
- checked statement
- checked statement
- checked statement
- checked statement
- checked statement
- checked statement
- checked statement
- checked statement
- checked statement
- checked statement
- checked statement
- checked statement
- checked statement
- checked statement
- checked statement
- checked statement
- checked statement
- checked statement
- checked statement
- checked statement
- checked statement
- checked statement
- checked statement
- checked statement
- checked statement
- checked statement
- checked statement
- checked statement
- checked statement
- checked statement
- checked statement
- checked statement
Constructors, projections, and other meaning dependencies
- constructor
- constructor
- constructor
- constructor
- constructor
- constructor
- constructor
- constructor
- recursor
- constructor
- constructor
- constructor
- constructor
- constructor
- constructor
- constructor
- constructor
- constructor
- constructor
- constructor
- constructor
- constructor
- constructor
- constructor
- constructor
- recursor
- constructor
- constructor
- constructor
- constructor
- constructor
- constructor
- constructor
- constructor
- constructor
- constructor
- constructor
- constructor
- constructor
- constructor
- recursor
- constructor
- constructor
- constructor
- constructor
- constructor
- constructor
- constructor
- constructor
- constructor
- constructor
- constructor
- constructor
- constructor
- constructor
- constructor
- recursor
- constructor
- constructor
- constructor
- constructor
- constructor
- constructor
- constructor
- constructor
- constructor
- constructor
- constructor
- constructor
- constructor
- constructor
- constructor
- constructor
- constructor
- constructor
- constructor
- constructor
- constructor
- constructor
- recursor
- constructor
- constructor
- constructor
- constructor
- constructor
- constructor
- constructor
- constructor
- constructor
- recursor
- constructor
- constructor
- constructor
- constructor
- constructor
- constructor
- constructor
- constructor
- constructor
- recursor
- constructor
- constructor
- constructor
- recursor
- constructor
- constructor
- constructor
- constructor
- constructor
- constructor
- constructor
- constructor
- constructor
- constructor
- constructor
- constructor
- recursor
- constructor
- constructor
- constructor
- constructor
- constructor
- constructor
- constructor
- constructor
- constructor
- constructor
- constructor
- constructor
- constructor
- recursor
- constructor
- constructor
- constructor
- constructor
- recursor
- constructor
- constructor
- recursor
- constructor
- recursor
- constructor
- recursor
- constructor
- recursor
- constructor
- recursor
- constructor
- recursor
- constructor
- recursor
- constructor
- recursor
- constructor
- recursor
- constructor
- constructor
- recursor
- constructor
- constructor
- recursor
- constructor
- recursor
- recursor
- constructor
- constructor
- recursor
- recursor
- constructor
- constructor
- recursor
- constructor
- recursor
- constructor
- recursor
- constructor
- recursor
- constructor
- constructor
- constructor
- recursor
- constructor
- recursor
- constructor
- recursor
- constructor
- recursor
- constructor
- recursor
- constructor
- recursor
- constructor
- recursor
- constructor
- recursor
- constructor
- constructor
- constructor
- constructor
- constructor
- constructor
- constructor
- constructor
- constructor
- constructor
- constructor
- recursor
- constructor
- constructor
- constructor
- constructor
- constructor
- constructor
External mathematical declarations
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
Physical premises, route dependencies, outputs, and qualifiers below are exposed by the Lean semantics and their source, coverage, and fidelity ledgers. Loop integration, bubble summation, pion-inclusive beta calculations, and phase-branch extraction remain imported calculations. The actual pionless running solution and beta derivatives are now derived from the explicit observable/contact coefficient contract. Printed equations (4), (5), (11), and (13), together with the coupled-channel S-matrix, retain value-level formulas and domains. Algebraic theorems derive normalization, first-order unitarity, and the quadratic truncation defect. Historical public identifiers EquationFivePDSLoopAt and EquationSixPDSAmplitudeAt are retained for compatibility; their printed source numbers are (4) and (5). The author TeX label 14 denotes the printed two-term equation (13), not the following pion potential. These checks do not establish physical fidelity by themselves.
Observable matching, running and the first pionless correction
New retained-pion argument: inspect the complete counterterm calculation, or see its formulas and assumption boundary. The compact model and the larger paper adapter are separate unreviewed scopes.
Assessment: the Lean argument faithfully captures this conditional distinction in the supplied scalar, on-shell pionless model. It does not yet certify a controlled approximation to an actual nuclear amplitude. This is an automated source assessment, not recorded human approval.
Actual threshold matching, not a free remainder identity
The paper adapter now computes R(p)=K(p)-[-1/a+(r0/2)q(p)²] from the observable K and physical momentum q(p). This removes one stored function. The former effectiveRangeDataMatched only equated K with a polynomial plus a freely chosen R; that did not identify a or r0.
|(K(p)+1/a)/q(p)²-r0/2|<ε.
The finite-length chart excludes a=0; the standalone inverse-length model separately allows the unitary limit. The revised condition also requires a family realizing positive momenta near zero, so an empty physical domain cannot satisfy it. The radius is chosen before the momentum. This is a stronger, explicit correction of the old matching predicate, not a claimed equivalence to its weaker meaning or to matching one selected curve. It describes the model's observable function, not exact parameter inference from finite experimental data.
The effective_range_matching_iff_uniform_remainder theorem preserves the equivalent uniform small-remainder formulation for any R reconstructing K on this domain. The actual coefficient limit and sampled R/q²→0 are derived and used by the existing RG and amplitude routes. There is no equality claim for an independently supplied R outside the domain, and no implied quartic bound or finite-momentum truncation estimate.
The Lean examples and counterexamples include finite a=-1000, r0=1 and a nonzero quartic residual through the running-coupling conclusion. Wrong r0 and conflicting momentum labels are rejected. The value at exactly zero can remain unrelated to the punctured limit. At that earlier stage the framework had 73 stored fields, including the explicit pion mass and nominal mass-insertion readout; this is not an independent-assumption count or human approval. Subsequent consolidations are accounted for below.
One regime: failed raw loops, small dressed correction
The larger paper adapter now uses this same numerical comparison: one stored factor c≥1, p>0 and p/c≤μ≤cp. The former freely assignable scaleComparableToMomentum field is now a derived predicate. Lean proves its equivalence to 1/c≤μ/p≤c and its incompatibility with minimal subtraction. The factor is fixed before any pair is selected; it cannot be enlarged separately at each momentum. The adapter examples check both boundaries, reject zero and out-of-window values, and use the predicate in this complete argument. Comparability can still hit the contact pole; the nonpole and enhanced-regime conditions below remain necessary. This is a finite-window interpretation of the source prescription, not a derivation of assigned orders or an equivalence to the old arbitrary predicate.
The primary review statement is now PionlessRGFlow.observable_matching_realizes_a_controlled_resummation_window. It connects the matched running contacts to a nonempty interval, not just separate conditional estimates. Choose fixed c≥1, ρ>0 and 0<ε<1, with ρ²+2cρ≤1. Write α=1/a, k1=r0/2 and |Λk1|≤B.
For every p in it and p/c≤μ≤cp:
|f1|≤(Bp/Λ)|f0|<ε|f0|; |SN-f0|=RN+1|f0|≥|f0|.
The same theorem gives a nonpole scale, unique numerical solutions of the local PDS equations, both amplitude formulas, actual running and beta derivatives, exact leading unitarity, the linearized optical theorem and the quadratic optical defect. It assumes no assigned contact orders. The complete literal Lean contract also checks finite a=-1000 and nonzero r0=Λ=1 in chosen units: c=2, ρ=1/8 and ε=1/10 give the entire interval 1/125<p<1/15 with p/2≤μ≤2p. It is not just a unitary-limit example.
Assessment and limits: this sufficient window is our deduction from the source formulas, not KSW error bars. Its precision concerns the first insertion, not the unknown physical remainder. A matched negative-a diagnostic keeps the momentum window but takes μ far above p: the tree's error is smaller than the resummed term, so dropping μ≤cp invalidates the stated raw-loop obstruction. A unique scalar-model solution is not proof that a nuclear amplitude obeys the imported PDS calculation. The source normalization, pionless applicability, higher-contact naturalness and generic assigned-order interpretation remain external. No new production physical definition or field was added; no reduction in independent semantic choices or human approval is claimed. The earlier complete statements below retain their exact signatures and every output.
Start here: the connected first-order physics argument
The earlier standalone value statement is PionlessRGFlow.observable_matching_controls_the_complete_first_order_argument, not an isolated correction bound. Its only project-defined object is the existing proof-free data M, α, r0, C0(μ) and C2(μ). The complete canonical Lean specification displays every premise and conclusion without project-defined physical predicates. The former complete contact-family contract independently checks preservation of all its outputs.
Inputs: M>0; one K(q)=q cot δ(q); the explicit positive-threshold quadratic limits of K and -1/[K(q)+μ], with coefficients -α, r0/2, MC0(μ)/(4π) and MC2(μ)/(4π), separately at every nonpole μ. The normalized contact G(μ,q)=MC(q²,μ)/(4π) is fixed to -1/[K(q)+μ], not independently chosen. The observable limit and nonpole scale derive its eventual nonzero denominator. Also p>0, Λ>0 and |Λr0/2|≤B. At the separate prediction momentum p, the two local PDS equations below remain imported calculations using those same contacts. The threshold neighborhoods need not be uniform in μ.
Deductions: the equation-(11) running values and actual beta derivatives; both reduced amplitudes below at every nonpole scale; the relative correction bound and its strict-smallness condition; exact leading elastic unitarity; the linearized optical theorem; and, for every real t, Im(f0+tf1)-p|f0+tf1|²=-pt²|f1|². Every finite raw leading-loop sum has error Rn+1|f0| with R=|g0||μ+ip|; R≥1 keeps that error at least |f0|. If μ>0, ρ<1 and |α|≤ρμ, the same theorem derives 1/(1+ρ)≤|μg0|≤1/(1-ρ). No running solution, beta equation or full-amplitude scale invariance is separately assumed.
This earlier standalone value contract has six outer hypotheses rather than seven: the free contact function and separate inverse-amplitude premise have been eliminated. A kernel-checked coefficient/germ equivalence and the former complete contract preserve every output of that presentation. Its signature deliberately changed at that consolidation; the established observable-to-amplitude export still follows with its exact original signature. No new physical definition or premise was added by that consolidation. It removes a duplicate function choice, not a physical matching obligation; it is not a count of independent semantic choices or a human approval. Higher-contact counting, nuclear applicability and omitted-term control remain separate, explicitly unreviewed obligations. The earlier fixed-μ=p argument remains supporting material, not the whole review target.
Why infinitely many C0 bubbles, but only one C2 insertion?
The source's first two terms now have one defining equation. With L=μ+ip, V(X)=g0+hX+X²Vhigher(X), h=g1p², and F(X)=f0+f1X+X²Fhigher(X), require the coefficients of X0 and X1 in F+VLF+V to vanish. X is formal derivative grade, not a loop counter or a numerical momentum.
[X1]: f1+g0Lf1=-h(1+Lf0).
What Lean connects: graded_chain_is_actual_amplitude_monomial proves that the graded product of a chain's actual vertices and PDS loops is its existing numerical amplitude times XS, where S is the sum of derivative indices. Arbitrarily many C0 vertices leave S=0. S=1 is exactly one C2 vertex with arbitrary C0 dressing. Every chain with S≥2 has zero coefficient at both retained grades, even if its numerical amplitude is nonzero. The earlier matching and naturalness bounds supply the conservative (p/Λ)S estimate; the grading identity alone supplies no physical scaling law.
Exact consolidation: EquationThirteenAt is now this single residual through grade one. A kernel-checked equivalence retains the complete former two-equation specification, including M>0 and p≥0. A second equivalence permits arbitrary higher interaction and amplitude tails. The two closed source amplitudes, nonpole domain, optical relations and connected source-route deductions are preserved. The literal definition and independent preservation check and chain/graded-equation contracts expose the mathematical content.
Still not established: formal coefficient independence is not convergence at X=1 or an error estimate for the physical amplitude. Bounds for a supplied finite matching jet do not validate unsupplied higher contacts. The larger treatment-label route still has its assigned-exponent interpretation boundary. This consolidates one physical relation; it does not establish a manageable whole-library review scope or human approval.
In particular, at subtraction scale μ=p, matching to inverse scattering length α and effective-range coefficient k1=r0/2 gives the reduced amplitudes
|SL-f0| = (√2 |pg0|)L+1|f0|,
|f1| ≤ (Bp/Λ)|f0|. SL sums the actual leading-contact chains through L loops. If |α|≤ρp and 1+ρ≤√2, every such raw sum has error at least |f0|. Yet Bp<Λ makes the resummed first correction strictly smaller than |f0|.
Why this matters: a loop expansion and an expansion in derivative insertions are not the same approximation. The result checks an actual finite-sum error, not merely that an omitted graph is nonzero. The extra ρ condition is our sufficient bound for the PDS sum at μ=p, not a numerical claim made by KSW. Raw loop convergence depends on the subtraction scheme, even when the resummed observable is the same.
From matched amplitudes to shared treatment semantics
ContactChains.matching_and_local_equations_control_the_pionless_expansion remains the numerical proof core for the complete finite-jet argument at μ=p. Its exact premises, every chain bound, finite-loop error, sector-selection result, amplitude, correction bound and quadratic residual are unchanged. Its proof does not depend on the shared treatment context. The combined export matching_derives_first_order_treatment_and_amplitudes is a corollary constructing that context instead of requesting freely supplied treatment predicates or an interpretation certificate.
Six explicit fields: N is the last supplied coefficient index, and required chains use only indices n≤N. The allowed vertex grade is n-1, scoped through order zero and n≤N; order comparison is the integer order; retention means membership in a nonempty supplied chain with total derivative grade at most one; resummation means unbounded required occurrences; perturbativity means a uniform finite insertion bound within this jet; suppression compares C2 with C0 only when N≥1 and the actual calculated dressed correction is smaller than the resummed leading amplitude. The literal definition contract exposes all six fields.
resummed ⇔ n=0; perturbative ⇔ n≠0 and n≤N;
nonvacuously sound ⇔ N≥1 and |f1|<|f0|.
Exact API readback: for N≥1, first_order_treatment_contract_iff_numerical_suppression proves that the complete five-clause output is equivalent to Bp<Λ ⇒ |f1|<|f0|. The resummed leading sector, failure of uniform perturbativity, separated treatments and retained-label characterization add no numerical condition once this context is fixed. That does not validate its six field meanings. This is an interface check, not a replacement for the complete physical argument above.
The matched negative-scattering-length example obtains the complete numerical and API results while every finite raw leading sum has order-one error. With N=1, its unsupplied C4 is arbitrary and its tree amplitude can be arbitrarily large. The result therefore cannot certify unsupplied interactions. Separate diagnostics reject soundness for an oversized correction and for a jet containing only C0, even if the correction is zero. Zero C2 is still allowed when supplied: contribution labels describe allowed interactions, not guaranteed nonzero coefficients.
Limits: the derivative grade has the actual-chain identity and finite matching bounds above as its conservative interpretation. This does not derive exact nonzero asymptotic orders or validate the larger generic treatment adapter. Restricting the previously unscoped context to the supplied jet is a semantic correction, not an equivalence to its former classification of every positive index. A false predicate outside this scope is not a physical verdict about that interaction. Higher-coefficient naturalness remains a separate source assumption. This is one derived six-field context requiring semantic inspection, not human approval, a physical remainder bound or an established independent-definition count.
A complete realization: resummation at infinite scattering length
Canonical coefficient calibration: given [K(q)+α]/q²→k1 and α-μ≠0, the new exact equivalence canonical_contact_coefficients_iff_values says that the quadratic coefficient limit for -1/[K(q)+μ] is precisely g0=1/(α-μ) and g1=k1/(α-μ)². The literal Lean characterization exposes both limits and algebraic values. Thus this part of the complete contract identifies the supplied contact coefficients; it is not a new regularity assumption beyond the observable ERE. It still commits to the source's inverse-amplitude relation and normalization. No analyticity, common threshold neighborhood or physical remainder estimate follows.
The independent unitary-limit realization consumes the complete first-order contract, rather than just its correction bound. In chosen units M=4π, α=0 (infinite scattering length), r0=1 and Λ=2, use K(q)=q²/2, C0(μ)=-1/μ and C2(μ)=1/(2μ²). The characterization derives the canonical contact-coefficient limit, and the two local interaction equations are checked for the actual amplitudes at μ=p.
|SN-f0|=(√2)N+1/p.
Im(f0+tf1)-p|f0+tf1|²=-pt²/4.
For every 0<p<1 the derivative correction is strictly smaller, yet every finite raw leading-loop sum misses by at least the leading amplitude's own magnitude. The same contract supplies the actual beta derivatives at every μ≠0, exact leading elastic unitarity and the linearized optical relation. This tests the connected distinction between a failed raw loop expansion and a small resummed derivative correction.
Limits: this is an algebraic EFT realization, not measured nuclear data or a finite-range potential construction. The interval and units are ours. A second checked boundary permits zero effective range and therefore a zero C2; conservative upper orders cannot force a nonzero derivative coefficient. The generic higher-contact treatment interpretation, physical applicability and unknown omitted terms remain unreviewed. No production physical definition or field was added; no independent-semantic-count reduction or human approval is claimed.
Assessment: what this establishes, and where the paper route still falls short
Interaction grades are not graph membership: the contribution clause now reads couplingOrder n + 2*n = q for the vertex C2np2n. Previously it included every grade of a chain containing that vertex, giving C0 both grades -1 and 0 when it dressed a C2 insertion. Applying the shared strict-order soundness law then forced C0 to be suppressed relative to itself. That law was not previously asserted, so this exposes an interface-role mismatch, not a contradiction in the value argument. Chain-based retention and uniform insertion bounds are unchanged. The independent Lean diagnostic proves this obstruction and realizes all eight original treatment outputs in a corrected three-label model with nonvacuous order soundness, irreflexive suppression, and no spurious grade-zero C0 contribution. This is a correction, not an equivalence to the old predicate. The model's comparison is nominal, not a numerical suppression estimate or a nuclear realization. Physical exponent assignments and higher-term control remain separate inputs; human review remains pending.
Physical inputs, not derived here: K=q cot δ, f=MA/(4π) and G=MC/(4π) identify the observable and normalization. The original nonrelativistic singlet channel and momentum much smaller than the pion mass justify the pionless model; real/complex variables and p≤Λ do not establish those conditions. The PDS bubble calculation and zero/one-insertion equations are explicitly imported. The effective-range size is a separate naturalness input, not a consequence of large scattering length.
Checked deductions: observable matching fixes the two contact-coefficient equations; the imported interaction equations then determine the two amplitudes. Finite loop errors and the relative insertion bound are derived. This is a useful conditional argument, but neither a derivation of nuclear applicability nor a bound on the unknown full remainder.
Remaining interpretation boundary: the paper-level large_scattering_length_requires_resummed_leading_contact uses explicit equalities for the selected loop and indexed contact exponents, plus an imported InterpretsContactCountingAt. The former freely assignable scaling predicates are removed; the treatment interpretation and bubble requirement now use the same exponent data. This repairs their disconnection, but does not derive the physical scaling assignment. The two-route composition below connects the actual amplitude output to the RG route's actual coefficients and quantitative bounds. An upper bound alone cannot establish a nonzero leading scaling order.
Removed higher-order commitment: contribution and retention labels are now interpreted only through order p0, the scope of this source conclusion. Previously they were constrained at every integer order, which forced a distinct library label for every derivative contact. The checked diagnostic proves that hidden injectivity requirement and realizes the unchanged mixed-treatment conclusion with three labels: C0, C2, and excluded higher contacts. Every actual derivative index, chain, and coupling remains distinct in the calculation; all higher contacts are still excluded through this order. The new interface does not promise to interpret higher-order contributions. This removes an unnecessary assumption, not a physical naturalness premise, and is not an equivalence to the stronger old interface.
This source/code assessment is automated, not a human semantic approval. The graph below supports inspection; its size and successful compilation do not settle these interpretation choices.
Actual chain bounds need comparable scales, not the special choice μ=p
The source chooses μ of order p. The new comparable_matching_window_controls_actual_chains fixes one finite effective-range jet, Λ, ρ, its naturalness bound B and c≥1 before both μ and p. For 0<μ≤Λ, |α|≤ρμ, ρ<1, p>0 and p≤cμ, μ≤cp, every nonempty chain from the retained contacts satisfies
L counts contacts and S is their total derivative index. The bound has a factor (p/Λ)S, but adding C0 bubbles does not increase S. This does not assert a ratio between the actual values of two chains. Every finite loop cutoff misses a nonzero leading chain with lower bound [1/(c(1+ρ))]N+2 on p|F|, where N is the cutoff. No assigned loop or coupling exponent is assumed. The exact rescaling keeps μ/p; all earlier sharper μ=p identities and bounds remain intact.
The literal Lean contract and diagnostics use finite a=-100, nonzero r0=1, μ=1/20, p=1/10, Λ=1 and c=2 in chosen units. A separate diagnostic keeps matching and the large-length window but violates μ≤cp; the proposed leading lower bound then fails. These are algebraic model tests, not nuclear measurements or potential realizations.
Boundary: these constants are our sufficient estimates, not KSW error bars. They may grow with chain length. No infinite-sum bound, nonzero derivative order, physical remainder estimate or nuclear applicability follows. A nonempty coefficient window need not reach p much smaller than Λ, and fixed finite a does not permit the enhanced window to extend to p=0. This gives a numerical finite-window interpretation of conservative counting, not validation of the broader route's imported order interpretation or a human approval. No new physical definition was added.
The same physical amplitudes now connect the two source routes
certified_routes_control_the_same_pionless_amplitudes consumes the existing pionless-RG and mixed-interaction certificates for the same channel. The former supplies its derived C0(μ) and C2(μ); the latter supplies its two source amplitudes. No second set of amplitudes or coefficient matches is assumed. The same-channel equality is explicit. The selected scales and momenta of the two routes need not be equal: the running family supplies every nonpole scale.
Write g0=MC0(μ)/(4π), α=1/a and k1=r0/2. The additional inputs are p>0, μ>0, Λ>0, |α|≤ρμ, ρ<1 and |Λk1|≤B. Nonpole status follows; μ need not equal p. Lean derives 1/(1+ρ)≤|μg0|≤1/(1-ρ), f0=(-α-ip)-1, f1=-k1p²f0², and |f1|≤(Bp/Λ)|f0|. The correction is strictly smaller when Bp<Λ.
For every finite leading-loop sum Sn=-∑j=0ng0[-g0(μ+ip)]j, its exact error is Rn+1|f0|, with R=|g0| |μ+ip|. Only when R≥1 does the theorem conclude that every finite error is at least |f0|. Neither this ratio test nor the range bound is replaced by an assigned order label. A bound on μg0 becomes a uniform p-scaling bound only with a quantitative relation between μ and p.
A standalone specification for this complete quantitative deduction: PionlessRGFlow.matched_running_values_control_resummation_and_first_correction uses only M, α, r0, C0(μ) and C2(μ) from the existing running model, together with the selected real scales, two complex amplitudes and all the equations and inequalities just stated. Equation (11) is an explicit premise here, derived by the earlier observable-family argument. The source-level theorem now extracts the same running values and interaction equations from its two certificates and calls this core. Its signature and every conclusion are unchanged; no new physical predicate, model or assumption has been introduced. The larger certificate scope is still displayed and unreviewed.
The independent complete core contract also checks an inhabited example with M=4π, α=0, r0=2, μ=2 and p=1/10 in chosen units. Its reduced amplitudes are f0=10i and f1=1: the correction has 10% of the leading magnitude, while every finite raw leading-loop sum has error at least |f0|. This tests the actual inference away from μ=p; it is a model diagnostic, not measured nuclear data or a bound on omitted physical terms.
The exact Lean contract retains every premise and conclusion, plus a readout-level diagnostic showing that two unitary real-contact amplitudes need not represent the same channel. The review graph exposes this larger composition separately from the compact core. It inherits both certificate scopes, including their source interpretation choices. It does not prove a nuclear remainder estimate, the pionless regime or the correctness of the order-label interpretation. Human semantic review remains pending.
The first-order argument does not need a higher matching jet
The supporting fixed-scale statement is observable_matching_separates_loop_and_derivative_expansions. Its entire physical specification is below. K and G are real functions; g0, g1, k1, p, Λ, α, ρ and B are real; f0 and f1 are complex. Use K(q)=q cot δ(q), G(q)=MC(q²,μ)/(4π), g0=MC0/(4π), g1=MC2/(4π), k1=r0/2 and f=MA/(4π) with M>0. The subtraction scale is fixed at μ=p while q tends to zero.
- Domain: 0<p≤Λ, |α|≤ρp and ρ<1. Here Λ is a short-distance momentum scale, not a regulator. α=0 is allowed; for finite nonzero scattering length a, α=1/a.
- Matching: as q→0 from above, require [K(q)+α]/q²→k1 and [G(q)-g0]/q²→g1. These imply K(q)→-α and G(q)→g0; the constant limits are not separate premises. Require [K(q)+p]G(q)=-1 for all sufficiently small positive q. No coefficient of q4 or higher is specified.
- Effective-range size: |Λk1|≤B. This is a separate physical input, not a consequence of a large scattering length.
- Interaction calculation: write L=p+ip and h=g1p². Require f0+g0Lf0=-g0 and f1+g0Lf1=-h(1+Lf0). These are the zero/one-insertion PDS equations; no hLf1 term occurs in the second equation.
Every conclusion: the two amplitude formulas, finite-sum error and relative bound displayed above, with Sn=-∑ℓ=0ng0(-g0L)ℓ; the error is at least |f0| when 1+ρ≤√2; and the correction is strictly smaller than |f0| when Bp<Λ. Finally, for every real t, V=g0+th and F=f0+tf1 satisfy F+VLF+V=t²hLf1. This is an exact insertion-order residual, not exact scattering at t=1.
The preceding MS failure is now part of this same theorem: for every real gMS satisfying αgMS=1, put SnMS=-∑ℓ=0ngMS(-igMSp)ℓ. At every finite n, |SnMS-f0|=(p/|α|)n+1|f0|>|f0| on the stated window. The comparison uses the same observable f0 and adds no premise to the theorem. At α=0 no finite gMS satisfies matching; the PDS conclusions still apply. This is not a claim that the unitary limit has gMS=0.
The supporting theorem minimal_subtraction_matching_fixes_loop_series_radius checks actual finite contact-chain sums and proves their error tends to zero exactly when p<|α|. For finite nonzero a this is p<1/|a|. At equality the error never shrinks. This leading-series radius is not a sufficient condition for the whole EFT expansion to be accurate, nor a replacement of the paper's parametric “much smaller” regime by a sharp full-validity threshold. At α=-3/4 and p=1, checked examples give MS ratio 4/3 and PDS ratio 4√2/7<1 for the same f0: the scheme changes loop convergence, not that observable.
A checked failure of sufficiency: in fixed numerical units take K(q)=-1+16q4 and f(q)=1/[K(q)-iq]. The threshold coefficients are -1 and zero, and the amplitude is elastic-unitary at every positive q. At p=1/2 the leading MS series converges, yet |f(p)-f0|=2|f0|>0: a 200% error relative to the leading amplitude. This is a diagnostic, not a nuclear model or a counterexample with controlled higher shape coefficients. The theorem ms_leading_convergence_does_not_control_an_uncontrolled_shape_term exposes why those additional bounds matter.
The independent Lean contract spells out the two supplied limits and the full conclusion without project-defined predicates. It also checks first_two_coefficients_iff_quadratic_limit, the exact equivalence deriving each formerly separate constant limit. This removes two redundant clauses, not any physical matching, naturalness or interaction obligation. Values at q=0, analyticity and a quartic remainder bound are not assumed. The broader theorem below derives its retained first-order conclusions through this theorem, while retaining its separate higher-chain bound and diagram-selection statement. All eight original outputs remain checked. This removes higher-jet assumptions from the first-order claim, not from higher-order physics. The MS comparison adds no new physical definition. The paper adapter also replaces its independent MS flag with its existing numerical scale being zero. Neither theorem bounds the unknown physical remainder or establishes nuclear applicability. Human semantic review is pending.
Supplement: finite higher contact chains, all original inputs and eight outputs
g,k : ℕ→ℝ; K,G : ℝ→ℝ; N : ℕ; p,Λ,α,ρ,B : ℝ; f0,f1 : ℂ. The physical interpretation is K(q)=q cot δ(q), G(q)=MC(q²,μ)/(4π), gn=MC2n/(4π) and f=MA/(4π), with positive nucleon mass M. The prediction momentum p fixes μ=p; q is the separate threshold-limit variable. Λ is a short-distance momentum scale, not a loop regulator. α is the inverse-length datum: for finite nonzero a, α=1/a; α=0 is permitted by this core, not an encoding of a=0.
- Retained domain: N≥1, 0<p≤Λ, |α|≤ρp, ρ<1. Positivity of Λ and nonnegativity of ρ follow.
- Observable matching and the retained higher jet: as q→0 from above, K(q)→-α, [K(q)+α]/q²→k1, G(q)→g0, and [G(q)-g0]/q²→g1. Require [K(q)+p]G(q)=-1 on a sufficiently small positive neighborhood, with p held fixed. Lean derives (α-p)g0=1 and (α-p)g1=k1g0. For higher coefficients only, let Γ(z)=∑n≥0gnzn and H(z)=(α-p)-z∑j≥0kj+1zj; additionally require [zn](ΓH)=[zn]1 for 2≤n≤N. Together these imply the full retained recurrence. At N=1 there is no higher-jet premise to supply. For N>1, the higher formal coefficients are independent inputs, not consequences of two limits or a claim of convergent evaluation. Coefficients beyond N are unconstrained; k0 is unused.
- Naturalness input: |Λ2j-1kj|≤B for every 1≤j≤N. B≥0 follows. This is not derived from large scattering length.
- Local interaction equations: with L=p+ip and h=g1p2, f0+g0Lf0=-g0 and f1+g0Lf1=-h(1+Lf0). These specify zero and one derivative insertion; they do not claim convergence of a graph series.
All project-defined ingredients in the statement: the shared approach is the positive neighborhood filter at zero; HasFirstTwoCoefficients supplies the quadratic limit displayed above, used once for K and once for G. Each constant limit is derived, and a checked equivalence preserves the former pair for every real function without a condition on its value at zero. The remaining ingredient is the amplitude of a nonempty ordered list v of contact indices, with m entries and d=∑v:
SL = ∑ℓ=0LA([0 repeated ℓ+1 times]).
The product counts repeated entries. Empty lists are excluded. This formula retains the tree sign, derivative powers, and PDS bubble factor; one declaration is not one independent physical assumption.
- For every such v using indices ≤N, p|A(v)|≤(√2)m-1(1-ρ)-m{[1+B/(1-ρ)]p/Λ}d. The constant depends on m; it does not bound an infinite sum.
- For every L≥0, the exact error above holds; if 1+ρ≤√2, it is at least |f0|.
- For every nonempty v, d≤1 exactly when v contains only zeros, or one 1 with zeros on either side. Identifying these with retained orders uses the stated contact-chain interpretation.
- f0=1/(-α-ip).
- f1=-k1p2f02.
- |f1|≤(Bp/Λ)|f0|.
- Bp<Λ implies |f1|<|f0|.
- For every real t, putting V=g0+th and F=f0+tf1 gives F+VLF+V=t2hLf1. Thus the constant and linear residuals vanish, not the full residual at t=1. t counts insertions, not momentum.
These are a mathematical reading of matching_and_local_equations_control_the_pionless_expansion, not a replacement formalization. Its exact full type is checked by the Lean contract. Inspect the exact statement and complete dependencies; the larger paper certificate has a separate, larger unreviewed scope.
One mass, one momentum family, one subtraction-scale family
The source uses the same M, p and μ in its vertices, loop and bubble amplitude. The formula readout is now constructed from the framework's existing mass, momentum family and subtraction-scale family, rather than storing second copies and requiring equality. Its total center-of-mass kinetic energy is now derived as E(p)=p²/M in the selected leading nonrelativistic model. The contact polynomial, evaluated loop and amplitude families remain explicit inputs. The interpretation boundary has only the two external obligations for energy and contact interaction. The complete Lean contract check exposes all seven constructed fields, recovers the former five-clause boundary exactly, and retains M>0 in the imported loop formula while deriving M E(p)=p² for the constructed readout.
For nonzero selected M and the three retained data families unchanged, an arbitrary old readout equals the generated one iff its mass, scale and momentum selections agree and its old on-shell equation holds. The equation uniquely fixes the entire energy family. Zero-mass, single-nucleon-energy and relativistic-dispersion controls test the limits of this equivalence. This preserves every proposition about that readout, not just its zero-power loop or one amplitude. The complete source-route contract retains every loop, bubble, normalization and matching output. Mismatched old records are not claimed equivalent, and the physical interpretations and imported calculations are not discharged.
The earlier kinematic consolidation changed the constructor from 78 to 81 fields; computing the remainder reduced this to 80 and deriving the on-shell energy reduced it to 79 (subsequent pion-inclusive beta consolidation left 75, and deriving omitted coefficients leaves 74): one nested seven-field record was replaced by its four nonduplicated data families. Thus three duplicate data choices and equality obligations were removed even though the raw top-level count increased. These are constructor counts, not counts of independent physical assumptions. Numerical equality does not prove that a parameter is a physical nucleon mass. Nonrelativistic applicability, the remaining interpretations and omitted physical terms still require scrutiny; human semantic approval remains absent.
No second, unused C2 term label
The former derivativeContact record field was read by no active KSW declaration. The actual C2 coupling, its running values, indexed contact chains and firstCorrection treatment label remain. No equality between two term labels is added. The Lean diagnostic restores an arbitrary extra label without a new inhabitation assumption and checks that changing this discarded payload cannot change any predicate of the retained record. This is a specification reduction, not a physics theorem or approval of the remaining fields. All named source routes remain subject to the same physical obligations.
The loop used downstream is the concrete source loop
The abstract loop type, its two separately supplied values and its unrestricted representation predicate have been removed. The existing pdsLoopIntegralObtained now means I0=-(M/(4π))(μ+ip) for the same complex-valued loop family, with the selected M, μ and p. PDSLoopCalculation supplies only the all-power source formula. The existing pds_subtraction_yields_loop_integral derives its zero-power instance; the complete bubble and observable-matching route still consumes that result.
The Lean contract proves the separate zero-power output redundant under this concrete meaning. The checked equivalence to a former abstract equality assumes faithful numerical readback of both sides under an injective encoding; these are sufficient conditions, not claimed necessary ones. Unequal abstract labels need not spoil a correct loop, and equal labels do not repair a wrong one. These controls concern the duplicate interface; the old complete route already required the numerical formula too. No production definition or theorem was added. Loop integration and regularization remain imported calculations; this is not a proof of nuclear applicability or omitted-term control. Human semantic review remains pending.
One observable family determines both amplitude terms
The source-level theorem observable_matching_controls_the_first_two_pionless_amplitudes replaces a helper that asked for two scalar coefficient matches separately. From the same positive-threshold observable/contact limits used by the RG route, it derives equation (11) and those matches. The two retained source graph equations then give f0=(-1/a-ip)-1 and f1=-(r0/2)p²f0². Both terms are therefore identical at any two nonpole subtraction scales where the graph equations hold. No full-amplitude scale-independence premise is used.
Given p>0, Λ>0 and |Λr0/2|≤B, it also derives |f1|≤(Bp/Λ)|f0|. The graph calculation and naturalness remain inputs; the theorem permits zero or negative effective range. Its exact Lean contract checks all four outputs. This is a deduction from the original formulas, not a proof of omitted-term control or a license to resum C2 exactly. The adapter still exposes the larger unreviewed framework context; the compact argument above remains the starting point for review. Human approval remains pending.
The resummation model uses the same complex amplitude
The full-contact pionless target is now computed as A=-C/[1+MC(μ+ip)/(4π)], with a nonzero denominator. It is neither the C0-only leading term nor the later pion-inclusive amplitude. The existing bubble theorem derives this equality from the imported iA formula; it is no longer independently supplied. The shared technical model selects this same complex amplitude for its resummation and unitarity conclusions. Changing the unrelated pion-inclusive amplitude values cannot change this pionless result.
Full pionless scale independence means A(μ,p)=A(μ',p) for the actual readout. It remains an imported obligation in the full RG route, not a consequence of knowing just two threshold coefficients. The first two terms have their own derived scale-independence result above. The later pion-inclusive cancellation is a separate proposition. The Lean contracts check the concrete quotient and redundancy of its second supplier; they do not equate arbitrary former abstract labels with physical amplitudes. The source graph retains an already-derived amplitude as a provenance predecessor, not an additional minimal physical assumption.
The contact family is fixed by the observable
The paper adapter now uses Gμ(q)=-1/[K(q)+μ] directly. It no longer asks for a second function and then constrains it back to this one. The contact-only inputs are positive mass, the two coefficient limits of this explicit function, a physical momentum sample, and equality to the actual normalized contact readout. The source equations (6), (8) and (9) supply the physical interpretation.
pionless_observable_matching_iff_contact_family proves equivalence to the complete former contract under the separate observable-matching premise, and both the RG and source-amplitude deductions use it. Eliminated: one existential function of scale and momentum. Now derived instead of duplicated: nonzero scattering length and a nonzero contact denominator near threshold. The first already belongs to observable matching; the second follows from its constant limit at each fixed nonpole scale. Retained: coefficient calibration, the same momentum sample, readout identification, pole exclusions and all other physical inputs. This is not one fewer independent physical assumption.
The premise matters: without observable matching, the reduced contact-only contract is weaker. A checked K=0, declared a=1 example satisfies it using totalized division, but fails the observable match and denominator exclusion at μ=0. It is not a complete physical model. The exact former canonical contract recovers both removed clauses under observable matching; no new production definition or field was added.
The equality holds only near q=0 from above at each fixed scale. It is not equality at zero, at an arbitrary prediction momentum, or on a common neighborhood for all scales. A checked numerical diagnostic changes the contact at zero and at q=2 while preserving threshold matching. The literal reduced contract and equivalence and result checks retain these boundaries. No human semantic approval is inferred.
Each channel selects its own running contacts
The source distinguishes singlet and triplet scattering lengths and separate fits in Fig. 3. The adapter formerly read C0 and C2 from a channel-independent family while assigning channel-dependent a and r0. Equation (11), at a common nonpole scale and mass, then forces those low-energy parameters to agree. That was an unintended restriction on the represented systems.
The existing coupling field now takes the channel explicitly. Its real flow, observable coefficient contract and first-correction amplitude readout all use the same selected channel. No production field or declaration was added. The Lean diagnostic proves the former identification and realizes two channels at M=4π, μ=2: α=-1,1 and r0=2,4 give C0=-1/3,-1 and C2=1/9,2. Both satisfy equation (11). These values test the representation; they are not nuclear fits. Wrong-channel mutations are rejected. The correction permits independent channel data while retaining each single-channel deduction; it does not establish the coupled matrix calculation or human semantic approval.
Observable matching without the full paper adapter
PionlessRGFlow.observable_family_controls_running_and_resummed_terms gives the observable-to-running-to-amplitude deduction using the existing five-field flow: M, α, r0, C0(μ) and C2(μ). There is no nuclear-framework, pion, coupled-channel or fit parameter in this theorem. Its complete physical input is:
- M>0 and real inverse scattering length α, including α=0; a positive prediction momentum p and positive short-distance scale Λ; |Λr0/2|≤B.
- A single real phase function K(q), independent of μ, whose positive-threshold coefficients are -α and r0/2. Here K(q)=q cot δ(q) is the physical interpretation, not a theorem about measured data.
- For each real μ≠α, a contact function G(μ,q) with threshold coefficients g0=MC0(μ)/(4π) and g2=MC2(μ)/(4π), satisfying [K(q)+μ]G(μ,q)=-1 near q=0 from above.
- At any selected nonpole scale, the literal two local equations for f0 and f1: with L=μ+ip and h=g2p², f0+g0Lf0=-g0 and f1+g0Lf1=-h(1+Lf0). These are reduced amplitudes f=MA/(4π); q is not p.
Lean derives C0=(4π/M)/(α-μ), C2=(2πr0/M)/(α-μ)², their ordinary derivatives C'0=MC0²/(4π) and C'2=MC0C2/(2π), and f0=(-α-ip)-1, f1=-(r0/2)p²f0² with the relative bound above. The same formulas apply at every nonpole scale satisfying the local equations. The original paper-level theorem delegates to this core with α=1/a and still explicitly requires finite nonzero a; it retains all four of its original outputs.
The complete compiled project meaning scope is 19 declarations, including selectors, constructors and generated proof terms; the larger adapter has its own separately exposed scope. These are not counts of independent physical assumptions. The exact Lean contracts check both the core and the unchanged adapter statement. The review page exposes both scopes; neither is marked reviewed. No physical interpretation, nuclear applicability, higher-order remainder or full-amplitude invariance has been proved by extracting the core.
Unitary-limit boundary: α=0 is admitted by this core and by the contact-chain argument. It denotes infinite scattering length, not a=0. Then μ=0 is the excluded contact pole: neither a value nor a derivative there is inferred from the off-pole formulas. The zero-scale boundary-data theorem requires α≠0. A single nonzero-effective-range observable family now tests both finite inverse length and α=0. This is an explicit extension of the finite-a parametrization of the source formulas, not a new claim about their nuclear applicability.
What the source comparison establishes
Original author TeX: the opening pionless setup and labels 1, 6, 8, 9, 11, 14. Label 14 is printed equation (13). The following assessment is mine; the equalities, domains, and retained-order restrictions are inspectable above.
- Faithful within the model: the normalization, tree sign, PDS factor, effective-range matching sign, and two dressed terms agree with the original formulas. The local equations are our equivalent reconstruction, not another equation quoted from KSW. Their equivalence derives a nonzero denominator but does not remove the interaction-model assumption.
- Physical applicability remains external: KSW starts with the nonrelativistic singlet S wave at momentum much smaller than the pion mass. The core theorem has no nucleon fields, pion mass, potential, or relation to a measured phase shift. Its real/complex variables and p≤Λ do not by themselves establish that regime or the applicability of the PDS reduction. Adding a validity flag would not resolve this.
- Accuracy remains limited: the observable/contact limits and identity derive two matching equations; higher-jet matching and naturalness remain inputs. None follows from the scattering length alone. A small f1 establishes neither a bound on the physical remainder nor convergence or all-order EFT control. The estimate is at one prediction momentum; a separate fixed-window theorem fixes coefficients and constants across scales.
Checked diagnostic: in the contract, p=μ=1, α=-1/4, Λ=2, k1=1/16 and B=1/8 give g0=-4/5, g1=1/25. Every leading-loop cutoff has error at least |f0|, but the nonzero correction is bounded by |f0|/16. A second matched example with α=-3/4 has raw error below |f0|: ρ<1 alone is insufficient. These are algebraic diagnostics, not nuclear fits or finite-range-potential constructions.
Review burden and remaining boundary: the first-order argument requires the complete first-order specification and its physical interpretation, not approval of every proof lemma or the higher-jet supplement. The latter is still necessary when assessing the broader chain bounds. Existing checked equivalences remove duplicate presentations; redundant positivity and nonpole premises have been derived. Actual observable/contact limits discharge the first two coefficient equations using the same coefficient semantics as the RG argument. This does not remove laws of physics or certify the source interpretation. The approach, limits, interaction model and nuclear applicability still require scrutiny; there is not yet evidence that the library-wide review burden is manageable. Human review remains pending.
Four independent roots feed three distinct continuations
The source map does not present one undifferentiated proof. Pionless PDS, the minimal-subtraction scope contrast, large-length power counting, and the coupled-channel calculation begin independently. Only the explicit-pion, scale-cancellation, and singlet-fit routes form a dependency chain.
| Ingredient | Status | What Lean permits the reader to conclude |
|---|---|---|
| PDS loop, resummation, RG, power counting, pion graphs, cancellation, fits, and coupled calculation | deferred calculations | Their exact proposition-valued outputs may be used downstream; their internal mathematics is not proved locally. |
| Large-length, minimal-subtraction, pion-scale, and coupled regimes | controlled approximations | Every result remains scoped to its declared low-energy regime and order. |
| Effective-range matching and phase-shift fit inputs | imported results | The low-momentum p cot δ family is retained explicitly; the imported fit remains a separate hypothesis. |
| Validity suggested by fitted coupling sizes | author expectation + interpretation | It is channel-scoped support, not a theorem that omitted corrections are controlled. |
| Analytic subleading coupled formula | open obligation | The displayed observables may be used at their declared orders, but a complete subleading matrix formula is absent. |
PDS turns the large scattering length into an all-orders pionless amplitude
Select low pionless momentum, a channel with large scattering length, a PDS subtraction scale, and the required bubble chain. Three supplied calculations act in sequence: subtraction gives the loop value, the loop feeds the bubble sum, and comparison with the S-matrix form establishes S-wave unitarity.
iA = -iC(p2,μ) / [1 + MC(p2,μ)(μ + ip)/(4π)],
then PDS loop → all-orders bubble amplitude → unitary S-wave form. literal printed equations (4) and (5), with M > 0, ME = p², the n = 0 loop bridge used by the bubble chain, and a nonzero bubble denominator; the elastic-channel and phase-readout identification remain explicit (1)
The scalar S-matrix is the actual complex quantity S = 1 + i p M A/(2π). For a real elastic contact, equation_six_with_real_contact_proves_elastic_unitarity derives its unit norm from the bubble quotient. The observable-normalization stage consumes the already retained bubble formula and imports K = ip + 1/f for the physical phase function K = p cot δ, where f = M A/(4π), away from a zero contact. It no longer supplies the bubble formula again or directly assumes K = -1/g - μ. Lean derives that contact relation for g = MC/(4π). A complex contact can obey the same bubble formula while violating elastic unitarity; complex_contact_bubble_formula_does_not_supply_elastic_unitarity checks that distinction. The public source-route certificate exposes the actual unit-norm equation and depends on the upstream formula.
The effective-range premise now requires actual threshold coefficients throughout the selected physical domain and a realized positive-momentum approach. The residual is derived from that observable, not separately chosen. This corrects the former pointwise identity, which could not identify a or r0. The RG contract supplies contact coefficient limits and the inverse-amplitude identity on an admissible sampling family; the threshold premise gives R(p)/p² → 0 on that same family. Pionless coupling samples directly evaluate the existing real functions. The three earlier parallel abstract derivative, beta and solution fields and their three wrapper predicates remain removed. The source route derives the real beta equations and solutions; full-amplitude scale independence remains a separate imported output. Nonconstant running is separate: C2 can vanish identically when r0 = 0.
From the observable to running contacts: the complete coefficient argument
Take M > 0, finite a ≠ 0, K(p) = p cot δ, and Gμ(p) = MC(p²,μ)/(4π). Every limit below is p → 0 from above, with μ held fixed and μ ≠ 1/a. K is the same function for every μ.
Gμ(p) → g0(μ), [Gμ(p)-g0(μ)]/p² → g1(μ),
[K(p)+μ]Gμ(p) = -1 on a sufficiently small positive neighborhood,
g0 = MC0/(4π), g1 = MC2/(4π).
Therefore (1/a-μ)g0 = 1, (1/a-μ)g1 = (r0/2)g0. These determine both equation-(11) functions below. No value at exactly p=0, quartic bound, analyticity, or coefficient beyond g1 is assumed. The existence and physical identification of the coefficient limits remain explicit physics inputs.
observable_family_derives_equation_eleven proves this inference; observable_matching_derives_running_values connects the actual paper observables and sampled contacts, and the existing source route now uses it. The complete resummation theorem above also uses this coefficient inference: its first two matching equations are no longer independently supplied. All eight conclusions remain, with higher-jet coefficients still required explicitly from degree two through N. This reconstructs the source's matching logic before differentiating the resulting functions; it is not a proof that scale independence alone determines them. Choosing μ comparable to a prediction momentum comes after coefficient extraction, not inside these limits. A nonzero-range rational contact family realizes the premises, while an unrestricted quadratic remainder can hide an incorrect effective range. The contract repairs a missing restriction and is not equivalent to the old one. Higher jets, naturalness, nuclear applicability, and full-amplitude accuracy remain separate. Human semantic review is pending.
observable_normalization_and_upstream_formula_iff_contact_readout proves exact preservation of the former normalization contract together with its upstream formula supply. The new conditional contract alone is not equivalent. pionless_observable_matching_constrains_the_bubble_contact checks the displayed observable-to-contact relation. This removes one duplicate formula supplier, not a physical assumption. The observable identification, elastic domain, PDS reduction, and larger paper context still require semantic scrutiny; human review remains pending.
for every momentum in the declared low-momentum expansion regime. the remainder stays explicit; agreement at one momentum is not the family (1a)
C0(μ) = (4π/M)/(-μ + 1/a), C2(μ) = (2π/M)(-μ + 1/a)-2r0,
pionless samples directly evaluate these functions, independently of pion-inclusive couplings;
full amplitude(scale) = physical amplitude for every scale.
equationElevenPionlessRunningValuesAt retains M > 0 and a ≠ 0, and applies the finite values whenever -μ + 1/a ≠ 0; exact beta equations, selected solution equalities, and nonconstant running remain distinct propositions
(2)
PionlessRGFlow contains actual real-valued coupling functions. From the now-derived full non-pole equation-(11) family, equation_eleven_derives_actual_beta_derivatives proves the ordinary derivatives C0' = M C02/(4π) and C2' = M C0C2/(2π). actual_beta_derivatives_retain_the_printed_scale_weight then recovers the printed equations above. For nonzero inverse scattering length, the proof also covers μ = 0, where a scale-weighted equality alone loses all information about the derivative. The pole remains excluded. Physical applicability of the observable/contact family, rather than the resulting solution formula, is the imported boundary.
The source beta-function and running-control atoms now use these actual derivatives and real running values directly, without separately supplied abstract-carrier equalities. pionless_rg_exposes_derivative_equations_and_running_solutions retains both printed scale-weighted beta equations and both real solution formulas at every nonpole scale. Three data fields and three proposition wrappers were removed, with no replacement definitions. This corrects the former unrestricted interface; it is not an equivalence to its arbitrary labels, and values at the pole are not asserted. Pionless samples are now direct evaluations of the same functions. An independent six-theorem KSW flow client changes the mass, scattering length, and effective range, obtains nonzero derivative values 2/9 and -4/9, and audits three public API uses without production diagnostic witnesses. This certificate is pionless; the distinct retained pion-inclusive model is described below.
Matching at one scale is not identification of two EFT flows
The source explicitly changes the C0 beta function after including pions. The former adapter used one sampled coupling field for both theories. With a real-valued scale sampler, its two contracts forced equal C0 functions on positive nonpole neighborhoods, incompatible with the different beta equations when the pion correction is nonzero. This obstructed their simultaneous interpretation; it did not invalidate each independent conditional route.
The field is now explicitly pionInclusiveCouplingValueAt. The pionless expansion uses pionlessCouplingValueAt directly. The cross-theory equality premise and its sample-identification theorem are removed, and the equation-(11) predicate uses the existing real-flow solution contract with the paper adapter's finite-nonzero-a condition. No replacement production definition was added. The Lean regression fixture preserves both derivative laws and realizes matching C0=-1/2 at μ=1 with derivatives +1/4 and -1/4 in the two models. The pion-inclusive example is a local jet, not a global solution. The correction reduces duplicate coupling specifications without claiming nuclear applicability or full-remainder control. Human semantic review remains pending.
The checked deductions compose the loop, bubble sum, unitarity comparison, effective-range matching, scale principle, and RG calculation into the declared amplitude and running-coupling outputs. pds_loop_calculation_retains_equation_five_formula and bubble_resummation_retains_equation_six_formula separately project the printed complex formulas, while effective_range_matching_identifies_observable_coefficients derives the actual threshold coefficients from nonvacuous uniform matching and zero_momentum_effective_range_matching_retains_inverse_scattering_length recovers the -1/a intercept when momentum and remainder vanish. pionless_rg_retains_equation_eleven_running_values separately projects the displayed C0(μ) and C2(μ) family from the completed RG route.
pds_bubble_resummation_yields_pionless_amplitude · pionless_pds_route_exposes_equations_five_and_six · pionless_rg_exposes_derivative_equations_and_running_solutions · pionless_rg_retains_equation_eleven_running_values · printed equations (4), (5), and (11)Ordinary minimal subtraction has different domains for natural and large scattering lengths
At zero subtraction scale, the natural and unnatural regimes do not share one validity criterion. For a natural scattering length, small momentum relative to the short-range scale supports ordinary perturbative counting. For a very large scattering length, the product of momentum and scattering length becomes the restrictive parameter.
large |a| at zero subtraction scale: ordinary MS validity requires p ≪ 1/|a|,
therefore the large-|a| MS momentum range is restricted. retained source-level scope contracts; full counting validity is imported, not derived from the leading-loop radius alone (3)
The large-length inverse-length window is a necessary condition, not a sufficient one. The adapter now takes that necessary law over the selected pionless domain and a momentum outside the window, then derives an actual excluded pionless momentum. Restricted range is this existential conclusion, no longer an independent flag. General natural-regime validity and the physical meaning of the domain and window remain imported. This corrects the old equivalence; it does not prove that an arbitrary validity predicate describes nuclear physics. Minimal subtraction is the numerical condition μ=0. The compact argument above separately derives the leading-series radius and the MS failure on the large-length window for the same observable. Convergence of that leading series does not by itself control higher contacts or the physical remainder. The definition contract and result contract check the precise direction and witness.
natural_and_large_scattering_lengths_have_distinct_ms_scopes · arXiv p. 4The KSW expansion is deliberately nonuniform across interaction terms
Now choose a nonzero PDS scale comparable to momentum. In the large-scattering-length regime, supplied loop and coupling scaling place the leading contact in both the leading and subleading truncations, require it to be resummed, and explicitly deny that it is perturbative. The first correction contributes at subleading order and is perturbative.
A−1 = −C0/D, A0 = −C2p²/D²,
Atruncated = A−1 + A0,
C0: retained and resummed to all orders, first correction: retained perturbatively.
EquationThirteenAt uses local leading and single-insertion equations; equation_thirteen_iff_source_terms recovers exactly the two dimensionful source equations with M > 0, p ≥ 0, real contacts, and D ≠ 0. The nonpole condition is now derived. Higher terms and pion contributions remain separate.
(4)
A nonempty list records contact vertices C2np2n; k vertices have k-1 loops. Given coupling order -(n+1) and loop order +1, ContactPowerCounting.momentumOrder adds these exponents and yields total order ∑n-1. Lean derives that every finite loop cutoff misses a leading-order chain and that through order p0 the only chains are all-C0 or one C2 insertion surrounded by C0 vertices. Natural counting instead bounds loop count at each fixed order. These are assigned diagram orders, not a convergence theorem, a nonzero lower bound, or remainder control.
ContactPowerCounting.enhanced_counting_requires_all_leading_bubbles_and_only_one_first_correction · original author TeX between labels 11 and 14 · Inspect the formal statement and its inputsFor finite nonzero a, positive M and μ, and 0 ≤ ρ < 1 with |1/a| ≤ ρμ, the equation-(11) solutions imply that the contact pole is excluded and
1/(1+ρ) ≤ -μ M C0/(4π) ≤ 1/(1-ρ),
|r0|/[2(1+ρ)2] ≤ |μ2 M C2/(4π)| ≤ |r0|/[2(1-ρ)2].
With μ=p these give quantitative enhanced counting on a momentum window, not as p approaches zero at fixed a. The range can be zero or negative. Its natural size, the low-momentum condition, and higher-contact scaling are not consequences of these inequalities. Merely choosing μ=p can hit the pole for positive a; sufficiently small p leaves this window for every finite nonzero a. The exact unitary limit a=infinity is not represented by this finite-real-a model. These bounds are formal consequences derived here, not quoted error estimates from the paper.
PionlessRGFlow.scale_window_derives_first_two_contact_bounds · original author TeX label 11 and following scale discussion · sampled and continuous APIs now share the same two formulas, with sampled_equation_eleven_formulas_unchanged checking the literal old expressionsDerived treatment claims, one exponent assignment. InterpretsContactCountingAt connects the existing API to contact membership, the selected contact/loop exponents, and bounds on occurrences of each contact. One finite insertion bound must work for every retained chain. The source inputs now literally require coupling order -(n+1) for every n and loop order +1 at the selected subtraction scale and momentum. C0 uses index zero of the same family; it has no independent order field. Both the bubble requirement and mixed-treatment deduction use these same data. The former two scaling flags have been removed, and the interpretation no longer hides another fixed enhanced assignment. This is a correction, not equivalence to unrestricted flags.
From these assigned orders, Lean derives unbounded leading C0 occurrences and at most one C2 insertion through order zero. One C2 insertion can still have arbitrarily many dressing loops. diagram_interpretation_derives_mixed_treatments retains all eight mixed-treatment clauses but needs only C0 order -1, C2 order -2, loop order +1, and cn+2n ≥ 1 for n ≥ 2. first_correction_sector_iff_minimal_contact_orders proves these conditions necessary and sufficient for the complete retained chain sector. The original source route preserves its stronger all-order assignment and supplies these weaker inputs. Independent Lean contracts allow higher coupling orders zero while retaining all eight outputs, and reject an order-zero C4 or a promoted C2. This removes unnecessary precision about excluded contacts, not a physics input. Label identifications, the displayed amplitude calculation, and justification of the physical scaling assignment remain inputs; amplitude convergence and the physical remainder are not established.
Write gn=M C2n/(4π) and kj for the coefficient of p2j in p cot(δ), so k1=r0/2. The finite coefficient equations are (1/a-μ)g0=1 and (1/a-μ)gn+1=∑j=0n kn+1-jgj. For 0<μ≤Λ, |1/a|≤ρμ, ρ<1, and |Λ2j-1kj|≤B for 1≤j≤N, Lean derives, for every n≤N,
|Λnμn+1gn| ≤ (1-ρ)-1[1+B/(1-ρ)]n.
The dimensional normalization is checked. Equation (11) is equivalent to the first two matching equations. The higher-coefficient naturalness premise is essential: a finite-a matching family keeps g0, g1, and k1 fixed while |g2| is arbitrarily large. These finite-jet upper bounds permit zero coefficients; they are not a convergence or remainder theorem. The constants and diagnostic are derived here, not source estimates or a finite-range nuclear-potential realization.
ContactMatching.finite_matching_jet_derives_enhanced_contact_bounds · original author TeX labels 6, 8, 9 and discussion after 11The main quantitative theorem now takes [zn]{G(z)[1/a-μ-z∑j≥0kj+1zj]}=[zn]1 for n≤N, with μ fixed during extraction. ContactMatching.finite_inverse_amplitude_jet_iff_matching proves that this is exactly the finite recurrence above, including N=0, and the main proof uses that implication. Formal power series provide coefficient bookkeeping, not evaluated functions or convergence. A diagnostic has G=-2+2z and H=-1/2-z/2, so GH=1-z2: matching through first order is true while an all-orders identity is false. The shift keeps k0 irrelevant. This makes the source relation inspectable without removing the physical matching or naturalness assumptions.
The scale-family theorem fixes kj, Λ, ρ and B throughout one nonempty scale window, while gn(μ) runs with μ. The condition |1/a|≤ρΛ ensures that this window has a point. Choosing a different naturalness bound at each subtraction scale is not the statement being proved.
The review starts from the literal reduced chain amplitude, including the tree minus sign, p2∑n, and k-1 loop factors -(μ+ip). At μ=p, finite matching bounds derivative chains with factor (p/Λ)∑n. More importantly, if SL is the actual sum through L leading loops, Lean derives |SL-f0|=(√2|pg0|)L+1|f0|. For |1/a|≤ρp and 1+ρ≤√2, this error is at least |f0| at every cutoff. Merely having a nonzero omitted diagram would not establish that. The sufficient window and exact error bound are our deductions from the source model, not numerical estimates quoted from KSW.
The two local equations below now derive the source amplitudes; resummation does not assert convergence of the raw bubble series. Matching derives f0=(-1/a-ip)-1 and f1=-(r0/2)p2f02. For |Λr0/2|≤B and p>0, |f1|≤(Bp/Λ)|f0|. Thus Bp<Λ makes the first resummed correction strictly smaller, even where raw loop truncation fails. Through this correction only all-C0 chains and one dressed C2 insertion are retained. The source readout and independent consumer use the shared matching derivation. Zero or negative range is allowed; no full physical remainder bound follows.
ContactChains.matching_and_local_equations_control_the_pionless_expansion · original author TeX labels 6, 8, 9, 11 and 14 · Inspect the complete conditional argumentWhy the insertion has a squared denominator. Write K=μ+ip, h=g1p2 and D=1+g0K. The local equations are f0+g0Kf0=-g0 and f1+g0Kf1=-h(1+Kf0). The latter contains one derivative insertion, not an hKf1 feedback term. local_interaction_equations_iff_source_amplitudes derives D≠0, f0=-g0/D and f1=-h/D2, and proves the converse. This is our algebraic reconstruction of the source graphs and printed equation (13), not an additional equation quoted from the paper or a convergence claim. The public EquationThirteenAt now uses these equations, with an exact equivalence to its entire former specification, including zero momentum and zero leading contact. One explicit domain restriction is derived; changing the presentation does not itself remove the physical interaction assumptions.
Local rules determine the finite chains. ContactChains.chain_evaluation_iff_tree_and_pds_composition proves that the displayed chain formula is equivalent, for every nonempty chain, to its tree value -gnp2n and the rule that adjoining one vertex and bubble multiplies by gnp2n[-(μ+ip)]. The finite-sum error proof uses these rules. The empty-list value is not constrained. This makes the scalar on-shell composition assumption inspectable without deriving the original loop integral. The primary theorem no longer separately assumes Λ>0 or B≥0: they follow from 0<p≤Λ and the retained first naturalness bound. Its eight hypothesis arguments preserve all prior conclusions; replacing the two recurrence arguments with one equivalent coefficient condition does not reduce the independent physical assumptions.
What first order means here. In the selected two-contact model, insert V(ε)=g0+εh and F(ε)=f0+εf1 into the scalar equation F+VKF+V=0. The local equations are equivalent to the exact identity F+VKF+V=ε2hKf1 for every real ε. Thus the constant and linear residuals vanish; the quadratic one is not silently discarded as zero. local_equations_iff_quadratic_scattering_residual checks both directions. The public source readout and the complete matching theorem retain this identity, and the certified original power-counting route now derives it. For g0=h=p=1 and μ=0, the actual first-order solution leaves residual -ε2/2, which is nonzero at ε=1. Conversely, matching the equation only at ε=1 can misidentify the leading term. This parameter counts insertions, not powers of momentum. This characterizes the existing approximation without adding a physical premise; it supplies neither a full-EFT remainder bound nor a reason for a finite correction to be small.
The paper adapter now derives its requirement. Its former free Boolean-valued bubble-chain field has been removed. The replacement bubbleChainRequired states that every loop cutoff omits a C0-only chain of assigned order -1, at the selected channel, subtraction scale and momentum. bubble_chain_required_iff_source_orders proves that this is equivalent to leading-contact order -1 and loop order +1. The source setup and named derivation now retain these two integer-valued counting inputs; bubble_chain_realizes_shared_resummation_requirement uses the equivalence to derive the shared requirement. A wrong loop exponent fails despite the correct tree exponent. This is a repair of the formerly arbitrary interface, not equivalence to its old unconstrained meaning.
Remaining physical boundary. The primary quantitative argument is pointwise and retains a finite matching jet. The local interaction equations and evaluated PDS loop rule remain physical inputs; the two resummed amplitudes now follow algebraically. This does not prove convergence of the infinite chain series, a bound on unknown physical terms, or equivalence between one-sided amplitude bounds and the assigned-order interpretation. The separate fixed-window statement keeps coefficients and constants fixed across scales. The ordinal adapter establishes diagram-order completeness, not the quantitative obstruction proved separately here. Its interpretation of assigned orders as the source's enhanced-regime scaling remains an explicit physical obligation; integer annotations alone do not establish amplitude scaling. The finite matching and naturalness premises, source interpretation, and larger framework remain subject to human semantic validation; no review approval or whole-library reduction is claimed.
amplitudeHasKSWExpansion now constrains these actual complex values. The normalized amplitudes f0 = M A−1/(4π) and f1 = M A0/(4π) satisfy leading elastic unitarity and Im f1 = 2p Re(conj(f0) f1) at positive momentum. The latter is an interference identity, not exact unitarity of the truncated sum.
equation_thirteen_realizes_perturbative_elastic_unitarity · equation_thirteen_truncation_has_quadratic_optical_defect; ε is a real bookkeeping parameter.
The nonzero insertion control satisfies the full two-term source formula while its truncated S-matrix is not exactly unitary. This quadratic defect does not contradict order-by-order unitarity. Conversely, exactly resumming a derivative correction would add higher-order terms and would require its own approximation justification. No infinite-series convergence, controlled numerical error, or pion-inclusive A0 follows from the displayed two-term formula alone.
A second subtraction-scale control has the same two retained amplitudes. Resumming C0 + C2p² at each scale produces exactly unitary amplitudes that nevertheless differ between those scales. The theorem exact_unitarity_does_not_make_two_contact_resummation_scale_independent keeps this higher-order scale dependence distinct from failure of unitarity.
Explicit pions require a same-order quark-mass counterterm
The explicit-pion route depends on the mixed expansion and further selects momenta of order the pion mass. Its deferred five-graph calculation places one potential pion at subleading order and excludes radiation pions there. One subgraph carries logarithmic subtraction-scale dependence.
→ one potential pion at order p0, no radiation pion at that order, logarithmic scale dependence,
→ D2mπ2 required at order p0. including the quark-mass contact restores scale independence through the computed order; omitting it does not (5)
The same calculation states that the quark-mass contact is not suppressed relative to one-pion exchange once the leading contact has been resummed. It supplies the retained pion-inclusive beta equations for C0, C2, and D2 and completes the declared A0 amplitude. Nonconstant sampled parameter variation is a separate input; the beta equations do not require all three couplings to vary. Unlike the pionless route, this calculation does not claim a new explicit closed-form solution equality analogous to equation (11).
μ dC2/dμ = (M/2π) C0C2μ,
μ dD2/dμ = (M/2π) D2C0μ + M2gA2C02/(32π2f2). actual derivatives on neighborhoods of represented positive scales; source formulas at the computed order, not exact all-orders physical beta functions (5a)
Counterterm necessity is now derived from the same amplitude
The complete coefficient argument has a smaller interface: PionCoefficientData retains four constants M,gA,f,m, the scale and momentum maps, the selected momentum family, and the with/without coefficient pairs (A-1, A0). These nine fields are projected from existing data, not selected independently. The pairs contain only the leading and first-correction coefficients; no higher-order tail is stored here. Its contract retains the four reference values, actual scale image, positivity, pole exclusion, interacting witness and all four readout equations. The production source proof now uses this argument. Exact bridges preserve the whole pointwise and common-family contracts, including singlet identity, and the counterterm endpoint. A further theorem shows that changing the rest of the adapter cannot change those singlet propositions when the projected data agree. Checked arbitrary changes above n=1 preserve all three contracts; the full paper adapter retains those higher coefficients. An interacting test family permits a varying higher coefficient, so all-order invariance is not inferred. The review view makes this readout-level inference primary and retains the original calculation and full adapter separately. The adapter's 78 fields are not removed; no minimal independent basis or human approval is claimed.
The compact Lean specification has M,gA,f and four real functions c,s,r,d. Scale the soft variables together by Q and write C0=c/Q+s, C2=r/Q2, D2=d/Q2. With α=M/(4π), h=gA2/f2, D=1+αc(μ+ip), the retained coefficients are -c/D and -s/D2 plus graphs I through V. The first C0 correction is essential.
The graded equations are c'=αc2, s'=2αcs+αch, r'=2αcr, d'=2αcd+α2hc2/(2μ). Exact scaling identities connect them to the canonical printed beta functions. They are not exact nominal equations for C0=c+s.
Derived conclusion: on a connected open domain with M,f,mπ,p,μ>0, both retained coefficients are scale independent. Dropping only graph V while keeping the other data and running fixed leaves derivative α2hc2mπ2/(2μD2), nonzero where gA and c are nonzero. The paper adapter now imports explicit coefficient identification and scale-domain coverage, then uses this deduction. It no longer imports both cancellation verdicts.
One scale domain, not two: the paper adapter uses the actual image of its subtraction-scale map. It no longer chooses a second real set and then asks for coverage in both directions. The exact pion_coefficient_calculation_iff_explicit_scale_coverage equivalence recovers the entire former contract, including the interacting witness and all four coefficient readouts. Openness and connectedness remain explicit inputs. A checked finite-image rejection exposes the continuum RG scope; it does not say finite samples cannot disagree. The scale indexing and physical assumptions are unchanged, and no independent-assumption count is inferred.
No second constants in the coefficient calculation: both the calculation and fitted jets use the framework's existing M,gA,f. The earlier consolidation removed three duplicate constant choices and their equality premises, not three independent physical assumptions. The general pionCoefficientJet constructor still preserves the entire calibrated jet when its four functions are supplied. The finite-data construction below identifies functions only on the physical scale domain. The adapter still has 78 fields; physical identification and human review remain pending.
Four values replace four function-valued inputs: at the interacting reference scale μ*, choose c*,s*,r*,d*. Set a=M/(4π), h=gA2/f2, z=1-a c*(μ-μ*). The constructed flow is c=c*/z, s=(s*+h/2)/z2-h/2, r=r*/z2, d=[d*+a2h c*2log(μ/μ*)/2]/z2. Lean proves both directions between this reconstruction and the four graded RG equations on the open connected positive domain. The contact pole z=0 is excluded on the actual scale image. The complete former coefficient contract, including every readout, is recovered by pion_coefficient_calculation_iff_calibrated_jet. Outside-domain functions are not equated, as an interacting control demonstrates. This implements the source's reference-scale idea for separate grades, not a new four-parameter nuclear fit or an exact nominal flow. Graph identification and omitted-order control remain obligations.
Same-order relevance is not a supplied verdict: the broader route no longer imports a separate negated suppression relation. Lean derives a nonzero first coefficient difference between retaining and omitting graph V at some represented scale. Both order-label assignments remain imported. The tested counting claim is omission through the first correction at every represented scale, with the other inputs fixed; that claim is refuted. This repairs an unconstrained relation rather than proving equivalence to arbitrary old suppression flags. It is not a numerical lower bound at every scale or a verdict on all Weinberg schemes. The interacting diagnostic has D2=0 and identical with/without coefficients at μ=1, yet different coefficients elsewhere. Absorbing D2 into s changes other data and remains a different operation.
Necessary does not mean leading: the same interacting jet is scale independent through the first correction with graph V and scale dependent without it. At m=p=1, μ=2, both the leading coefficient L and the insertion difference V are nonzero. Yet |V/(L/Q)| tends to zero as Q approaches zero from above. This compares the Q0 insertion with the Q-1 leading contact amplitude, not with the Q0 pion exchange. The checked boundary rejects the same limit without the relative Q factor. Four old declarations, including a five-field scalar residual/order record, have been removed; no new physical record or predicate replaces them. This is not an independent-assumption count. The reconstructed-grade limit supplies no full-EFT chiral-limit validity or remainder bound.
One redundant premise removed: D≠0 follows from real coupling data and p>0. The exact admissible_on_iff_regular_domain equivalence recovers the entire former domain contract; the physical model is not weakened. At p=0 this reasoning fails: the separate IV/V domain still explicitly excludes a threshold pole and admits regular threshold points. This derives an existing restriction, not one fewer independent physical assumption.
Nonzero realization: M=4π, gA=f=1, c=-1/μ, s=-1/2, r=0 and d=log(μ)/(2μ2) satisfy the graded equations at every positive scale. With the mass insertion the retained prediction is unchanged; without it there are different predictions. This unitary-limit model is not a nuclear fit or a full nominal RG trajectory.
The coefficient argument has an observable readout: one canonical formula maps (A-1, A0) to (S0, δ1), with S0=1+iMpA-1/(2π) and δ1=MpA0/(4πS0). The original first-phase formula is preserved as its second component. This readout retains both coefficients when M,p and S0 are nonzero. The actual calculation derives unit modulus of S0 and reality of δ1, with or without graph V. With graph V the readout is scale independent; without it S0 is still constant but the first phase increment varies. No additional phase data or physical premises are introduced. Algebraic controls at zero M, zero p and S0=0 expose the inverse-readout boundary; these are not threshold evaluations of the pion graphs. No global logarithm branch, exact unitarity of the truncated full amplitude, fit quality or remainder bound is asserted. Human semantic approval remains pending.
Calibration does not require a continuous sample: the primary scattering result uses CalibratedAt and two distinct physical scale values. The same reference constants, positive domain, excluded contact pole, nonzero interactions and all four coefficient equations remain explicit. Direct algebra makes the with-graph-V coefficients constant at every sampled scale. Omitting graph V changes A0 by its logarithmic prefactor times log(μ/reference), so the omitted predictions agree exactly when their scale values agree. An interacting model sampled at 1 and 2 satisfies the complete counterterm result but fails the old connected-domain premise. Two labels at the same physical scale cannot detect scale dependence. The original CalculationAt remains exactly calibration plus its open/connected clauses; its full former existential contract and the paper adapters are preserved by checked equivalences. This does not reconstruct one common calibration from unrelated differential solutions on disconnected components or continue through the excluded pole. The source interpretation, truncation validity and human semantic review remain open obligations.
Under s→s-t m02, d→d+t the first coefficient changes by -t(m2-m02)/D2: one mass hides the distinction, a second mass can reveal it. Other parameters and the finite PDS convention stay fixed; no scheme-independent D2 value follows.
Absorption is not omission: setting d=0 and replacing s by s+d m02 preserves both retained predictions at the reference mass. The new contact runs with the additional source m02B/μ, where B=α2hc2/2. The mass dependence has moved, not disappeared. The checked interacting model remains scale independent after this absorption, unlike simply deleting graph V.
What two masses test: at fixed dressing, momentum and scale, no single mass-independent shift a+bp2 can cancel the actual logarithmic prefactor Bm2/D2 at two distinct positive masses when gA and c are nonzero. One mass can be matched; with zero axial coupling the obstruction disappears. This is a diagnostic of the retained operator basis, not a two-mass experiment reported by KSW or a uniqueness claim across arbitrary schemes.
The fit route now derives non-identifiability: its two stored verdict relations have been removed. One concrete fitted jet supplies the formula, using the framework's existing M,gA,f and four separately selected contact functions. The imported readback identifies the reported values C0=c+s, C2=r, D2=d at the selected scale, and the two retained coefficients at represented positive momenta. With the other data fixed, equality of the first coefficient is equivalent to equality of s+d m2. The theorem constructs distinct numerical C0,D2 values giving the same retained prediction curve; the source route no longer accepts a separate interpretation premise. Constant replacements compare parameters at one scale, not constant RG solutions.
What was and was not reduced: two freely assignable truth-valued fields were replaced by one fitted-model data family, and the interpretation implication is derived. The constructor count changes from 73 to 72, but the fitted model has seven data; this is not an independent-assumption count. The interacting readback and calibration checks reject matching c alone to the reported C0 and reject a wrong D2. They do not prove Nijmegen fit quality or omitted-term control.
No second M,gA,f: the subsequent consolidation replaces the seven-component fitted-model datum with its four contact functions and constructs the jet from the existing framework constants. The top-level count therefore moves from 72 to 75 while three duplicated constants and their equality clauses disappear. Lean characterizes equality of the entire old and constructed jets by calibrated constants and equality of the four functions. Every property of such an old jet is preserved; a model with a mismatched mass is not identified with the constructed one. The complete former readback is recovered, without changing the Fit/real-scale indexing or equating nominal and graded flows. This is not an independent-assumption count or a proof of the constants' physical interpretation.
No parallel scalar-only fit model: the old five-field record, three predicates and selected data definition have been removed. The fidelity example now compares the actual amplitude at m=μ=1, M=4π, gA=f=1, c=-1 and r=0. The pairs (s,d)=(-1/2,1) and (-3/2,2) give equal leading and first coefficients for every positive momentum, but their reported (C0,D2) pairs are (-3/2,1) and (-5/2,2). The checks reject agreement without the compensating s shift or at m=2. This removes five meaning-bearing declarations, not five independent physical assumptions. It is a fixed-scale amplitude diagnostic, not a nuclear fit or an RG trajectory.
One nucleon mass in the nominal flow: its former six-component record is replaced by gA, f and the three contact functions. The flow is constructed using the existing M, so its mass-calibration equality is derived. Equality of the entire old flow is characterized by calibrated data, including all function values, and the complete former coupling-representation contract is recovered. That earlier change moved the adapter count from 75 to 79 while one duplicated scalar is removed; this is not an independent-assumption count. The preservation and mismatch checks reject a different old mass and verify that the nominal flow, pionless formula and fitted jet share M. Nominal and graded contact functions remain distinct. Coupling readback and physical interpretation remain external.
Review boundary: projected singlet graph identification, the chiral mass operator, power-counting interpretation, omitted-term control and full-amplitude claims remain external. The printed II/III formulas require p>0; their threshold limits are separate. No principal-log phase branch is differentiated. The complete dependency view separates the compact calculation from the larger 78-field adapter. Both remain unreviewed; Lean compilation is not human semantic approval.
The logarithm and mass insertion are explicit formulas
Write D=1+(MC0/4π)(μ+ip), A-1=-C0/D and P=[gA2/(2f2)][mπMA-1/(4π)]2. The Lean definitions encode printed equation (15) on p. 6 (author-TeX label 17) directly. The retained phase readout is printed equation (20) on p. 7; equation (21) instead gives the fitted couplings.
A0(IV) = P [ -((μ+ip)/mπ)2 + i arctan(2p/mπ) - ½ log((mπ2+4p2)/μ2) + 1 ],
A0(V) = -D2mπ2/D2.
For positive μ, the explicit log coefficient is P=mπ2B/D2, where B=M2gA2C02/(32π2f2). At fixed C0 dressing, a formal log shift t is canceled by D2→D2+Bt. B is exactly the inhomogeneous term in the retained D2 beta function. These checked identities do not establish the complete scale cancellation, which also involves the other graphs and running dressing.
The source contract identifies the two nominal graph values on M,f,mπ,μ>0, p≥0 and D≠0. Finite threshold points are included; zero scale, the contact pole and the unevaluated chiral limit are excluded. Nominal graph values are distinct from formal expansion coefficients because running couplings can carry higher-order effects. The formula and boundary diagnostics test the signs, factors, a nonzero log coefficient and cancellation, and a zero-axial-coupling graph. The source-route contract connects the graph values to actual D2 running. Chiral interpretation, the remaining diagram calculation, truncation justification and human semantic approval remain outstanding.
The logarithmic claim now requires P≠0 at an admissible represented scale, equivalent there to gA≠0 and C0(μ)≠0. Lean derives the nonzero response P/μ of P log(μ) with P held fixed. This is not the total derivative of the running graph. The former two-scale graph-variation premise has been removed from this contract. An exact equivalence recovers the old contract only when that additional variation witness is restored. The checked comparison and controls include one represented scale with nonzero P but no possible two-sample graph difference, and vanishing P when either coupling is zero. That sampling example does not realize the open-domain graded route or assert a constant graph on an open interval. This is a correction of an overstrong source premise, not proof that the two contracts alone are equivalent. No new physical record or predicate is introduced; physical graph identification remains unreviewed.
PionInclusiveRGFlow keeps this real coupling family distinct from pionless running. PionInclusiveRetainedFlowRepresentsAt identifies the selected coupling values and mass with that same family. Beta values and weighted derivatives are now computed directly from it. explicit_pions_retain_the_actual_computed_order_beta_equations exposes the equations from the source route. The compatibility name pionInclusiveExactBetaFunction denotes the retained-model equation at positive sampled scales, indexed by the intrinsic source contact, not an assertion about omitted physical contributions.
One real flow supplies the beta equations
Four stored fields have been removed: an abstract beta-value type, independently chosen beta and derivative families, and their decoding function. The three sampled weighted equations now follow from the retained differential equations rather than being supplied again. That step reduced the framework from 79 to 75 stored fields; this is not a count of independent physical assumptions. Positive mass and decay constant, local derivatives on the represented scale domain, mass agreement, coupling calibration and the computed-order scope remain explicit.
The Lean preservation and boundary checks recover all three numerical clauses and retain the complete source, physical-readout and scale-cancellation results. An old encoded equality is equivalent when readback is injective and identifies both sides with the stated numbers. Without injectivity, equal physical numbers can have unequal tags. A local retained-system example has C0=C2=2 at μ=1, but β0=6 and β2=8: equal sampled values do not identify their operators. Intrinsic indices avoid imposing beta equalities through aliases of generic coupling labels.
This is an API correction, not equivalence to every old abstract representation. The example is a local jet, not a global RG trajectory or nuclear fit. No all-orders accuracy, nonconstant running or human semantic approval follows.
Local RG equations do not assert global continuation
The contract requires at least one represented positive scale and an open neighborhood of every such scale on which all three retained differential equations hold. It is stronger than fitting a derivative at one point, but does not constrain an arbitrary extension beyond those neighborhoods. The source specifies computed-order equations and boundary data at μ=mπ, not a global continuation theorem.
pion_rg_control_iff_global_on_positive_scale_coverage recovers the former global contract when every positive real scale is represented. Without that coverage this is a scope correction, not an equivalence. The local-domain diagnostic satisfies the equations near μ=1 with nonzero axial coupling and D2, but fails at μ=3. No nuclear fit, connection between disjoint neighborhoods, or human approval is claimed.
The inhomogeneous term has a checked consequence: with positive mass and decay constant and nonzero axial and leading contact couplings, D2 = 0 does not make its beta function zero. The same term prevents a regular extension of the weighted equation to μ = 0 under those conditions. A local affine coupling jet tests these consequences with actual derivatives; it is not claimed to solve the coupled RG system globally.
→ graph V cannot be postponed beyond that order with the other data fixed. the scoped omission claim in the Weinberg comparison, not a claim about every possible nuclear effective theory (6)
The checked theorem returns pion order, radiation-pion absence, logarithmic dependence, counterterm necessity, same-order status, three-coupling RG control, and subleading completeness; a separate obstruction theorem derives the scoped Weinberg-counting failure.
explicit_pions_complete_subleading_order_only_with_d2_counterterm · weinberg_counting_fails_for_declared_resummed_system · arXiv pp. 5–7Full and truncated amplitudes cancel scale dependence at different strengths
Pion-inclusive RG control and completeness of the subleading amplitude are the explicit inputs to the scale-cancellation route. The supplied cancellation calculation distinguishes an exact statement about the full amplitude from an order-qualified statement about the truncation.
A−1 + A0: independent only through order p0,
remaining scale dependence: higher order and canceled by later terms. running parameters do not imply a running physical amplitude (7)
PionAmplitudeScaleExpansion encodes formal coefficients with momentum power n - 1. The paper adapter derives omitted coefficients as full minus retained. Completeness now states agreement of the full and retained coefficients at n = 0, 1 at every represented scale; low-order omitted coefficients therefore vanish. Full-amplitude invariance remains a separate cancellation input. completion_and_full_invariance_derive_computed_order_invariance derives equality of the retained p-1 and p0 coefficients across subtraction scales. omitted_terms_cancel_the_actual_retained_residual also derives, at every order, retained(left) - retained(right) = -[omitted(left) - omitted(right)]. These coefficient identities imply neither convergence nor a numerical remainder estimate.
Coefficient conditions, not freely assigned verdicts
For every represented scale μ, radiation absence requires R0(μ)=R1(μ)=0. Completeness requires Fn(μ)=Tn(μ) for n=0,1 throughout the represented scale family. Here F and T are the full and with-D2 coefficient readouts. The named scale argument of subleadingAmplitudeComplete is retained for API compatibility; agreement only at that point is insufficient. Since O=F-T, the omitted low-order condition follows without another premise. The coefficient controls allow nonzero higher-order radiation and residuals but reject retained-order mismatches.
Two proposition-valued fields have been replaced by one complex radiation-coefficient family, reducing stored fields from 79 to 78. This is not an independent-assumption count. The scale_cancellation_iff_identified_legacy_contract equivalence requires identification of the old completeness flag with this coefficient meaning; it is not an unconditional equivalence to arbitrary old verdicts. Graph identification, the coefficient map, the radiation calculation, physical truncation validity and full-amplitude invariance remain external. No convergence, numerical accuracy or human semantic approval is established.
The residual is derived; its order is not
The earlier removal of the independent omitted-coefficient field and duplicate completion premise left 74 stored framework fields at that stage. pion_amplitude_readout_eq_generated_iff proves equality of the entire old and generated records when their full and retained families agree and the old completion identity holds. With the coefficient meaning of completeness identified explicitly, the complete Lean contract recovers the former source cancellation output pair and both original conclusions. It does not preserve arbitrary old completeness verdicts.
Full invariance and low-order coefficient matching remain physical inputs. An actual-adapter diagnostic retains nonzero low-order coefficients but has a scale-dependent higher coefficient, compensated by its derived residual. Moving the mismatch to leading order violates the low-order condition even though exact completion and full invariance still hold. Bookkeeping is not a truncation estimate; no convergence, nuclear accuracy or human semantic approval is inferred.
One coefficient comparison for both counterterm claims: agreement through index d now means equality of every coefficient n≤d. The freely chosen agreement relation has been removed. Through order p0, both the with-D2 and without-D2 families compare indices 0 and 1. The counterterm condition is equivalent to equality of these coefficients at every pair of scales with D2, plus a retained-coefficient mismatch at some pair without it. A diagnostic allows nonzero higher-order scale dependence in the with-D2 family. The former RG interpretation clause is derived; comparison with an arbitrary former relation requires that it already meant coefficient equality. This supplies no bound on the physical remainder. The coefficient map and the pion diagram calculation remain explicit inputs.
A separate seven-theorem pion-inclusive client changes the mass and pion parameters, verifies a positive-scale derivative jet, and uses four public APIs. Its formal retained amplitude has a nonzero higher-order residual -7 that is exactly compensated by omitted terms, while its two retained low-order coefficients remain invariant. It therefore tests the distinction between computed-order and all-order invariance directly.
The formalization derives full physical invariance, truncated invariance through the computed order, and a higher-order residual. It also realizes running parameter flow and invariant predictions in the shared RG vocabulary.
pion_inclusive_rg_control_leaves_physical_amplitude_scale_independent · pion_inclusive_rg_control_makes_truncated_amplitude_scale_independent_through_computed_order · arXiv p. 7A good fit does not identify every fitted parameter or control every omitted term
The fit route depends on the complete subleading pion amplitude. It imports a fit to Nijmegen singlet phase shifts through 200 MeV and uses a deferred numerical calculation. The fitted leading coupling lies near its large-length value, the derivative coupling has the expected size, and the phase-shift agreement is good. The same calculation retains a different scope fact: through the computed order, the amplitude can be written with the C0 + D2mπ2 combination, so the separately quoted C0 and D2 values are not individually meaningful.
→ expected fitted coupling sizes + good singlet phase-shift agreement,
amplitude uses only C0 + D2mπ2 through p0 → C0 and D2 are not separately meaningful,
expected sizes + author interpretive bridge → channel-scoped suggestion that the expansion is valid. parameter non-identifiability is derived from the calibrated retained model; validity support remains a separate author interpretation (8)
singlet_fit_retains_c0_d2_combination_scope derives the combination-only amplitude fact and distinct numerical parameter pairs with the same retained prediction curve. It no longer takes the non-identifiability interpretation as a separate premise. Physical readback and empirical fit quality remain distinct inputs.
singlet_fit_retains_c0_d2_combination_scope · arXiv p. 7That suggestion does not settle the truncation error. Above 100 MeV, the magnitude of the subleading-to-leading amplitude ratio is at least roughly one half. The supplied assessment therefore denies control of neglected terms quadratic in that ratio, even while retaining the good phase-shift agreement.
→ neglected quadratic terms are not controlled,
while empirical phase-shift adequacy may still hold. empirically adequate but uncontrolled at the selected subleading truncation and regime (9)
The shared effective-theory adapter certifies calculation completeness and empirical adequacy, then proves the absence of remainder control. Neither expected coupling sizes nor a good fit licenses the missing implication.
high_momentum_fit_does_not_control_neglected_terms · high_momentum_fit_realizes_shared_uncontrolled_truncation · arXiv pp. 7–8The coupled-channel prediction is parameter-free but not uniformly subleading-complete
This route begins independently with a large triplet scattering length and analogous power counting. At leading order only the S-to-S amplitude component may be nonzero; the S-to-D, D-to-S, and D-to-D components vanish. From these numerical zeros, the printed S-matrix relation, and explicit intervals for the phase representatives, Lean derives zero leading mixing and D-wave phase. The implication itself is no longer assumed.
leading amplitude order p-1 (phase degree 0): ASD = ADS = ADD = 0
→ ε1 = 0 and δ2 = 0 at phase degree 0. derived on the explicit zero-centered branch above; only the S-to-S component is allowed to remain nonzero (10)
Common phase degree is not relative accuracy
The former adapter reused the amplitude's leading/subleading labels for observable accuracy. It now uses a common nonnegative phase degree: degree n corresponds to amplitude order pn-1. The first allowed degrees are 0 for δ0 and 1 for ε1, δ2. Thus common degree 1 is subleading for the S-wave phase, but only leading for mixing and the D-wave phase. The post-calibration prediction now uses degree 1, not the zero-mixing background.
The Lean theorem phase_matrix_first_variation_at_unmixed_background checks this distinction against the actual printed matrix. Around δ0=δ, ε1=δ2=0, its first variation is:
An actual differentiable phase family has zero background mixing but a nonzero first variation. The relative-accuracy contract also admits all three phases through common degree 1 while rejecting uniform relative next-to-leading accuracy, which would require degree 2 for mixing and the D wave. This is a correction, not equivalence to the old shared order labels. The degree is formal soft-scale counting, not a momentum Taylor order at fixed pion mass, a convergence claim, or proof of the deferred nuclear calculation. Human review remains pending.
Through means every lower degree: calculation coverage through n is now defined as availability of every coefficient k≤n, including known zeros. Individual availability remains explicit input, not certified physical correctness. The gap diagnostics allow an isolated higher coefficient without reporting a complete expansion. The source's degree-one coverage plus failure at degree two now identifies the unavailable mixing and D-wave coefficient precisely; it does not set that coefficient to zero. An old cumulative predicate is recovered at every degree exactly when it was downward closed.
| Observable | Relative accuracy | Common phase degree | Calibration status |
|---|---|---|---|
| S-wave phase δ0 | Subleading order | 1 | Three S-to-S amplitude parameters are fitted to it. |
| Mixing angle ε1 | Leading order only | 1 | No additional parameter after the S-wave fit. |
| D-wave phase δ2 | Leading order only | 1 | No additional parameter after the S-wave fit. |
The complete analytic order-p0 formula for every coupled-amplitude component remains deferred. Thus “parameter-free” describes calibration at the declared order; it does not give the mixing and D-wave observables the same relative accuracy as the S-wave phase.
The formalization derives the leading phase zeros from the displayed S-matrix and vanishing numerical amplitude entries on an explicit branch. It keeps the parameter-free post-calibration predictions and proves the failure of uniform subleading completeness across the three observables. The calculation of the amplitude entries and higher-order predictions remains input, not a new result of this branch argument. The active-sector theorem separately witnesses that the selected mixing observable is genuinely calculated rather than merely excluded from the fit.
coupled_channel_calculation_retains_displayed_s_matrix_formula · coupled_channel_predictions_are_parameter_free_after_s_wave_fit · coupled_channel_calculation_has_nonuniform_observable_order · coupled_mixing_realizes_active_prediction_sector · arXiv pp. 8–9Accuracy of an inverse amplitude needs a conditioned observable readout
The real phase function and reduced physical amplitude are related by the source inverse-amplitude formula. The library derives the exact distance identity below from that formula. A quantitative phase error is an additional premise, not a consequence of having summed the PDS diagrams or assigned an EFT order.
|f(K1,k) - f(K2,k)| = |K1 - K2|/(|K1 - i k| |K2 - i k|).
k >= k_min > 0 and |K1 - K2| <= e imply |f(K1,k) - f(K2,k)| <= e/k_min^2. The PDS formula, real nonzero contact, amplitude normalization, and supplied phase-remainder bound are distinct inputs.
controlled_phase_error_bounds_the_pds_amplitude_error uses the actual paper bubble formula and nonzero real contact to identify the target amplitude, then applies the shared stability theorem. A positive lower momentum bounds the two denominator norms. The resulting estimate is deliberately nonuniform at threshold; this algebraic bound does not estimate any omitted pion, derivative, or relativistic term.
|f(K1,p)|, |f(K2,p)| >= b > 0 and amplitude error <= e imply phase-function error <= e/b2.
On 1 <= p <= 2 with |K1|, |K2| <= 1, b=1/3 suffices, giving error <= 9e.
Diagnostic K1=L, K2=2L: both amplitudes are exactly elastic-unitary and their distance is <= 1/(2L), while |K1-K2|=L. The inverse bound needs amplitude conditioning, not only a positive momentum floor. The numerical domain and constants use a fixed normalization.
The Lean-grounded nuclear review now exposes the exact inverse identity, its uniform-conditioning hypothesis, and the bounded-domain recovery theorem. For every positive amplitude tolerance, the diagnostic has a choice L>=1 on the same fixed band 1<=p<=2 that fails phase accuracy 1/2. It changes scattering length across models and leaves the large-length regime; it is not a regulator limit, a nuclear fit, or a finite-range potential realization. These conditional error bounds are deductions in the library, not uncertainty estimates attributed to KSW, and they do not reconstruct a unique phase angle or potential. Human semantic review remains pending.
Concept guide
Large scattering length
The low-energy regime in which the scattering length is unnaturally large and the leading contact cannot be treated by ordinary uniform perturbation theory.
largeScatteringLengthEffective-range matching
The selected low-momentum family p cot δ = -1/a + (r0/2)p2 + remainder, with scattering length, effective range, and applicability retained as data.
effectiveRangeDataMatched · effectiveRangeExpansionValueAtPower divergence subtraction
The selected nonzero subtraction prescription whose scale is taken comparable to momentum in the mixed-counting route.
pdsSubtractionAtBubble-chain resummation
The all-orders construction that turns the PDS loop and required chain into the pionless amplitude.
BubbleResummationCalculationRG control and nonconstant running
The pionless RG route derives the actual beta equations and real running values from observable/contact families; it does not assume nonconstant running. Equation (11) implies nonconstant C0 on positive non-pole scales; C2 is nonconstant there exactly when the effective range is nonzero. Values at the pole are excluded. The explicit-pion source contract likewise requires its retained equations and real-flow interpretation, not variation of all three couplings. Setting C2 identically to zero preserves those equations without changing C0 or D2. Exact amplitude scale cancellation remains separate from parameter variation. The shared nonvacuous-running endpoint additionally requires two positive sampled scales with unequal real values of at least one of C0, C2, D2; the representation relation then transfers that difference to the shared parameter family. This sampling evidence is an explicit extra premise, not a conclusion of the beta equations or a claim of all-orders accuracy.
pionless_rg_exposes_derivative_equations_and_running_solutions · equation_eleven_classifies_nonconstant_couplings · pionInclusiveRGControlledCouplings · SampledPionParameterVariationMinimal-subtraction scope
The contrast between ordinary natural-regime counting and the narrower inverse-scattering-length window at large |a|.
LargeLengthMSRestrictionCalculationMixed KSW expansion
A resummed leading contact together with perturbative higher corrections, yielding an amplitude ordered as leading, subleading, and higher terms.
KSWMixedExpansionAtPotential pion
The one-pion-exchange contribution counted at subleading order when momentum is of order the pion mass.
potentialPionAtSubleadingOrderQuark-mass counterterm
The D2mπ2 interaction required to restore scale independence through subleading order and not suppressed relative to one-pion exchange.
quarkMassCountertermRequiredPhysical scale independence
Equality of the full scale-indexed amplitude to one physical amplitude at every subtraction scale.
fullAmplitudeScaleIndependentSinglet fit
The imported Nijmegen-data setup and deferred numerical fit through 200 MeV, retaining expected sizes, phase agreement, the C0/D2 combination-only scope, and the high-momentum warning.
SingletFitCalculation · C0D2CombinationInterpretationEmpirically adequate but uncontrolled
A complete selected calculation with good phase-shift agreement but without control of its neglected quadratic terms above 100 MeV.
highMomentumTruncationContextMixed-order coupled prediction
A coupled-channel result whose S-wave phase reaches subleading order while mixing and D-wave observables remain leading-order predictions.
mixingAndDWaveOnlyLeadingOrderPost-calibration parameter-free prediction
A target outside the S-wave calibration sector that requires no additional fit parameter at its declared leading order.
toPostCalibrationPredictionContextTheory–world grounding
The additional theory use, world representation, empirical interpretation, and claim bridges required before a formal model result is transferred to theory and physical world.
toRenormalizedPredictionTheoryModelInterpretationComplete route inventory, non-implications, and provenance
The source map declares seven routes, sixty-three claims, and sixty-three sourced steps. Coverage assigns every atom paper-local semantics and certifies every route. The inventory below preserves all declared dependencies and outputs; no all-routes theorem conflates them into one stronger conclusion.
| Route | Direct dependencies | Declared outputs | Profile |
|---|---|---|---|
| Pionless PDS | — | All-orders amplitude, unitarity, exact beta functions, value-level equation-(11) C0/C2 RG control, full scale independence | exact construction from deferred calculations |
| Minimal-subtraction scope | — | Natural-regime validity, inverse-length window, restricted large-length range | scope contrast |
| Large-length power counting | — | Mixed expansion, amplitude expansion, shared nonuniform power counting | main conclusion |
| Explicit pions | Large-length power counting | Potential-pion order, radiation-pion absence, logarithm, D2 necessity and same-order status, three-coupling RG control, subleading completeness, Weinberg obstruction | five-graph calculation |
| Scale cancellation | Explicit pions | Full invariance, truncated invariance through subleading order, higher-order residual | renormalization accounting |
| Singlet fit | Explicit pions | Expected couplings, C0/D2 combination scope, non-separate meaning, good agreement, validity suggestion, large ratio, uncontrolled neglected terms | fit with validity warning |
| Coupled channel | — | Displayed S-matrix formula, leading S-only amplitude, zero leading mixing/D phase, subleading S phase, mixed orders, deferred formula, parameter-free predictions | mixed-order prediction |
Pionless PDS · pionless_pds_route_is_semantically_realized
Minimal-subtraction scope · minimal_subtraction_scope_route_is_semantically_realized
Large-length power counting · large_length_power_counting_route_is_semantically_realized
Explicit pions · explicit_pions_route_is_semantically_realized
Scale cancellation · scale_cancellation_route_is_semantically_realized
Singlet fit · singlet_fit_route_is_semantically_realized
Coupled channel · coupled_channel_route_is_semantically_realized
Selected formally blocked shortcuts
| Fact available | Conclusion that does not follow by itself | Lean witness |
|---|---|---|
| Actual retained pion-inclusive derivative equations | The pionless C0 equation | actual_pion_derivatives_do_not_satisfy_the_pionless_c0_equation |
| D2 vanishes at a positive scale | Its derivative vanishes | zero_d2_does_not_mean_zero_d2_running |
| Positive-scale retained equations and nonzero source couplings | The weighted D2 equation extends to zero scale | the_zero_scale_endpoint_cannot_satisfy_the_weighted_d2_equation |
| Full invariance, higher-order completion, and computed-order agreement | All retained coefficients are invariant | computed_order_cancellation_does_not_give_exact_retained_invariance |
| Full invariance and coefficient completion | Computed-order agreement without restricting the omitted orders | full_invariance_without_the_omitted_order_condition_is_insufficient |
| Correct physical contact values at zero subtraction scale | The actual beta-function derivatives | a_correct_zero_scale_sample_does_not_determine_the_beta_equations |
| A candidate derivative satisfies the zero-scale weighted equality | The unweighted derivative equation | the_zero_scale_weight_does_not_test_a_candidate_derivative |
| The zero-scale boundary point is non-pole | The contact pole is also admissible | the_contact_pole_is_not_a_zero_scale_boundary_point |
| Effective-range agreement at one momentum | The full low-momentum p cot δ family | one_momentum_agreement_does_not_supply_effective_range_family |
| Positive-scale on-shell PDS loop and nonsingular bubble denominator | The printed equation-(5) resummed amplitude | named_pds_outputs_do_not_supply_equations_five_and_six |
| Correct leading C0 amplitude with a nonzero C2 | The single derivative-insertion amplitude | leading_source_term_does_not_supply_derivative_insertion |
| Actual two-term source formula and first-order optical theorem | Exact unitarity of the truncated sum | source_single_insertion_is_not_an_exactly_unitary_truncation |
| Equal retained terms and exactly unitary two-contact resummations at distinct scales | Scale independence of the resummed amplitude | exact_unitarity_does_not_make_two_contact_resummation_scale_independent |
| Positive-momentum phase matrix with symmetric off-diagonal entries | The amplitude-normalized S-matrix relation | named_coupled_phase_output_does_not_supply_s_matrix_formula |
| PDS loop value | Resummed amplitude value | loop_integral_does_not_by_itself_supply_resummed_amplitude |
| Graph V is required for retained-order scale independence | It must be leading: its ratio to A-1/Q need not vanish | scale_independence_requirement_alone_does_not_fix_relative_power_counting: the actual nonzero ratio tends to zero |
| An exact zero beta equation | Nontrivial running | exact_zero_beta_equation_does_not_imply_nontrivial_running |
| A nonconstant coupling | The declared RG equation or selected running solution | nonconstant_running_does_not_supply_rg_equation_or_solution |
| Positive non-pole equation-(11) data with the correct C0(μ) | The displayed C2(μ) value | named_running_solution_does_not_supply_equation_eleven_values |
| Good fit agreement | Controlled truncation | good_fit_does_not_imply_controlled_truncation |
| Expected fitted coupling sizes | Controlled correction hierarchy | expected_coupling_sizes_do_not_establish_controlled_corrections |
| Quoted C0/D2 values with combination-only amplitude | Separate parameter meaning | reported_c0_and_d2_values_with_combination_only_amplitude_do_not_supply_separate_meaning |
| Running couplings | A running physical amplitude | running_couplings_do_not_imply_running_physical_amplitude |
| Parameter-free selected predictions | Uniform subleading completion | parameter_free_prediction_does_not_imply_uniform_subleading_completion |
| Pionless low momentum | Removal of the large-length MS restriction | pionless_scope_does_not_remove_large_length_ms_restriction |
The formula-level witnesses retain actual domains and partial outputs. The PDS witness has positive subtraction scale, on-shell energy, the complete InPDS family, and a nonsingular denominator but the wrong amplitude. The coupled witness retains the complete phase matrix while its nonzero S-wave amplitude violates S - 1 = i p M A/(2π). The running witnesses use two positive non-pole scales and the literal pionless beta and equation-(11) forms; the fit witness gives distinct C0,D2 assignments with identical actual leading and first amplitude coefficients at the fixed pion mass and scale for every positive momentum; and the scope witness keeps both selected momenta pionless while only one lies below 1/|a|. These are numerical/formula countermodels, not truth labels or nuclear fits.
Source-formula identifiers. The source map keeps
pdsLoopFormula as claim loopFormula through
retainPDSLoopFormula, and
pdsAmplitudeFormula as claim
amplitudeFormula through
retainPDSAmplitudeFormula. It also keeps
coupledSMatrixFormula as a claim of the same name
through retainCoupledSMatrixFormula; the zero-phase
step consumes that claim and leadingSOnly.
Machine-checked audit boundary
argument_wellFormed, argument_auditable, and routes_wellFormed certify source-map structure. every_source_claim_has_semantics covers all sixty-three claims, and route_semantic_realization_is_exhaustive covers all seven route identifiers. Dedicated audits retain the mixed expansion’s controlled-regime and deferred-calculation inputs, the minimal-subtraction scope restriction, the C0/D2 combination dependency of the parameter-meaning qualification, the fit’s author-expectation bridge, the controlled high-momentum warning, the D2-dependent Weinberg obstruction, the pion-inclusive RG dependency of scale cancellation, the coupled route’s deferred and mixed-order status, and the displayed S-matrix dependency of the zero-phase inference.
Lean-encoded bibliographic record
D. B. Kaplan, M. J. Savage, and M. B. Wise, A New Expansion for Nucleon-Nucleon Interactions (1998), arXiv:nucl-th/9801034v2, pp. 1–10.
TraceComplete Lean semantic identifier ledger
Reading note. The article above is the human exposition. This collapsed cross-reference records every public theorem and every constructor of the five paper-local source-map vocabularies. It introduces no additional claim; its purpose is to make semantic omissions mechanically detectable.
Primary semantic theorems (207)
equation_eleven_classifies_nonconstant_couplingsequation_eleven_iff_first_two_matching_equationsobservable_family_derives_equation_elevenequation_eleven_derives_actual_beta_derivativesrunning_values_control_resummed_termsmatched_running_values_control_resummation_and_first_correctionobservable_matching_controls_the_complete_first_order_argumentobservable_matching_realizes_a_controlled_resummation_windowobservable_family_controls_running_and_resummed_termsactual_beta_derivatives_retain_the_printed_scale_weightequation_eleven_retains_zero_scale_boundary_datascale_window_derives_leading_contact_boundsequation_eleven_derives_normalized_derivative_contactscale_window_derives_first_two_contact_boundsa_correct_zero_scale_sample_does_not_determine_the_beta_equationsthe_zero_scale_weight_does_not_test_a_candidate_derivativethe_contact_pole_is_not_a_zero_scale_boundary_pointpositive_comparable_scale_can_hit_the_contact_polefixed_scattering_length_does_not_allow_the_window_at_all_momentaretained_indices_are_exactly_the_powers_through_zerocompletion_and_full_invariance_derive_computed_order_invarianceomitted_terms_cancel_the_actual_retained_residualcomputed_order_cancellation_does_not_give_exact_retained_invariancefull_invariance_without_the_omitted_order_condition_is_insufficientreal_contact_bubble_formula_has_unitary_source_normalizationon_shell_energy_iff_nonrelativistic_dispersionsource_scalar_s_matrix_has_reduced_amplitude_normalizationreal_contact_retains_actual_bubble_denominatorequation_six_recovers_actual_reduced_contact_amplitudeequation_six_with_real_contact_proves_elastic_unitaritynonzero_contact_recovers_source_inverse_amplitudecontrolled_phase_error_bounds_the_pds_amplitude_errorelastic_control_bubble_denominatorelastic_control_reduced_amplitudeelastic_control_realizes_source_bubble_formulasreal_contact_bubble_sum_realizes_source_unitaritycomplex_contact_bubble_formula_does_not_supply_elastic_unitaritynamed_pds_outputs_do_not_supply_equations_five_and_sixphase_matrix_first_variation_at_unmixed_backgroundzero_amplitudes_determine_phases_on_branchnamed_coupled_phase_output_does_not_supply_s_matrix_formulaequation_thirteen_iff_local_interaction_equationsequation_thirteen_iff_graded_scattering_equationequation_thirteen_iff_first_order_scattering_equationequation_thirteen_iff_reduced_source_termsequation_thirteen_iff_source_termsequation_thirteen_has_actual_reduced_amplitudesequation_thirteen_realizes_perturbative_elastic_unitarityequation_thirteen_truncation_has_quadratic_optical_defectsingle_insertion_control_realizes_source_formulaother_subtraction_scale_retains_source_amplitudesexact_unitarity_does_not_make_two_contact_resummation_scale_independentleading_source_term_does_not_supply_derivative_insertionsource_single_insertion_is_not_an_exactly_unitary_truncationdiagram_interpretation_derives_mixed_treatmentsradiation_absence_iff_zero_leading_and_first_coefficientspion_flow_eq_iff_calibrated_datagenerated_pds_readout_has_nonrelativistic_shellpds_readout_eq_generated_iff_kinematics_and_shellscale_comparison_iff_fixed_ratio_boundsscale_comparison_excludes_minimal_subtractionbubble_chain_required_iff_source_ordersenhanced_scaling_selects_the_resummed_sectorsource_mixed_expansion_has_perturbative_elastic_unitarityeffective_range_remainder_reconstructs_observableeffective_range_matching_iff_uniform_remaindereffective_range_matching_identifies_observable_coefficientseffective_range_matching_controls_sampled_remainderzero_momentum_effective_range_matching_retains_inverse_scattering_lengthsampled_equation_eleven_formulas_unchangedpionless_observable_matching_iff_contact_familyobservable_matching_derives_running_valuesequation_eleven_values_derive_real_beta_equationsobservable_matching_controls_the_first_two_pionless_amplitudespion_flow_representation_iff_with_mass_calibrationpion_rg_control_iff_global_on_positive_scale_coveragecontrolled_pion_running_retains_actual_weighted_equationscontrolled_pion_running_identifies_sampled_valuessubleading_complete_iff_omitted_coefficients_vanishpion_amplitude_scale_expansion_is_completepion_amplitude_readout_eq_generated_iffpion_amplitude_coefficient_agreement_is_derivedfull_amplitude_invariance_preserves_every_formal_coefficientsampled_pion_parameter_variation_realizes_rg_parameter_flowrunning_coupling_realizes_rg_parameter_flowfull_amplitude_scale_independence_realizes_matching_at_every_scalefull_amplitude_scale_independence_realizes_cross_scale_prediction_agreementfull_amplitude_target_prediction_is_activefull_amplitude_scale_independence_and_running_coupling_realize_nonvacuous_rg_prediction_independencepion_inclusive_renormalization_model_retains_paper_semanticspion_inclusive_inputs_select_shared_renormalized_prediction_setupselected_pion_inclusive_system_retains_channel_and_momentumpion_inclusive_inputs_make_shared_renormalization_route_applicablepion_inclusive_inputs_realize_structural_renormalized_prediction_explanationpion_inclusive_source_derivation_makes_shared_renormalization_route_applicablepion_inclusive_running_couplings_and_scale_independent_full_amplitude_realize_source_structural_renormalized_prediction_explanationpion_inclusive_renormalization_realizes_shared_predictionpion_inclusive_renormalization_exhibits_nonvacuous_shared_predictionselected_amplitude_family_makes_shared_empirical_grounding_route_applicablepion_inclusive_renormalization_establishes_empirically_grounded_predictionpion_inclusive_renormalization_realizes_every_shared_claimpion_inclusive_model_inputs_establish_theory_model_groundingpion_inclusive_renormalization_establishes_theory_model_grounded_predictiongrounded_pion_inclusive_renormalization_transfers_every_shared_claimformer_pion_log_contract_iff_explicit_log_and_graph_variationexplicit_pion_log_has_a_nonzero_fixed_dressing_responsequark_mass_counterterm_required_iff_coefficient_witnesspion_coefficient_jet_eq_iff_calibrated_datapion_coefficient_argument_iff_selected_datasinglet_coefficient_argument_preserved_by_same_datapion_coefficient_family_specializes_at_momentumpion_coefficient_family_iff_common_calibrated_jetpion_coefficient_calculation_iff_calibrated_jetpion_coefficient_calculation_iff_explicit_scale_coveragepion_coefficient_calculation_requires_the_mass_countertermpion_coefficient_calculation_exposes_a_nonzero_mass_insertionobservable_normalization_and_upstream_formula_iff_contact_readoutscale_cancellation_iff_identified_legacy_contractsinglet_fit_jet_eq_iff_calibrated_datasinglet_fit_readback_derives_the_contact_combinationc0_d2_combination_interpretation_is_derivedcoupled_readout_eq_generated_iff_normalizeddisplayed_coupled_formula_iff_phase_matrixold_coupled_formula_iff_generated_and_normalizedcoupled_coverage_is_downward_closedcoupled_coverage_successor_iffcoupled_coverage_matches_input_iff_downward_closedpds_subtraction_yields_loop_integralpds_loop_calculation_retains_equation_five_formulabubble_chain_and_loop_yield_full_amplitudebubble_resummation_retains_equation_six_formulapds_amplitude_has_unitary_s_wave_formpionless_observable_matching_constrains_the_bubble_contactpionless_unitarity_realizes_actual_nonvacuous_elastic_s_wavepds_bubble_resummation_yields_pionless_amplitudepionless_pds_setup_realizes_shared_large_length_setupbubble_chain_realizes_shared_resummation_requirementpds_bubble_sum_realizes_shared_all_order_resummationunitarity_realizes_shared_low_energy_recoverypionless_inputs_make_shared_large_length_route_applicablepionless_pds_route_realizes_large_length_resummation_derivational_reductionpionless_pds_inputs_realize_structural_large_length_resummation_explanationpionless_pds_realizes_shared_large_length_resummationpionless_resummation_model_retains_paper_semanticspionless_source_derivation_makes_shared_large_length_route_applicablepionless_pds_source_inputs_realize_source_structural_large_length_resummation_explanationpionless_source_inputs_realize_source_large_length_resummation_derivational_reductionpionless_pds_exhibits_nonvacuous_shared_large_length_resummationksw_resummed_mixed_expansion_realizes_composed_renormalized_predictionksw_resummed_mixed_expansion_realizes_source_sensitive_renormalized_predictionpionless_resummation_model_retains_two_nucleon_pds_systempionless_resummation_model_inputs_establish_theory_model_groundingpionless_pds_establishes_grounded_large_length_resummationgrounded_pionless_resummation_transfers_every_shared_claimscale_independence_yields_running_couplings_and_rg_equationspionless_rg_retains_equation_eleven_running_valuespionless_rg_retains_actual_beta_derivativespionless_rg_exposes_derivative_equations_and_running_solutionslarge_scattering_length_requires_resummed_leading_contactnatural_and_large_scattering_lengths_have_distinct_ms_scopesksw_mixed_expansion_realizes_shared_power_countingexplicit_pions_complete_subleading_order_only_with_d2_countertermexplicit_pions_identify_the_mass_counterterm_insertionexplicit_pions_expose_pion_inclusive_rg_equationsexplicit_pions_link_logarithm_mass_insertion_and_runningexplicit_pions_retain_the_actual_computed_order_beta_equationsweinberg_counting_fails_for_declared_resummed_systempion_inclusive_rg_control_leaves_physical_amplitude_scale_independentpion_inclusive_rg_control_makes_truncated_amplitude_scale_independent_through_computed_ordersource_scale_cancellation_retains_the_actual_higher_order_compensationexpected_fitted_coupling_sizes_support_channel_scoped_validitysinglet_fit_supports_expansion_in_declared_channelsinglet_fit_retains_c0_d2_combination_scopehigh_momentum_fit_does_not_control_neglected_termshigh_momentum_fit_realizes_shared_uncontrolled_truncationcoupled_channel_leading_order_forces_zero_mixing_and_d_wavecoupled_channel_calculation_retains_displayed_s_matrix_formulacoupled_channel_predictions_are_parameter_free_after_s_wave_fitcoupled_channel_calculation_has_nonuniform_observable_ordercoupled_calculation_reaches_common_phase_degree_onecoupled_calculation_leaves_second_degree_coefficients_unavailablepost_calibration_prediction_model_retains_paper_semanticscoupled_inputs_realize_shared_post_calibration_setupcoupled_calculation_realizes_shared_mixing_predictioncoupled_inputs_make_shared_post_calibration_route_applicablecoupled_mixing_realizes_shared_post_calibration_predictioncoupled_mixing_exhibits_nonvacuous_shared_post_calibration_predictioncoupled_inputs_realize_structural_post_calibration_prediction_explanationksw_post_calibration_source_derivation_makes_shared_route_applicablecoupled_s_phase_fit_and_parameter_free_mixing_prediction_realize_source_structural_post_calibration_prediction_explanationcoupled_mixing_realizes_active_prediction_sectorcoupled_model_inputs_establish_theory_model_groundingcoupled_mixing_establishes_grounded_shared_predictiongrounded_coupled_mixing_prediction_transfers_every_shared_claimone_momentum_agreement_does_not_supply_effective_range_familyloop_integral_does_not_by_itself_supply_resummed_amplitudescale_independence_requirement_alone_does_not_fix_relative_power_countingexact_zero_beta_equation_does_not_imply_nontrivial_runningnonconstant_running_does_not_supply_rg_equation_or_solutionnamed_running_solution_does_not_supply_equation_eleven_valuesgood_fit_does_not_imply_controlled_truncationexpected_coupling_sizes_do_not_establish_controlled_correctionsreported_c0_and_d2_values_with_combination_only_amplitude_do_not_supply_separate_meaningrunning_couplings_do_not_imply_running_physical_amplitudeparameter_free_prediction_does_not_imply_uniform_subleading_completionpionless_scope_does_not_remove_large_length_ms_restrictionksw_realizes_shared_post_calibration_empirical_boundary
Coverage theorems (13)
unitary_atom_retains_actual_scalar_s_matrixevery_source_claim_has_semanticspionless_pds_route_is_semantically_realizedpionless_pds_route_exposes_equations_five_and_sixminimal_subtraction_scope_route_is_semantically_realizedlarge_length_power_counting_route_is_semantically_realizedexplicit_pions_route_is_semantically_realizedscale_cancellation_route_is_semantically_realizedsinglet_fit_route_is_semantically_realizedcoupled_channel_route_is_semantically_realizedcoupled_channel_route_exposes_displayed_s_matrix_formulaall_routes_are_semantically_realizableroute_semantic_realization_is_exhaustive
Source-map audit theorems (16)
argument_wellFormedargument_auditableroutes_wellFormedroutes_have_exact_predecessor_graphcalculation_and_interpretation_contracts_have_no_source_predecessorsdependent_result_steps_apply_exact_semantic_inputsmixed_expansion_retains_controlled_regime_and_deferred_scalinglarge_length_ms_restriction_retains_scope_and_calculationfit_validity_retains_author_expectationfit_validity_uses_expected_couplings_and_interpretive_bridgefit_c0_d2_meaning_depends_on_combination_scopehigh_momentum_warning_retains_approximation_assessmentweinberg_failure_depends_on_required_same_order_d2scale_cancellation_depends_on_pion_inclusive_rg_controlcoupled_predictions_retain_deferred_and_mixed_order_statuscoupled_zero_phases_depend_on_displayed_s_matrix_formula
Semantic atoms (63)
pionlessPDSSetuppdsLoopCalculationbubbleResummationCalculationpionlessUnitarityCalculationpdsLoopIntegralpdsLoopFormulapdsAmplitudepdsAmplitudeFormulaunitaryAmplitudeeffectiveRangeMatchingphysicalScaleIndependenceRequirementpionlessRGCalculationexactC0C2BetaFunctionsc0C2PionlessRGControlfullAmplitudeScaleIndependentnaturalMSSetuplargeLengthMSSetupnaturalMSPowerCountingCalculationlargeLengthMSRestrictionCalculationnaturalMSCountingValidlargeLengthMSValidityRequiresInverseLengthWindowlargeLengthMSRangeRestrictedlargeLengthScalingSetuplargeLengthPowerCountingCalculationmixedKSWExpansionkswAmplitudeExpansionresummedNonuniformPowerCountingpionScaleSetupexplicitPionSubleadingCalculationpotentialPionAtSubleadingOrderradiationPionsAbsentAtSubleadingOrderlogarithmicSubleadingScaleDependenced2CountertermRequiredd2NotSubdominantToOnePionExchangepionInclusiveRGControlledCouplingssubleadingAmplitudeCompleteweinbergCountingFailurescaleCancellationCalculationfullPionAmplitudeScaleIndependenttruncatedScaleIndependentThroughSubleadingresidualScaleDependenceHigherOrdersingletFitSetupsingletFitCalculationfittedCouplingsHaveExpectedScalingc0D2CombinationControlsSubleadingAmplitudec0D2CombinationInterpretationindividualC0D2FitValuesNotSeparatelyMeaningfulgoodSingletPhaseShiftAgreementfitValidityExpectationfitSuggestsExpansionValiditylargeSubleadingLeadingRatiohighMomentumTruncationAssessmentneglectedQuadraticTermsControlledcoupledChannelSetupcoupledChannelCalculationcoupledSMatrixFormulaleadingCoupledAmplitudeOnlySComponentleadingMixingAndDWavePhasesZerosubleadingSPhaseCalculatedmixingAndDWaveOnlyLeadingOrderanalyticSubleadingCoupledFormulaDeferredcoupledSPhaseFittedmixingAndDWaveParameterFreeAtDeclaredOrder
Claim identifiers (63)
pdsSetuploopCalculationresummationCalculationunitarityCalculationloopIntegralloopFormulaamplitudeamplitudeFormulaunitarityrangeMatchingscaleRequirementrgCalculationbetaFunctionsc0C2RGControlfullScaleIndependencenaturalMSRegimelargeLengthMSRegimenaturalMSCalculationlargeLengthMSCalculationnaturalMSValiditylargeLengthMSWindowlargeLengthMSRestrictionscalingSetupscalingCalculationmixedExpansionamplitudeExpansionsharedPowerCountingpionSetuppionCalculationpotentialPionradiationPionAbsencelogarithmicScaleDependenced2Requiredd2UnsuppressedpionInclusiveRGControlsubleadingCompleteweinbergFailurescaleCalculationfullPionScaleIndependencetruncatedScaleIndependencehigherOrderResidualfitSetupfitCalculationexpectedCouplingsc0D2Combinationc0D2Interpretationc0D2IndividualMeaningphaseAgreementvalidityExpectationvaliditySuggestionlargeRatiotruncationAssessmentuncontrolledNeglectedTermscoupledSetupcoupledCalculationcoupledSMatrixFormulaleadingSOnlyzeroMixingAndDWavesubleadingSPhasemixedObservableOrdersdeferredCoupledFormulafittedSPhaseparameterFreePredictions
Step identifiers (63)
statePDSSetupstateLoopCalculationstateResummationCalculationstateUnitarityCalculationderiveLoopIntegralretainPDSLoopFormuladerivePDSAmplituderetainPDSAmplitudeFormuladeriveUnitaritystateEffectiveRangeMatchingimposePhysicalScaleIndependencestateRGCalculationderiveBetaFunctionsderiveC0C2RGControlderiveFullScaleIndependencestateNaturalMSRegimestateLargeLengthMSRegimestateNaturalMSCalculationstateLargeLengthMSCalculationderiveNaturalMSValidityderiveLargeLengthMSWindowderiveLargeLengthMSRestrictionstateScalingSetupstateScalingCalculationderiveMixedExpansionderiveAmplitudeExpansionrealizeSharedPowerCountingstatePionSetupstatePionCalculationderivePotentialPionOrderderiveRadiationPionAbsencederiveLogarithmicDependencerequireD2CountertermderiveD2UnsuppressedderivePionInclusiveRGControlderiveSubleadingCompletenessexcludeWeinbergCountingstateScaleCancellationderiveFullPionScaleIndependencederiveTruncatedScaleIndependencederiveHigherOrderResidualstateFitSetupstateFitCalculationderiveExpectedCouplingsderiveC0D2CombinationstateC0D2CombinationInterpretationinterpretC0D2IndividualValuesderivePhaseAgreementstateValidityExpectationinferValiditySuggestionderiveLargeRatiostateTruncationAssessmentexcludeControlledNeglectedTermsstateCoupledSetupstateCoupledCalculationretainCoupledSMatrixFormuladeriveLeadingSOnlyderiveZeroMixingAndDWavederiveSubleadingSPhaserecordMixedObservableOrdersrecordDeferredCoupledFormularecordCoupledSFitderiveParameterFreePredictions
Route identifiers (7)
pionlessPDSminimalSubtractionScopelargeLengthPowerCountingexplicitPionsscaleCancellationsingletFitcoupledChannel
Route kinds (7)
exactPionlessConstructionminimalSubtractionScopeContrastmixedPowerCountingsubleadingPionCalculationrenormalizationScaleAccountingempiricalFitWithValidityWarningmixedOrderCoupledPrediction
Checked source-route details
This ledger is generated from the elaborated Lean route records. It lists direct predecessors, ordered inference steps, and exported claims. The independent fidelity audit checks every field; this ledger does not replace the physical semantics or certify every explanatory diagram.
pionlessPDS
Logical kind: exactPionlessConstruction.
Required predecessor routes: none.
Ordered inference steps: statePDSSetup, stateLoopCalculation, stateResummationCalculation, stateUnitarityCalculation, deriveLoopIntegral, retainPDSLoopFormula, derivePDSAmplitude, retainPDSAmplitudeFormula, deriveUnitarity, stateEffectiveRangeMatching, imposePhysicalScaleIndependence, stateRGCalculation, deriveBetaFunctions, deriveC0C2RGControl, deriveFullScaleIndependence.
Exported conclusions: loopFormula, amplitudeFormula, amplitude, unitarity, betaFunctions, c0C2RGControl, fullScaleIndependence.
minimalSubtractionScope
Logical kind: minimalSubtractionScopeContrast.
Required predecessor routes: none.
Ordered inference steps: stateNaturalMSRegime, stateLargeLengthMSRegime, stateNaturalMSCalculation, stateLargeLengthMSCalculation, deriveNaturalMSValidity, deriveLargeLengthMSWindow, deriveLargeLengthMSRestriction.
Exported conclusions: naturalMSValidity, largeLengthMSWindow, largeLengthMSRestriction.
largeLengthPowerCounting
Logical kind: mixedPowerCounting.
Required predecessor routes: none.
Ordered inference steps: stateScalingSetup, stateScalingCalculation, deriveMixedExpansion, deriveAmplitudeExpansion, realizeSharedPowerCounting.
Exported conclusions: mixedExpansion, amplitudeExpansion, sharedPowerCounting.
explicitPions
Logical kind: subleadingPionCalculation.
Required predecessor routes: largeLengthPowerCounting.
Ordered inference steps: statePionSetup, statePionCalculation, derivePotentialPionOrder, deriveRadiationPionAbsence, deriveLogarithmicDependence, requireD2Counterterm, deriveD2Unsuppressed, derivePionInclusiveRGControl, deriveSubleadingCompleteness, excludeWeinbergCounting.
Exported conclusions: potentialPion, radiationPionAbsence, logarithmicScaleDependence, d2Required, d2Unsuppressed, pionInclusiveRGControl, subleadingComplete, weinbergFailure.
scaleCancellation
Logical kind: renormalizationScaleAccounting.
Required predecessor routes: explicitPions.
Ordered inference steps: stateScaleCancellation, deriveFullPionScaleIndependence, deriveTruncatedScaleIndependence, deriveHigherOrderResidual.
Exported conclusions: fullPionScaleIndependence, truncatedScaleIndependence, higherOrderResidual.
singletFit
Logical kind: empiricalFitWithValidityWarning.
Required predecessor routes: explicitPions.
Ordered inference steps: stateFitSetup, stateFitCalculation, deriveExpectedCouplings, deriveC0D2Combination, stateC0D2CombinationInterpretation, interpretC0D2IndividualValues, derivePhaseAgreement, stateValidityExpectation, inferValiditySuggestion, deriveLargeRatio, stateTruncationAssessment, excludeControlledNeglectedTerms.
Exported conclusions: expectedCouplings, c0D2Combination, c0D2IndividualMeaning, phaseAgreement, validitySuggestion, largeRatio, uncontrolledNeglectedTerms.
coupledChannel
Logical kind: mixedOrderCoupledPrediction.
Required predecessor routes: none.
Ordered inference steps: stateCoupledSetup, stateCoupledCalculation, retainCoupledSMatrixFormula, deriveLeadingSOnly, deriveZeroMixingAndDWave, deriveSubleadingSPhase, recordMixedObservableOrders, recordDeferredCoupledFormula, recordCoupledSFit, deriveParameterFreePredictions.
Exported conclusions: coupledSMatrixFormula, leadingSOnly, zeroMixingAndDWave, subleadingSPhase, mixedObservableOrders, deferredCoupledFormula, parameterFreePredictions.