PhysicsLogic · Paper-first editionLean-extracted article 077

Formal reconstruction · Finite propagation, spectral filtering, and clustering

Spectral Gap and Exponential Decay of Correlations

Power-law and exponential propagation bounds, Gaussian frequency filtering, uniform thermodynamic-limit transfer, corrected bosonic clustering, unsubtracted fermionic decay, self-similarity strengthening, U(1) model upgrades, controlled degeneracy growth, and the exact scope of the gap–correlation implication

Original work encoded in Lean: M. B. Hastings and T. Koma Edition: human-readable logical reconstruction
Formal objectPhysicsLogic.Papers.HastingsKoma2006
Physical resultFor local quantum lattice systems, time slicing and iteration over overlapping supports yield state-independent Lieb–Robinson propagation bounds. Power-law interactions produce a finite-velocity interpretation with an algebraic spatial tail; exponentially decaying interactions produce exponential suppression outside an effective cone. Independently, a uniform gap above a possibly degenerate ground sector and a Gaussian negative-frequency filter separate excited-sector and ground-sector contributions. Combining either propagation form with filtering first produces a uniformly controlled corrected-clustering estimate in every admissible finite volume; an explicit bridge transfers that property through the selected thermodynamic-limit ground state. The resulting infinite-volume bosonic correlation decays only after its ground-sector correction is subtracted. The analogous fermionic anticommutator calculation, together with a normalized ground-projection identity, cancels the correction and establishes decay of the unsubtracted fermionic correlation. Finite ground degeneracy plus distant self-similar copies and prior decay removes the bosonic correction as well. Translations realize this mechanism in selected finite-range U(1)-symmetric XXZ or Hubbard models, upgrading an imported stretched-exponential result to exponential decay. A further controlled route allows finite-volume ground degeneracy to grow slowly enough. The proof uses only real-time propagation, does not prove the converse from clustering to a gap, and does not claim raw decay for every gapped bosonic correlation.
Argument architecture9 routes · 45 semantic claims · 3 independent roots for power-law propagation, exponential propagation, and spectral filtering · explicit finite-volume-to-limit transfer inside corrected bosonic clustering · sibling corrected-bosonic and fermionic branches · 3 strengthenings branching from corrected bosonic clustering · complete scoped synthesis · 12 independent fidelity boundaries · 3 shared semantic adapters, with explicit theory/world grounding for propagation and clustering

Definitions, structures, and assumptions

Structures, classes, and inductive alternatives

  • structureThe selected corrected-correlation phenomenon. It retains the ground-sector correction, observable pair, separated supports, and calculated bound without claiming decay for the unsubtracted correlation.
  • structureProof-free physical data selected by one correlation-decay route. The envelope kind and all numerical envelope parameters remain explicit, so a source using an algebraic tail is not silently reclassified as exponential.
  • structure
  • structureThe selected channel constraint paired with one typed paper-local derivation. The source relation is independent of the shared asymptotic endpoint.
  • inductiveThe two genuinely different envelope routes kept by the shared channel contract. This tag selects a proof obligation; it does not identify algebraic and exponential decay.
  • structureThe selected finite-information-propagation phenomenon. Its type omits the observables, regions, and calculated commutator relation that explain it.
  • inductiveThe complete model-local claim family of the shared route.
  • structureShared relational semantics for the repeated interaction-to-commutator-cone inference. The exact interaction class, dynamics construction, estimate, and physical reading are supplied by paper-local adapters.
  • structurePaper-local meanings for the selected model, the theory using it, and the physical system it represents.
  • structureProof-free data for one selected finite-velocity commutator route. The model retains its nine physical indices and exactly the eleven relation families used by the shared inference. It stores no proof that the route is applicable or physically representative.
  • structureProof-free source constraint for one paper-local commutator-cone derivation. It retains an exact selected model, a typed derivation token, and the token's paper-local realization relation, but no proof that the derivation obtains and no calculated cone or finite-velocity output.
  • structure
  • structure
  • structureTyped gapped-local structure used by one complete clustering calculation. The calculated correlation bound is excluded because it belongs to the explained phenomenon rather than the constraining setup.
  • structure
  • structureThe proof-free local-interaction and commutator-cone structure selected by one finite-propagation route. It contains no calculation or explanatory proof.
  • structureFinite-volume spectral data; the selected band need not be exactly degenerate.
  • structure
  • structure
  • structure
  • inductiveThe complete model-local claim family of the shared route.
  • structureRelational semantics shared by the two independent clustering arguments. The paper-local adapter decides what the ground sector, subtraction, gap, propagation estimate, filtering calculation, and correlation bound mean.
  • structure
  • structureProof-free data selected by one spectral-gap clustering argument. The model retains its fifteen physical indices and exactly the sixteen relation families used by the shared inference. It stores no proof that the route is applicable or physically representative.
  • structure
  • structure
  • structureThe branch-independent physical phenomenon: one explicitly selected, nonvacuous correlation channel is suppressed at large separation. No claim about a full, raw, or otherwise unrelated correlator is stored here.
  • 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
  • structureOriginal v3 pp. 5-6, equations (3.2)-(3.4), as a scalar profile of the corrected bosonic clustering theorem. The selected value is identified below with an actual weak-star ground-state correlation. The remaining profile is an analytic envelope; it does not assert that every positive real distance is realized by a pair of lattice supports.
  • structure
  • structure
  • structure
  • structure
  • structure
  • structure
  • inductiveThe exponential support-chain to finite-volume corrected-boson join.
  • inductiveTyped token for the corrected bosonic clustering derivation.
  • inductiveTyped token for the printed corrected-bosonic correlation formula. This is narrower than the full Gaussian-filter and finite-volume clustering derivation below.
  • inductive
  • inductiveTyped token for the exponential support-chain propagation derivation.
  • inductive
  • inductive
  • structure
  • inductive
  • structure
  • inductive
  • structure
  • structurePaper-local physical vocabulary. The fields are data and predicates only; none carries a proof of a desired conclusion.
  • structure
  • structure
  • structure
  • structure
  • structure
  • structure
  • structure
  • structure
  • structure
  • structure
  • structure
  • structure
  • structure
  • structure
  • structure
  • structure
  • structure
  • structure
  • structure

Definitions and domain choices

  • 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 selected route keeps algebraic and exponential envelopes separate while sharing their final channel-suppression phenomenon.
  • definition
  • definition
  • definition
  • definitionBranch-independent direct content of a completed decay claim: the selected channel has a nonzero witness outside the core and tends to zero at long distance.
  • definition
  • definition
  • definitionAlgebraic specialization of the source-sensitive explanation contract.
  • definitionStructural explanation retaining one realized paper-local derivation.
  • definitionExponential specialization of the source-sensitive explanation contract.
  • definition
  • definition
  • definition
  • definition
  • definition
  • definition
  • definition
  • definition
  • definitionThe exact proof-free channel constraint selected by this context.
  • definitionThe selected channel constraint together with one source derivation.
  • definition
  • definition
  • definitionThe selected nonvacuously suppressed channel phenomenon.
  • definitionSource-sensitive structural explanation adds one independently realized paper-local derivation to the same ordinary channel route.
  • definitionOrdinary structural explanation retains the exact selected channel and branch-specific nonvacuous route, without paper-local derivational provenance.
  • definition
  • definition
  • definition
  • definition
  • definition
  • definition
  • definition
  • definition
  • definition
  • definition
  • definition
  • definition
  • definition
  • definition
  • definition
  • definitionThe complete selected local-cone route structurally explains its scoped finite-information-propagation phenomenon.
  • definition
  • definitionSource-sensitive explanation by one typed paper-local cone derivation.
  • definition
  • definition
  • definition
  • definition
  • definition
  • definition
  • definition
  • definition
  • definition
  • definition
  • definition
  • definition
  • definition
  • definition
  • definition
  • definition
  • definition
  • definitionThe unique model fixed by the context's nine selected physical indices.
  • definition
  • definition
  • definition
  • definition
  • definition
  • definition
  • definition
  • definition
  • definition
  • definition
  • definition
  • definition
  • definition
  • definition
  • definition
  • definition
  • definition
  • definition
  • definition
  • definitionThe complete physical content of the shared finite-velocity route, stated directly on a proof-free model. Every retained relation family occurs at the selected physical indices; localization occurs once for each observable and support role.
  • definition
  • definition
  • definition
  • definition
  • definition
  • definition
  • definition
  • definition
  • definition
  • definition
  • definition
  • definition
  • definition
  • definition
  • definition
  • definitionThe exact finite-propagation phenomenon selected by this model.
  • definitionExact proof-free source constraint selected by a model and source token.
  • definitionThe complete typed structural constraint selected by this model.
  • 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
  • definition
  • definition
  • definition
  • definition
  • definition
  • definition
  • definition
  • definition
  • definition
  • definition
  • definition
  • definition
  • definition
  • definition
  • definition
  • definition
  • definition
  • definition
  • definitionThe exact output of a finite-velocity commutator calculation is admissible as the selected real-time propagation input to this exact clustering model.
  • definition
  • definitionSource-sensitive explanation of the selected corrected clustering.
  • definitionThe complete selected clustering route structurally explains its decay.
  • definition
  • definition
  • definition
  • definition
  • definitionDirect physical content of a finite-velocity-supported clustering route. The generic clustering endpoint remains propagation-source agnostic, because a paper may establish its finite-propagation input without first packaging a finite-velocity commutator cone. Nachtergaele-Sims and the exponential Hastings-Koma branch use a stronger source order: the direct nonvacuous cone child, exact established cone route, paper-local bound-admissibility bridge, selected gapped setup, and direct clustering endpoint must all hold together. This prevents the cone from surviving only in theorem ancestry after its bound has been consumed downstream.
  • definition
  • definitionSource-sensitive finite-velocity-supported clustering retains exact selected cone and clustering models, their shared propagation indices, the inhabited composed physical result, independently sourced propagation and clustering histories, and a third paper-local joining derivation.
  • 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 unique model fixed by the context's fifteen selected physical indices.
  • definition
  • definition
  • definition
  • definition
  • definition
  • definition
  • definition
  • definition
  • definition
  • definition
  • definition
  • definition
  • definition
  • definitionStructural-explanation semantics for the complete corrected-clustering route. A candidate satisfies the typed constraint only when the exact selected gapped-local setup and all three paper-local calculations are applicable. The phenomenon retains the specified ground-sector correction, calculated bound, and its decay; a spectral-gap label or decay label alone is insufficient.
  • definition
  • definition
  • definition
  • definition
  • definition
  • definition
  • definition
  • definition
  • definition
  • definition
  • definition
  • definitionDirect physical content of one completed spectral-gap clustering argument. Unlike exact selected-record semantics, this proposition drops model equality while retaining the actual gapped-local setup and all five consumed clustering outputs at one model. The implication-valued paper calculations are derivation contracts, not terminal physical content.
  • 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 selected corrected-correlation decay whose structure is explained.
  • definitionThe complete selected gapped-local constraint as typed data.
  • definitionThe selected gapped-local constraint with one source derivation.
  • definition
  • definition
  • definition
  • definition
  • definition
  • definition
  • definition
  • definition
  • definition
  • definition
  • definition
  • definition
  • definition
  • 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
  • definition
  • definitionThe left-hand side of the corrected bosonic theorem: `omega(A_X B_Y) - 1/2 [omega(A_X P_0 B_Y) + omega(B_Y P_0 A_X)]`.
  • definition
  • definition
  • definitionOriginal v3 p. 6, the exponentially decaying branch of the corrected bosonic theorem.
  • definitionThe selected pair is genuinely separated and lies in the formula's domain. The positive gap, positive bare decay parameters, nonnegative velocity scales, and nonnegative prefactor retain the hypotheses needed to read the printed rates and bounds as physical decay estimates.
  • definitionThe scalar envelope covers every positive separation; physical pairs are realized separately.
  • definition
  • definitionOriginal v3 p. 6, the power-law branch of the corrected bosonic theorem.
  • definitionThe selected interaction class chooses exactly the printed branch that applies to the selected lattice system, while both branch formulas remain explicit paper-local definitions.
  • definition
  • definitionSource-sensitive explanation of the selected corrected bosonic channel, keeping the power-law and exponential formula branches distinct.
  • definitionOriginal v3 p. 5, equation (3.3): `tilde eta = eta / (1 + 2 v_eta / Delta E)` and `tilde mu = mu / (1 + 2 v_mu / Delta E)`.
  • 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 shared channel is the ground-sector-corrected bosonic correlator.
  • 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
  • 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
  • definitionThe source-map bosonic-clustering output retains the reusable established clustering route together with the literal corrected-correlation formula.
  • definition
  • definition
  • definitionThe selected scalar corrected-clustering readout is attached to the exact interaction, ground state, projection, observable pair, supports, gap, propagation bound, and correlation bound used by the paper-local route. The formula remains Hastings-Koma-local rather than entering the shared `SpectralGapClustering` interface.
  • 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
  • definition
  • definition
  • definition
  • definition
  • definition
  • definition
  • definitionThe finite-volume route used in the proof of the infinite-volume bosonic bound. Pointwise finite-volume control, uniformity, and the selected weak-star limit are deliberately separate premises.
  • definition
  • definition
  • definitionRaw source premises for original v3 pp. 1-2, 6, and 18-22. The exponential setup, time-sliced support-chain calculation, chain resummation, explicit bound, and physical velocity interpretation remain separate; no established propagation endpoint is stored.
  • 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
  • definitionThe Hastings-Koma joining source keeps the independently established exponential branch, Gaussian ground-sector filtering, finite-volume uniform transfer, nontrivial bosonic correction, and literal corrected bound.
  • 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
  • definitionInterpret the exact selected exponential-interaction dynamics model once its setup is available. Support-chain iteration and the finite-velocity conclusion remain in the separate propagation route.
  • definition
  • definition
  • definitionInterpret the exact selected gapped-local-system model once its setup is available. Propagation, Gaussian filtering, and corrected bosonic decay remain in the separate clustering route.
  • 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
  • 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
  • definitionUniform finite-volume control does not itself prove that the property is closed under the selected thermodynamic limit. That closure is this bridge.
  • definition
  • definition
  • definition
  • definition
  • definition
  • definition
  • 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

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
  • 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
  • definition
  • 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
  • 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
  • definition
  • constructor
  • definition
  • checked statement
  • 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
  • definition
  • 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
  • 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
  • definition
  • constructor
  • definition
  • checked statement
  • constructor
  • definition
  • checked statement
  • constructor
  • definition
  • checked statement
  • constructor
  • definition
  • checked statement
  • inductive
  • definition
  • instance
  • constructor
  • definition
  • checked statement
  • constructor
  • definition
  • checked statement
  • definition
  • constructor
  • definition
  • checked statement
  • definition
  • definition
  • definition
  • 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
  • definition
  • constructor
  • definition
  • checked statement
  • constructor
  • definition
  • checked statement
  • definition
  • definition
  • definition
  • definition
  • definition
  • checked statement
  • checked statement
  • checked statement
  • definition
  • definition
  • checked statement
  • definition
  • instance
  • checked statement
  • checked statement
  • instance
  • definition
  • definition
  • definition
  • definition
  • definition
  • definition
  • checked statement
  • checked statement
  • definition
  • definition
  • inductive
  • definition
  • instance
  • constructor
  • definition
  • checked statement
  • 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
  • constructor
  • definition
  • checked statement
  • inductive
  • definition
  • instance
  • 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
  • definition
  • definition
  • definition
  • checked statement
  • constructor
  • definition
  • checked statement
  • recursor
  • definition
  • constructor
  • definition
  • checked statement
  • definition
  • structure
  • definition
  • instance
  • checked statement
  • checked statement
  • checked statement
  • checked statement
  • checked statement
  • checked statementThe source-map bosonic-clustering atom retains Hastings-Koma's printed corrected-correlation bound in addition to the generic shared endpoint.
  • checked statement
  • checked statement
  • definition
  • checked statement
  • definition
  • checked statement
  • checked statement
  • checked statement
  • checked statement
  • definition
  • checked statement
  • definition
  • definition
  • definition
  • definition
  • definition
  • checked statement
  • constructor
  • definition
  • checked statement
  • checked statement
  • definition
  • checked statement
  • definition
  • definition
  • checked statement
  • recursor
  • definition
  • checked statement
  • checked statement
  • checked statement
  • checked statement
  • inductive
  • definition
  • instance
  • constructor
  • definition
  • checked statement
  • 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
  • definition
  • definition
  • 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
  • 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
  • definition
  • checked statement
  • checked statement
  • definition
  • checked statement
  • checked statement
  • definition
  • checked statement
  • checked statement
  • definition
  • checked statement
  • checked statement
  • checked statement
  • definition
  • checked statement
  • checked statement
  • definition
  • checked statement
  • definition
  • checked statement
  • definition
  • 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
  • checked statement
  • definition
  • definition
  • definition
  • definition
  • checked statement
  • checked statement
  • checked statement
  • checked statement
  • 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 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 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 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 statementThe full positive formula domain and the printed renormalized decay rates can hold while the selected exponential bound fails: at the selected separation the corrected correlation is one but the claimed prefactor is zero.
  • checked statement
  • checked statement
  • checked statement
  • checked statement
  • checked statement
  • checked statement
  • checked statement
  • checked statement
  • checked statementThe exponential case specializes the source formula to the selected separation. This is a literal use of the printed corrected-correlation inequality, not a projection from a name-only clustering conclusion.
  • checked statement
  • checked statement
  • checked statement
  • checked statement
  • checked statement
  • checked statementThe printed source formula and an independently nonzero selected corrected correlation source-sensitively explain the selected corrected channel. This does not promote the result to unsubtracted bosonic decay.
  • checked statementThe power-law case specializes the source formula to the selected separation.
  • checked 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 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 statement
  • checked statement
  • checked statement
  • checked statement
  • checked statementThe complete Hastings-Koma bosonic route structurally explains its selected corrected correlation decay. This projection covers both admissible propagation branches without identifying power-law and exponential bounds or promoting the corrected result to raw correlation decay.
  • checked statement
  • checked statement
  • checked statementGround the Hastings-Koma gapped-system model from exact retained semantics and its setup, before either propagation calculation, frequency filtering, or corrected bosonic correlation decay is established.
  • checked statement
  • checked statement
  • checked statement
  • checked statement
  • checked statement
  • checked statement
  • checked statement
  • checked statement
  • checked statement
  • checked statement
  • checked statementGround the Hastings-Koma dynamics model from exact retained semantics and the local-dynamics setup, before the propagation calculation or cone interpretation is established.
  • checked statementThe generic Hastings-Koma bosonic route permits either power-law or exponential propagation. When the independently established exponential branch is supplied, its shared commutator cone can be retained as direct upstream content of the completed clustering route; the power-law branch is not silently identified with this stronger endpoint.
  • checked statement
  • checked statement
  • checked statementThe original v3 pp. 18-22 derive the real-time support-chain estimate and its exponentially suppressed, state-independent bound; pp. 1-2, 6, and 18 retain the interpretation as an upper information-propagation velocity. The exponential branch therefore realizes every physical relation in the shared route, while the paper's power-law branch remains separate.
  • checked statement
  • checked statement
  • checked statement
  • checked statement
  • checked statementThe exponential support-chain calculation and its upper information-propagation-velocity interpretation directly realize the shared structural explanation. The power-law branch and spectral-gap clustering remain separate. Primary-source anchors: original v3 pp. 1-2, 6, and 18-22.
  • checked statementExecute the exponential time-slicing and support-chain route directly into the shared model. No established propagation or clustering result is used.
  • checked statementThe stronger source-sensitive result requires the independent exponential propagation source: Hastings-Koma's power-law clustering branch cannot be silently reclassified as finite-velocity exponential clustering.
  • checked statement
  • checked statement
  • checked statement
  • checked statement
  • checked statement
  • checked statement
  • checked statementThe checked paper route preserves the printed corrected-correlation bound beside the shared clustering endpoint.
  • checked 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 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

Axioms and trust boundaries

  • axiom / trust boundary
  • axiom / trust boundary
  • axiom / trust boundary
  • axiom / trust boundary
  • axiom / trust boundary
  • axiom / trust boundary
  • axiom / trust boundary
  • axiom / trust boundary
  • axiom / trust boundary
  • axiom / trust boundary

Constructors, projections, and other meaning dependencies

  • constructor
  • constructor
  • constructor
  • constructor
  • constructor
  • constructor
  • recursor
  • 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
  • recursor
  • 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
  • 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
  • recursor
  • constructor
  • recursor
  • constructor
  • recursor
  • constructor
  • recursor
  • constructor
  • recursor
  • constructor
  • recursor
  • constructor
  • recursor
  • constructor
  • recursor
  • constructor
  • recursor
  • constructor
  • recursor
  • constructor
  • recursor
  • constructor
  • recursor
  • constructor
  • recursor
  • recursor
  • constructor
  • constructor
  • recursor
  • constructor
  • constructor
  • recursor
  • constructor
  • recursor
  • constructor
  • recursor
  • constructor
  • constructor
  • recursor
  • constructor
  • recursor
  • constructor
  • recursor
  • constructor
  • recursor
  • constructor
  • recursor
  • constructor
  • recursor
  • constructor
  • recursor
  • constructor
  • recursor
  • constructor
  • recursor
  • constructor
  • recursor
  • constructor
  • recursor
  • constructor
  • recursor
  • constructor
  • recursor
  • constructor
  • recursor
  • constructor
  • recursor
  • constructor
  • recursor
  • constructor
  • recursor
  • 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
  • external type boundary
  • external type boundary
  • external type boundary
  • external type boundary
  • external type boundary
  • external type boundary
  • external type boundary
  • external type boundary
  • external type boundary
  • external type boundary
  • external type boundary
  • external type boundary
  • external type boundary
  • external type boundary
  • external type boundary
  • external type boundary
  • external type boundary
  • external type boundary
  • external type boundary
  • external type boundary
  • external type boundary
  • external type boundary
  • external type boundary
  • external type boundary
  • external type boundary
  • external type boundary
  • external type boundary
  • external type boundary
  • external type boundary
  • external type boundary
  • external type boundary
  • external type boundary
  • external type boundary
  • external type boundary
  • external type boundary
  • external type boundary
  • external type boundary
  • external type boundary
  • external type boundary
  • external type boundary
  • external type boundary
  • external type boundary
  • external type boundary
  • external type boundary
  • external type boundary
  • external type boundary
  • external type boundary
  • external type boundary
  • external type boundary
  • external type boundary
  • external type boundary
  • external type boundary
  • external type boundary
  • external type boundary
  • external type boundary
  • external type boundary
  • external type boundary
  • external type boundary
  • external type boundary
  • external type boundary
  • external type boundary
  • external type boundary
  • external type boundary
  • external type boundary
  • external type boundary
  • external type boundary
  • external type boundary
  • external type boundary
  • external type boundary
  • external type boundary
  • external type boundary
  • external type boundary
  • external type boundary
  • external type boundary
  • external type boundary
  • external type boundary
  • external type boundary
  • external type boundary
  • external type boundary
  • external type boundary
  • external type boundary
  • external type boundary
  • external type boundary
  • external type boundary
  • external type boundary
  • external type boundary
  • external type boundary
  • external type boundary
  • external type boundary
  • external type boundary
  • external type boundary
  • external type boundary
  • external type boundary
  • external type boundary
  • external type boundary
  • external type boundary
  • external type boundary
  • external type boundary
  • external type boundary
  • external type boundary
  • external type boundary
  • external type boundary
  • external type boundary
  • external type boundary
  • external type boundary
  • external type boundary
  • external type boundary
  • external type boundary
  • external type boundary
  • external type boundary
  • external type boundary
  • external type boundary
  • external type boundary
  • external type boundary
  • external type boundary
  • external type boundary
  • external type boundary
  • external type boundary
  • external type boundary
  • external type boundary
  • external type boundary
  • external type boundary
  • external type boundary
  • external type boundary
  • external type boundary
  • external type boundary
  • external type boundary
  • external type boundary
  • external type boundary
  • external type boundary
  • external type boundary
  • external type boundary
  • external type boundary
  • external type boundary
  • external type boundary
  • external type boundary
  • external type boundary
  • external type boundary
  • external type boundary
  • external type boundary
  • external type boundary
  • external type boundary
  • external type boundary
  • external type boundary
  • external type boundary
  • external type boundary
  • external type boundary
  • external type boundary
  • external type boundary
  • external type boundary
  • external type boundary
  • external type boundary
  • external type boundary
  • external type boundary
  • external type boundary
  • external type boundary
  • external type boundary
  • external type boundary
  • external type boundary
  • external type boundary
  • external type boundary
  • external type boundary
  • external type boundary
  • external type boundary
  • external type boundary
  • external type boundary
  • external type boundary
  • external type boundary
  • external type boundary
  • external type boundary
  • external type boundary
  • external type boundary
  • external type boundary
  • external type boundary
  • external type boundary
  • external type boundary
  • external type boundary
  • external type boundary
  • external type boundary
  • external type boundary
  • external type boundary
  • external type boundary
  • external type boundary
  • external type boundary
  • external type boundary
  • external type boundary
  • external type boundary
  • external type boundary
  • external type boundary
  • external type boundary
  • external type boundary
  • external type boundary
  • external type boundary
  • external type boundary
  • external type boundary
  • external type boundary
  • external type boundary
  • external type boundary
  • external type boundary
  • external type boundary
  • external type boundary
  • external type boundary
  • external type boundary
  • external type boundary
  • external type boundary
  • external type boundary
  • external type boundary
  • external type boundary
  • external type boundary
  • external type boundary
  • external type boundary
  • external type boundary
  • external type boundary
  • external type boundary
  • external type boundary
  • external type boundary
  • external type boundary
  • external type boundary
  • external type boundary
  • external type boundary
  • external type boundary
  • external type boundary
  • external type boundary
  • external type boundary
  • external type boundary
  • external type boundary
  • external type boundary
  • external type boundary
  • external type boundary
  • external type boundary
  • external type boundary
  • external type boundary
  • external type boundary
  • external type boundary

Every physical statement, dependency, and qualifier below comes only from HastingsKoma2006.lean, SourceMap.lean, and Coverage.lean. Support-chain estimates, Gaussian filtering, thermodynamic limits, parameter optimization, matrix arguments, and model-specific decay bounds remain proposition-valued inputs. Equation (4) is the encoded selected scalar component of the original v3 pp. 5–6 corrected bosonic bound; no other unencoded numerical decay formula is introduced.

01

Propagation and filtering are independent; corrected clustering is the junction

Power-law propagation, exponential propagation, and spectral filtering begin independently. The local clustering premise accepts either propagation result, but the source-map certification lists both propagation routes and filtering as declared dependencies. Bosonic and fermionic routes then diverge. Self-similarity, U(1) models, and controlled degeneracy growth branch only from corrected bosonic clustering.

Power-law propagationsupport chains · algebraic tail · finite-velocity interpretation
Exponential propagationsupport chains · exponential outside-cone suppression · finite velocity
Spectral filteringuniform gap · spectral decomposition · Gaussian negative-frequency filter · ground-sector term
Corrected bosonic clusteringreal-time integral · optimized rate · uniform finite-volume estimate · thermodynamic-limit transfer · printed corrected bound
Fermionic decayanticommutator calculation · projection identity · unsubtracted correlation
Self-similarityfinite degeneracy · distant copies · correction vanishes
U(1) model upgradeimported stretched decay · translations · exponential result
Infinite-degeneracy extensioncontrolled finite-volume growth · distant-copy matrix estimate · infinite-volume limit
Complete scoped resultfinite optimized rate · real-time only · no converse · bosonic correction remains necessary in general
Figure 1. Direct dependencies. Corrected bosonic decay is not raw decay, and neither propagation nor a gap supplies the other ingredients.
Epistemic ledger
TransitionStatusQualification
Support-chain bound to information velocityinterpretive inferenceThe commutator estimate is calculated; its velocity is interpreted as an upper information speed.
Gap to frequency separationspectral/filter calculationSpectral decomposition and Gaussian filtering are independent explicit inputs.
Propagation plus filtering to finite-volume controlcalculationThe real-time integral is bounded and the filter parameter optimized before the limit is taken.
Finite-volume control to infinite-volume clusteringuniform limit transferEvery admissible volume must satisfy the corrected estimate, the family must be uniform, and the selected ground state must be its thermodynamic limit.
Corrected to raw fermionic correlationprojection identityA normalized ground-average identity cancels the fermionic correction.
Corrected to raw bosonic correlationself-similarity matrix argumentFinite degeneracy alone is insufficient; distant symmetry copies and prior decay are required.
U(1) example upgradeimported resultEarlier stretched-exponential decay is invoked, then strengthened using translation self-similarity.
Growing degeneracy extensioncontrolled extensionFinite-volume degeneracy must be small relative to volume and satisfy a matrix estimate.
02

One support-chain mechanism yields two spatial decay regimes

The shared setup is a valid local Hamiltonian system on a graph-metric lattice with finite-dimensional local Hilbert spaces and an available fermionic Fock description. Two observables occupy disjoint, metrically separated regions. Time slicing gives a commutator integral inequality, and iteration over overlapping supports converges.

time-sliced commutator inequality + convergent overlapping-support expansion + interaction-decay control → state-independent real-time propagation bound. support-chain calculation shared by the two propagation routes (1)

Under a power-law interaction assumption, controlled chain sums yield a Lieb–Robinson estimate with an algebraic spatial tail. Under an exponential interaction assumption, they yield exponential suppression outside the effective cone. Each selected interaction class is explicit.

power-law interaction → finite-velocity bound with algebraic tail,
exponential interaction → finite-velocity bound with exponential outside-cone suppression. velocity-as-information-speed is an interpretation of the calculated parameter (2)
Two propagation theoremscalculation + physical interpretation

Both theorems retain setup, chain control, calculated bound, state independence, spatial tail, and finite-velocity interpretation.

support_chain_iteration_establishes_power_law_propagation · support_chain_iteration_establishes_exponential_propagation · v3 pp. 18–22
03

A uniform spectral gap enables filtering but does not provide propagation

The filtering setup uses actual finite Hamiltonian and spectral-projection matrices. The selected band lies at the bottom of the spectrum; its width tends to zero, while a positive lower bound on the gap above it is independent of volume. Exact finite-volume degeneracy is not required. Normalized vector states, normalized ground-sector traces, and their projected bilinear weak-star limits remain distinct.

The state-positivity review exposes the shared expectation condition: every a* a has a real nonnegative expectation, not merely a nonnegative real part. A checked projection bound and an independent two-outcome counterexample make the distinction inspectable. The finite vector and ground-average constructions and their weak-limit preservation retain this stronger condition; positivity alone does not identify a physical ground sector. Human semantic review remains pending.

The finite-sector Hamiltonian now supplies an actual unitary generator, and the local restriction intertwines that evolution with the source Hamiltonian. Contractive imaginary time requires an additional nonnegative-energy premise. A checked family with energies 0, 1/(n+1), 2 has a uniform gap and vanishing band splitting, yet its two-dimensional ground-band projection is never its exact finite-volume kernel projection. ground_bands_realize_finite_hamiltonian_dynamics · QuasiDegenerateGroundControl.actual_finite_band_dynamics_do_not_require_exact_kernel · v3 pp. 5–6

uniform gap + ground-state spectral decomposition + Gaussian negative-frequency filter → extracted negative-frequency term + explicitly separated ground-sector contribution. separated local observables; no propagation conclusion follows from the gap alone (3)
Spectral-filtering theoremdecomposition + Gaussian lemma

The theorem certifies the complete filtering setup and all four spectral outputs without importing a Lieb–Robinson estimate.

gaussian_filter_separates_excited_and_ground_sector_terms · v3 pp. 10–12
04

The generic bosonic conclusion is decay after a ground-sector subtraction

For a separated commuting bosonic pair, the setup combines filtering with either established propagation form. The real-time integral is bounded by the propagation estimate, and the filter parameter is optimized against separation and the gap. Those finite-volume estimates do not become an infinite-volume theorem automatically.

The transfer setup selects an exhausting sequence of admissible volumes and actual normalized vectors in their ground bands. The finite corrected correlations satisfy a common bound plus an error tending to zero. Weak-star convergence of both the ordinary and projected terms then proves the limiting inequality in Lean. The analytic estimates remain explicit inputs.

|ω(AXBY) − 1/2 [ω(AXP0BY) + ω(BYP0AX)]|
≤ Const. × { [1 + dist(X,Y)]−η̃ for power-law interactions; exp[−μ̃ dist(X,Y)] for exponential interactions },
η̃ = η / (1 + 2vη/ΔE), μ̃ = μ / (1 + 2vμ/ΔE). literal selected scalar component of the original v3 pp. 5–6 corrected bosonic theorem; raw decay is not established in general (4)

The formula readout keeps the two projection terms separate and chooses the power-law or exponential branch from the selected interaction class. Its domain requires an actual selected separation, positive gap and bare decay parameters, nonnegative velocity scales, and a nonnegative prefactor. The finite-volume transfer remains a separate logical step; the formula is retained beside, rather than substituted for, the shared clustering endpoint.

Uniform transfer and corrected bosonic clusteringreal-time integral + optimization + thermodynamic transfer

The limit theorem first establishes corrected clustering for the selected infinite-volume ground state from pointwise finite-volume control, uniformity, and the limit relation. The strengthened clustering theorem then returns the specified correction, calculated corrected bound, transferred decay, and printed value-level formula.

uniform_finite_volume_bounds_transfer_bosonic_clustering · gap_filter_and_real_time_bound_establish_bosonic_clustering_with_formula · bosonic_clustering_result_retains_printed_bound · v3 pp. 5–7, 10–14, and 17–22
05

The fermionic anticommutator route reaches the unsubtracted correlation

For a separated anticommuting pair, the filtering calculation retains a corrected bound for the chosen vector-state limit and a separate corrected bound for the normalized ground-sector average. Only the latter is combined with the trace identity. A bound for one arbitrary ground vector cannot be substituted for the average's bound.

anticommutator propagation + filtering + corrected ground-average bound + normalized ground-projection identity → decay of the unsubtracted normalized ground-average fermionic correlation. the projection identity, not statistics alone, removes the correction (5)
Fermionic correlation-decay theoremanticommutator calculation + identity bridge

The theorem retains both corrected-state bounds. Trace cyclicity, its bilinear weak-star limit, and the average's corrected estimate give the raw result by a checked deduction.

anticommutator_route_and_projection_identity_yield_fermion_decay · actual_ground_average_correction_derives_fermionic_bridge · v3 pp. 5–6 and 14
06

Three later routes strengthen or transport the corrected bosonic theorem

Finite-degeneracy self-similarity

Finite ground-sector degeneracy is combined with symmetry transformations producing distant Hamiltonian-preserving copies and with prior correlation decay to zero. Linear dependence among ground-sector matrix-element vectors forces the relevant matrix elements to vanish.

finite ground degeneracy + arbitrarily distant symmetry copies + prior decay → ground-sector matrix elements vanish → unsubtracted bosonic correlation decays. self-similarity is additional structure, not a consequence of finite degeneracy (6)

U(1)-symmetric XXZ or Hubbard models

The model route selects a finite-range globally U(1)-symmetric XXZ or Hubbard family below two dimensions, with both observables transforming as U(1) vectors. It imports an earlier stretched-exponential decay result and identifies translations as self-similarity.

imported stretched-exponential decay + translation self-similarity + corrected bosonic clustering → exponential decay for the selected model correlation. model-specific upgrade; the initial decay theorem is imported (7)

Controlled infinite degeneracy

Infinite-volume degeneracy is admitted only through finite-volume control: the ground degeneracy must remain small relative to volume, and distant copies must satisfy a matrix estimate. Those inputs support the controlled infinite-volume extension.

corrected clustering + controlled finite-volume degeneracy growth + distant-copy matrix estimate → infinite-degeneracy clustering extension. finite degeneracy without growth control is insufficient (8)
Three strengthening theoremsmatrix argument · imported model input · controlled limit

Each branch has a distinct extra premise and conclusion; none is folded into generic corrected clustering.

self_similarity_removes_the_ground_sector_correction · imported_uone_decay_and_translation_upgrade_model_correlations · controlled_finite_volume_degeneracy_extends_clustering
07

The theorem is one-way, real-time, and correction-sensitive

The scope assessment asserts a finite optimized exponential rate and says the filtering proof uses only real-time propagation. No complex-time propagation bound is established. Clustering does not imply a spectral gap. Nor does every bosonic correlation in a gapped system decay without the ground-sector correction.

controlled interaction decay + finite propagation + uniform spectral gap + filtering → qualified clustering,
but clustering ⇏ gap, and gap ⇏ raw decay for every bosonic pair. one-way implication with explicit correction and real-time scope (9)
Complete scoped resultnine-part checked conjunction

The complete theorem conjoins both propagation results, filtering, both statistics routes, all three strengthenings, and the five-part scope assessment.

independent_routes_establish_complete_scoped_result
08

Two reusable frameworks retain the dynamical and clustering layers separately

Shared semantic adapters
AdapterPaper-local realizationBoundary retained
Finite-velocity commutator coneEstablished exponential propagationReal-time state-independent cone suppression and velocity interpretation; no spectral filtering.
Uniform thermodynamic-limit transferFinite-volume corrected clustering transported to the selected ground statePointwise validity, uniformity, and the limit relation are distinct premises; the bridge transfers only the stated correlation property.
Spectral-gap clusteringEstablished corrected bosonic clusteringLocal gapped setup, either propagation form, frequency filtering, thermodynamic transfer, explicit correction, and corrected decay.
exponential propagation → shared finite-velocity commutator cone,
pointwise finite-volume clustering + uniformity + selected limit relation → shared infinite-volume correlation property,
gapped setup + admissible propagation + filtering + corrected correlation calculation → shared spectral-gap clustering,
exact selected models + setup-only grounding → every shared claim transfers to theory and world. clustering grounding is established before propagation, filtering, or decay is assumed (10)

The terminal shared commutator-cone result retains the inhabited exponential-dynamics setup, calculated bound, state independence, exterior-cone suppression, and finite information velocity rather than the implication-valued support-chain and interpretation contracts. Shared grounding directly requires the exact selected model and setup, but it remains logically earlier than the propagation calculation.

The exponential route directly realizes exponential_propagation_realizes_structural_information_propagation_explanation. Its typed constraint retains the selected lattice system, interaction, observables, supports, bound, and regime, while its distinct phenomenon retains only finite information propagation. The proof does not consume the established cone, the power-law branch, or clustering.

The source-sensitive route uses exponential_source_inputs_make_shared_commutator_route_applicable and proves exponential_support_chain_source_inputs_realize_source_structural_information_propagation_explanation. Its typed token records the exponential time-slicing and support-chain derivation, separately from the velocity interpretation; the power-law branch and clustering remain outside this provenance claim.

The completed bosonic route also exposes bosonic_clustering_exhibits_nonvacuous_shared_spectral_gap_clustering. Its selected model contains the gapped setup, admissible propagation, Gaussian filtering, ground-sector correction, corrected bound, and decay together as a direct clustering statement rather than only as implication-valued contracts. The terminal shared result stores those realized facts rather than the three implication-valued calculation functions; the paper-local BosonicCorrectedClusteringResult additionally retains the printed corrected-correlation formula without adding it to the shared interface.

That completed route also realizes bosonic_clustering_realizes_structural_corrected_clustering_explanation. The typed constraint contains the gapped-local propagation, filtering, correction, and decay calculation; the explained phenomenon is the distinct corrected-correlation result. The projection does not identify the exponential and power-law propagation mechanisms or imply raw bosonic decay.

The source-sensitive clustering route is stricter. hastingsKomaCorrectedClusteringDerivationObtains realizes gaussianFilteringRealTimePropagationAndFiniteVolumeTransfer only from the pp. 10–14 Gaussian-filter and real-time inputs together with the pp. 17–22 finite-volume setup, transfer, and corrected bosonic calculation. gaussian_filter_and_finite_volume_inputs_realize_source_structural_corrected_clustering_explanation rebuilds that route without consuming the terminal bosonic result, shared clustering endpoint, or ordinary explanation.

The generic bosonic route still permits either propagation branch. When the independently established exponential branch is supplied, exponential_propagation_and_bosonic_clustering_exhibit_nonvacuous_finite_velocity_supported_shared_spectral_gap_clustering additionally retains the direct nonvacuous commutator-cone child, exact cone route, admissibility bridge, gapped setup, and completed clustering together; it does not recast the distinct power-law route as an exponential cone.

Shared realizations, limit bridge, and groundingthree semantic adapters

The exponential route realizes the commutator cone. The finite-volume family realizes the generic thermodynamic-transfer setup and bridge. The corrected bosonic route then realizes the full spectral-gap clustering pattern. The propagation and clustering models retain their separate theory/world grounding theorems.

exponential_propagation_establishes_grounded_shared_commutator_cone · uniform_finite_volume_route_realizes_shared_limit_property · bosonic_clustering_establishes_grounded_shared_clustering · grounded_bosonic_clustering_transfers_every_shared_claim
A

Concept guide

Support-chain propagation

Time-sliced commutator control iterated through overlapping interaction supports.

SupportChainCalculation

Power-law propagation

A state-independent finite-velocity bound retaining an algebraic spatial tail.

EstablishedPowerLawPropagation

Exponential propagation

A state-independent real-time bound exponentially suppressed outside its effective cone.

EstablishedExponentialPropagation

Gaussian spectral filtering

Negative-frequency extraction separating excited-sector response from a ground-sector contribution.

EstablishedSpectralFiltering

Uniform thermodynamic-limit transfer

Passage of corrected clustering from every admissible finite volume to the selected infinite-volume ground state under a volume-uniform bound and explicit limit relation.

EstablishedFiniteVolumeThermodynamicClustering

Corrected bosonic clustering

Decay after subtracting the specified ground-sector projection term, with the selected power-law or exponential printed bound retained.

BosonicCorrectedClusteringResult

Unsubtracted fermionic decay

Anticommutator clustering whose correction is removed by a projection identity.

EstablishedFermionicCorrelationDecay

Self-similarity strengthening

Distant symmetry copies force ground-sector matrix elements to vanish and remove the bosonic correction.

EstablishedSelfSimilarityStrengthening

U(1) model upgrade

Translation self-similarity upgrading imported stretched decay to exponential decay in selected models.

EstablishedUOneModelUpgrade

Controlled degeneracy extension

An infinite-volume extension permitted only under finite-volume growth and matrix-estimate control.

EstablishedInfiniteDegeneracyExtension

One-way clustering scope

Real-time gap-to-correlation reasoning without a converse or universal raw bosonic decay.

PaperScopeAssessment

Shared clustering semantics

Separate reusable models for finite propagation and corrected spectral-gap clustering.

selectedSpectralGapClusteringModel
B

Complete route inventory, formal separations, and provenance

The source map declares nine routes and forty-five claims. Coverage interprets every atom, treats raw paper contracts as premise-free source hypotheses, reconstructs exact named premises for every composed result, certifies every route under explicit and transitive dependencies, and proves semantic realization exhaustive.

Complete route inventory
RouteDirect dependencyOutputProfile
Power-law propagation—Algebraic-tail finite-velocity boundcalculation + interpretation
Exponential propagation—Exponential cone suppressioncalculation + interpretation
Spectral filtering—Excited/ground-sector separationspectral + Gaussian calculations
Corrected bosonic clusteringBoth propagation routes; filteringInfinite-volume decay with ground-sector correction and printed boundreal-time bound + optimization + uniform limit transfer
Fermionic correlation decayBoth propagation routes; filteringUnsubtracted fermionic decayanticommutator + identity
Self-similarity strengtheningCorrected bosonic clusteringUnsubtracted bosonic decaymatrix vanishing
U(1) model upgradeCorrected bosonic clusteringExponential XXZ/Hubbard model decayimported prior theorem + translation
Infinite-degeneracy extensionCorrected bosonic clusteringControlled growing-degeneracy resultcontrolled extension
Complete scoped resultAll eight routesFull conjunction with scopelogical assembly
Power law · power_law_propagation_route_is_semantically_realized
Certifies support-chain iteration, algebraic-tail bound, state independence, and velocity interpretation.
Exponential · exponential_propagation_route_is_semantically_realized
Certifies support-chain iteration, exponential suppression, state independence, and velocity interpretation.
Filtering · spectral_filtering_route_is_semantically_realized
Independently certifies gap setup, decomposition, Gaussian lemma, and separated ground contribution.
Bosonic clustering · bosonic_corrected_clustering_route_is_semantically_realized
Certifies pointwise finite-volume control, uniformity, thermodynamic-limit transfer, and the corrected—not raw—bosonic correlation theorem with its printed bound.
Fermionic decay · fermionic_correlation_decay_route_is_semantically_realized
Certifies corrected calculation, projection identity, and raw fermionic decay.
Self-similarity · self_similarity_strengthening_route_is_semantically_realized
Certifies matrix-element vanishing and removal of the bosonic correction.
U(1) upgrade · uone_model_upgrade_route_is_semantically_realized
Preserves the imported prior decay theorem and model-specific translation argument.
Infinite degeneracy · infinite_degeneracy_extension_route_is_semantically_realized
Certifies the finite-volume matrix estimate and controlled limit.
Complete result · complete_scoped_result_route_is_semantically_realized
Consumes every prior certificate and certifies the full scope-qualified result.

Selected formal non-implications

The summary counts the independent Lean fidelity inventory. This table illustrates selected paper-local or shared-framework witnesses; it does not define that inventory.

Available factConclusion not suppliedLean witness
Positive gap and separated lattice distance with excessive interaction normControlled interaction decayspectral_gap_does_not_supply_interaction_decay
Propagation bound with nonzero filter and ground-sector-separation residualsSpectral filterpropagation_bound_does_not_supply_spectral_filter
Positive corrected-clustering domain, exponential class, and both tilde-rate relationsPrinted corrected-correlation boundcorrected_clustering_domain_and_rates_do_not_supply_printed_bound
Vanishing corrected correlation with nondecaying ground-sector contributionRaw bosonic decaycorrected_bosonic_clustering_does_not_supply_raw_decay
Stretched-exponential correlation at positive separationExponential model upgradestretched_exponential_decay_is_not_the_exponential_upgrade
Finite ground degeneracy q = 2 requiring four distant copies but supplying oneSelf-similarityfinite_ground_degeneracy_does_not_supply_self_similarity
Ground degeneracy q = 4 requiring sixteen copies in volume tenGrowth control for the extensionfinite_volume_degeneracy_without_growth_control_does_not_extend
Exponentially clustered sequence with zero gapSpectral gapexponential_clustering_does_not_imply_a_gap

Machine-checked audit boundary

argument_wellFormed, argument_auditable, routes_wellFormed, and routes_have_exact_predecessor_graph certify graph structure. every_source_claim_has_semantics covers all forty-five claims, and route_semantic_realization_is_exhaustive covers all nine routes. The source-contract audits pin premise-free raw inputs, while the result-step audits pin exact premise lists for propagation, filtering, finite-volume transfer, clustering, late strengthenings, and the complete result. bosonic_clustering_depends_on_thermodynamic_transfer proves that the limit step is a genuine dependency. Other status theorems preserve propagation interpretation, imported U(1) input, controlled degeneracy growth, and their transitive presence in the complete result.

Lean-encoded bibliographic record

M. B. Hastings and T. Koma, Spectral Gap and Exponential Decay of Correlations, arXiv:math-ph/0507008v3; Communications in Mathematical Physics 265 (2006), 781–804.

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 (82)

source_formula_bounds_actual_domainsource_formula_positive_decay_parameterssource_formula_realizes_shared_corrected_correlation_decaynonzero_source_formula_realizes_nonvacuous_corrected_decaynonzero_source_formula_realizes_source_structural_corrected_correlation_decay_explanationsource_formula_suppresses_the_corrected_correlation_channelpower_law_source_formula_bounds_selected_distanceexponential_source_formula_bounds_selected_distancecorrected_clustering_domain_and_rates_do_not_supply_printed_boundvector_limit_is_normalized_positiveaverage_limit_is_normalized_positivefinite_ground_average_projection_identityground_average_limit_projection_identityaverage_corrected_fermionic_bound_is_raw_boundvanishing_finite_volume_error_transfers_bosonic_boundvanishing_finite_volume_error_transfers_average_fermionic_boundground_bands_realize_finite_hamiltonian_dynamicsnonnegative_finite_hamiltonian_realizes_heat_dynamicsactual_finite_band_dynamics_do_not_require_exact_kernelrepresented_profile_is_actual_corrected_correlationdecay_bound_matches_readoutactual_ground_sector_realizes_uniform_gap_setupuniform_gap_setup_retains_actual_ground_sectorsupport_chain_iteration_establishes_power_law_propagationsupport_chain_iteration_establishes_exponential_propagationgaussian_filter_separates_excited_and_ground_sector_termsbosonic_setup_derives_actual_corrected_limitcorrected_formula_derives_actual_bosonic_boundactual_weak_star_semantics_supply_finite_volume_transferfinite_volume_setup_realizes_shared_thermodynamic_transfer_setupfinite_volume_transfer_realizes_shared_uniform_property_bridgeuniform_finite_volume_route_realizes_shared_limit_propertyuniform_finite_volume_bounds_transfer_bosonic_clusteringsource_formula_and_actual_ground_state_supply_bosonic_calculationgap_filter_and_real_time_bound_establish_bosonic_clusteringgap_filter_and_real_time_bound_establish_bosonic_clustering_with_formulabosonic_clustering_result_retains_printed_boundbosonic_clustering_result_retains_shared_correlation_decayfermionic_setup_derives_actual_corrected_limitactual_ground_average_supplies_projection_identityactual_ground_average_correction_derives_fermionic_bridgeanticommutator_route_and_projection_identity_yield_fermion_decayself_similarity_removes_the_ground_sector_correctionimported_uone_decay_and_translation_upgrade_model_correlationscontrolled_finite_volume_degeneracy_extends_clusteringindependent_routes_establish_complete_scoped_resultfinite_velocity_commutator_model_retains_paper_semanticsexponential_source_inputs_make_shared_commutator_route_applicableexponential_propagation_realizes_shared_setupexponential_propagation_realizes_shared_calculationexponential_propagation_realizes_shared_interpretationexponential_propagation_makes_shared_commutator_route_applicableexponential_propagation_realizes_structural_information_propagation_explanationexponential_support_chain_source_inputs_realize_source_structural_information_propagation_explanationexponential_propagation_establishes_shared_commutator_coneexponential_propagation_exhibits_nonvacuous_shared_commutator_routeexponential_dynamics_model_inputs_establish_theory_model_groundingexponential_propagation_establishes_grounded_shared_commutator_conegrounded_exponential_propagation_transfers_every_shared_claimspectral_gap_clustering_model_retains_paper_semanticsexponential_cone_bound_is_admissible_for_shared_clusteringbosonic_clustering_realizes_shared_setupbosonic_clustering_realizes_shared_propagationbosonic_clustering_realizes_shared_filteringbosonic_clustering_realizes_shared_correlation_calculationbosonic_clustering_makes_shared_route_applicablebosonic_clustering_establishes_shared_spectral_gap_clusteringbosonic_clustering_exhibits_nonvacuous_shared_spectral_gap_clusteringbosonic_clustering_realizes_structural_corrected_clustering_explanationgaussian_filter_and_finite_volume_inputs_realize_source_structural_corrected_clustering_explanationexponential_propagation_and_bosonic_clustering_exhibit_nonvacuous_finite_velocity_supported_shared_spectral_gap_clusteringexponential_support_chain_gaussian_filter_and_finite_volume_transfer_realize_source_sensitive_clusteringbosonic_gapped_model_inputs_establish_groundingbosonic_clustering_establishes_grounded_shared_clusteringgrounded_bosonic_clustering_transfers_every_shared_claimspectral_gap_does_not_supply_interaction_decaypropagation_bound_does_not_supply_spectral_filtercorrected_bosonic_clustering_does_not_supply_raw_decaystretched_exponential_decay_is_not_the_exponential_upgradefinite_ground_degeneracy_does_not_supply_self_similarityfinite_volume_degeneracy_without_growth_control_does_not_extendexponential_clustering_does_not_imply_a_gap

Coverage theorems (19)

every_source_claim_has_semanticsbosonic_clustering_atom_retains_printed_boundbosonic_clustering_atom_retains_shared_correlation_decaypower_law_propagation_route_is_semantically_realizedexponential_propagation_route_is_semantically_realizedspectral_filtering_route_is_semantically_realizedbosonic_corrected_clustering_route_is_semantically_realizedfermionic_correlation_decay_route_is_semantically_realizedself_similarity_strengthening_route_is_semantically_realizeduone_model_upgrade_route_is_semantically_realizedinfinite_degeneracy_extension_route_is_semantically_realizedcomplete_scoped_result_route_is_semantically_realizedroute_semantic_realization_is_exhaustiveactual_ground_sector_inputs_realize_source_filtering_routeactual_weak_star_inputs_realize_source_bosonic_routeactual_ground_average_inputs_realize_source_fermionic_routebosonic_clustering_atom_retains_actual_ground_sectorbosonic_clustering_atom_realizes_finite_hamiltonian_dynamicsfermionic_decay_atom_retains_distinct_state_bounds

Source-map audit theorems (16)

argument_wellFormedargument_auditableroutes_wellFormedroutes_have_exact_predecessor_graphpropagation_and_filtering_source_contracts_are_independent_hypothesesclustering_source_contracts_are_independent_hypotheseslate_source_contracts_are_independent_hypothesespropagation_filtering_and_transfer_results_apply_exact_inputsclustering_and_late_results_apply_exact_inputscomplete_result_applies_every_scoped_branchpower_law_propagation_retains_interpretive_statusexponential_propagation_retains_interpretive_statusbosonic_clustering_depends_on_thermodynamic_transferuone_upgrade_retains_imported_statusinfinite_degeneracy_extension_retains_controlled_statuscomplete_result_retains_imported_interpretive_and_controlled_scope

Semantic atoms (45)

powerLawSetuppowerLawSupportChainpowerLawCalculationpowerLawInterpretationpowerLawPropagationexponentialSetupexponentialSupportChainexponentialCalculationpropagationInterpretationexponentialPropagationfilteringSetupspectralDecompositiongaussianFilterLemmafilteringCalculationspectralFilteringbosonicSetuprealTimeIntegraldecayOptimizationfiniteVolumeSetupfiniteVolumeTransferthermodynamicTransferbosonicCalculationbosonicClusteringfermionicSetupfermionicRealTimeIntegralfermionicDecayOptimizationfermionicCalculationprojectionIdentityfermionicBridgefermionicDecayselfSimilaritySetupselfSimilarityMatrixselfSimilarityBridgeselfSimilarityStrengtheninguOneSetupimportedUOneDecaytranslationSelfSimilarityuOneUpgradeCalculationuOneModelUpgradeinfiniteDegeneracySetupinfiniteDegeneracyMatrixinfiniteDegeneracyCalculationinfiniteDegeneracyExtensionpaperScopecompleteScopedResult

Claim identifiers (45)

powerLawSetuppowerLawSupportChainpowerLawCalculationpowerLawInterpretationpowerLawPropagationexponentialSetupexponentialSupportChainexponentialCalculationpropagationInterpretationexponentialPropagationfilteringSetupspectralDecompositiongaussianFilterLemmafilteringCalculationspectralFilteringbosonicSetuprealTimeIntegraldecayOptimizationfiniteVolumeSetupfiniteVolumeTransferthermodynamicTransferbosonicCalculationbosonicClusteringfermionicSetupfermionicRealTimeIntegralfermionicDecayOptimizationfermionicCalculationprojectionIdentityfermionicBridgefermionicDecayselfSimilaritySetupselfSimilarityMatrixselfSimilarityBridgeselfSimilarityStrengtheninguOneSetupimportedUOneDecaytranslationSelfSimilarityuOneUpgradeCalculationuOneModelUpgradeinfiniteDegeneracySetupinfiniteDegeneracyMatrixinfiniteDegeneracyCalculationinfiniteDegeneracyExtensionpaperScopecompleteResult

Step identifiers (45)

statePowerLawSetupsupplyPowerLawSupportChainsupplyPowerLawCalculationsupplyPowerLawInterpretationderivePowerLawPropagationstateExponentialSetupsupplyExponentialSupportChainsupplyExponentialCalculationsupplyPropagationInterpretationderiveExponentialPropagationstateFilteringSetupsupplySpectralDecompositionsupplyGaussianFilterLemmasupplyFilteringCalculationderiveSpectralFilteringstateBosonicSetupsupplyRealTimeIntegralsupplyDecayOptimizationstateFiniteVolumeSetupsupplyFiniteVolumeTransfertransferThermodynamicLimitsupplyBosonicCalculationderiveBosonicClusteringstateFermionicSetupsupplyFermionicRealTimeIntegralsupplyFermionicDecayOptimizationsupplyFermionicCalculationsupplyProjectionIdentitysupplyFermionicBridgederiveFermionicDecaystateSelfSimilaritySetupsupplySelfSimilarityMatrixsupplySelfSimilarityBridgederiveSelfSimilarityStrengtheningstateUOneSetupsupplyImportedUOneDecaysupplyTranslationSelfSimilaritysupplyUOneUpgradeCalculationderiveUOneModelUpgradestateInfiniteDegeneracySetupsupplyInfiniteDegeneracyMatrixsupplyInfiniteDegeneracyCalculationderiveInfiniteDegeneracyExtensionrecordPaperScopeassembleCompleteResult

Route identifiers (9)

powerLawPropagationexponentialPropagationspectralFilteringbosonicCorrectedClusteringfermionicCorrelationDecayselfSimilarityStrengtheninguOneModelUpgradeinfiniteDegeneracyExtensioncompleteScopedResult

Route kinds (9)

powerLawSupportChainIterationexponentialSupportChainIterationgaussianNegativeFrequencyFilteringcorrectedBosonicGapClusteringanticommutatorFermionClusteringselfSimilarityMatrixVanishingimportedUOneApplicationcontrolledDegeneracyExtensioncompletePaperAssessment

R

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.

powerLawPropagation

Logical kind: powerLawSupportChainIteration.

Required predecessor routes: none.

Ordered inference steps: statePowerLawSetup, supplyPowerLawSupportChain, supplyPowerLawCalculation, supplyPowerLawInterpretation, derivePowerLawPropagation.

Exported conclusions: powerLawPropagation, powerLawInterpretation.

exponentialPropagation

Logical kind: exponentialSupportChainIteration.

Required predecessor routes: none.

Ordered inference steps: stateExponentialSetup, supplyExponentialSupportChain, supplyExponentialCalculation, supplyPropagationInterpretation, deriveExponentialPropagation.

Exported conclusions: exponentialPropagation, propagationInterpretation.

spectralFiltering

Logical kind: gaussianNegativeFrequencyFiltering.

Required predecessor routes: none.

Ordered inference steps: stateFilteringSetup, supplySpectralDecomposition, supplyGaussianFilterLemma, supplyFilteringCalculation, deriveSpectralFiltering.

Exported conclusions: spectralFiltering.

bosonicCorrectedClustering

Logical kind: correctedBosonicGapClustering.

Required predecessor routes: powerLawPropagation, exponentialPropagation, spectralFiltering.

Ordered inference steps: stateBosonicSetup, supplyRealTimeIntegral, supplyDecayOptimization, stateFiniteVolumeSetup, supplyFiniteVolumeTransfer, transferThermodynamicLimit, supplyBosonicCalculation, deriveBosonicClustering.

Exported conclusions: bosonicClustering.

fermionicCorrelationDecay

Logical kind: anticommutatorFermionClustering.

Required predecessor routes: powerLawPropagation, exponentialPropagation, spectralFiltering.

Ordered inference steps: stateFermionicSetup, supplyFermionicRealTimeIntegral, supplyFermionicDecayOptimization, supplyFermionicCalculation, supplyProjectionIdentity, supplyFermionicBridge, deriveFermionicDecay.

Exported conclusions: fermionicDecay.

selfSimilarityStrengthening

Logical kind: selfSimilarityMatrixVanishing.

Required predecessor routes: bosonicCorrectedClustering.

Ordered inference steps: stateSelfSimilaritySetup, supplySelfSimilarityMatrix, supplySelfSimilarityBridge, deriveSelfSimilarityStrengthening.

Exported conclusions: selfSimilarityStrengthening.

uOneModelUpgrade

Logical kind: importedUOneApplication.

Required predecessor routes: bosonicCorrectedClustering.

Ordered inference steps: stateUOneSetup, supplyImportedUOneDecay, supplyTranslationSelfSimilarity, supplyUOneUpgradeCalculation, deriveUOneModelUpgrade.

Exported conclusions: uOneModelUpgrade.

infiniteDegeneracyExtension

Logical kind: controlledDegeneracyExtension.

Required predecessor routes: bosonicCorrectedClustering.

Ordered inference steps: stateInfiniteDegeneracySetup, supplyInfiniteDegeneracyMatrix, supplyInfiniteDegeneracyCalculation, deriveInfiniteDegeneracyExtension.

Exported conclusions: infiniteDegeneracyExtension.

completeScopedResult

Logical kind: completePaperAssessment.

Required predecessor routes: powerLawPropagation, exponentialPropagation, spectralFiltering, bosonicCorrectedClustering, fermionicCorrelationDecay, selfSimilarityStrengthening, uOneModelUpgrade, infiniteDegeneracyExtension.

Ordered inference steps: recordPaperScope, assembleCompleteResult.

Exported conclusions: completeResult.