Formal reconstruction · cubic-lattice spin algebra, imported quasi-local dynamics, local matrix basis, commutator differential inequality, positive analytic Green function, contour shift, state-independent exponential cone, finite information velocity, interaction-tail extensions, crude velocity bounds, quasi-local asymptotic abelianness, G-abelianness, and invariant-state decomposition
The Finite Group Velocity of Quantum Spin Systems
From local equations of motion to an exponential commutator cone—and from that cone to operator-algebraic consequences
Definitions, structures, and assumptions
Structures, classes, and inductive alternatives
- 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.
- inductive
- inductive
- 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
- structureThe proof-free local-interaction and commutator-cone structure selected by one finite-propagation route. It contains no calculation or explanatory proof.
- structure
- structure
- structure
- structure
- inductive
- inductive
- inductive
- structure
- inductive
- structure
- structureA selected claim must depend on exactly these source-map steps.
- structureA selected claim must retain exactly these epistemic statuses.
- structureA selected route must name exactly these immediate predecessor routes.
- structure
- structure
- inductive
- inductive
- structure
- structure
- structure
- structure
- structure
- inductiveTyped token for the original finite-range commutator-cone derivation.
- structure
- structurePaper-local physical vocabulary. It distinguishes the quantum-spin kinematics, interaction assumptions, imported dynamics, local commutator calculation, physical interpretation, quasi-local extension, and representation-theoretic conclusions.
- structure
- structure
- structure
- structure
- structure
- structure
- structure
- structure
- structure
- structure
- structure
- structure
- structureThe numerical data appearing in the paper's cone estimate. The positivity, monotonicity, and commutator estimate are propositions in `PaperFramework`, not proof fields stored here.
- structure
- structure
- structure
- structureThe causal and signalling part of spacetime locality. It is deliberately separate from observable compatibility: a paper may establish one without even supplying semantics for the other.
- structureOperational signal exclusion needs only a spacelike-separation relation and a physically interpreted signal relation. It does not by itself assign a causal reachability relation or a propagation mechanism.
- structure
- structure
- structure
Definitions and domain choices
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definitionAn exact signal-exclusion conclusion requires an additional bridge from an effective commutator cone to an independently specified signalling model. Exponential suppression and finite group velocity do not provide this bridge.
- 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
- 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
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definitionOriginal report p. 9, Remark 1: the displayed two-body decay example.
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- 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 dynamics construction is recalled from Robinson's earlier work. Its exact output is exposed here as an imported theorem hypothesis.
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definitionThe paper states that a refinement of the finite-range proof covers a class of exponentially decreasing infinite-range interactions, but omits the calculation.
- definition
- definitionThe exterior-cone filter is not allowed to become vacuous: for every time scale there is a farther translated point still satisfying `|x| > v |t|`.
- definitionOne point in the original report's exterior cone `|x| > v |t|`. The subtype keeps the asymptotic domain in the formula instead of hiding it in a named "outside cone" predicate.
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definitionRaw source premises for the original report pp. 5-9 derivation. The imported dynamics, one-site reduction, differential inequality, Green-function calculation, contour estimate, physical interpretation, and exact-zero scope remain separate; no established finite-velocity endpoint is stored.
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definitionOriginal report p. 5 theorem: `lim_{|t| -> infinity, |x| > v |t|} exp (mu(v) |t|) ||[tau_t tau_x(A), B]|| = 0` for every `v > V_Phi` and all strictly local `A` and `B`. The selected threshold and decay function remain paper-local readouts. Nonnegativity of the represented displacement and commutator norms, positivity of `mu`, and its decrease above threshold are explicit logical content rather than consequences of field names.
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- 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 local-dynamics model once its setup is available. The Green-function and contour calculation and the finite-velocity conclusion remain in the separate commutator 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
- 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
Source mappings and interpretation choices
- checked statement
- inductive
- definition
- instance
- constructor
- definition
- checked statement
- constructor
- definition
- checked statement
- definition
- constructor
- definition
- checked statement
- constructor
- definition
- checked statement
- constructor
- definition
- checked statement
- constructor
- definition
- checked statement
- definition
- definition
- definition
- constructor
- definition
- checked statement
- constructor
- definition
- checked statement
- constructor
- definition
- checked statement
- constructor
- definition
- checked statement
- constructor
- definition
- checked statement
- constructor
- definition
- checked statement
- constructor
- definition
- checked statement
- constructor
- definition
- checked statement
- constructor
- definition
- checked statement
- constructor
- definition
- checked statement
- constructor
- definition
- checked statement
- constructor
- definition
- checked statement
- constructor
- definition
- checked statement
- constructor
- definition
- checked statement
- constructor
- definition
- checked statement
- constructor
- definition
- checked statement
- constructor
- definition
- checked statement
- constructor
- definition
- checked statement
- constructor
- definition
- checked statement
- constructor
- definition
- checked statement
- constructor
- definition
- checked statement
- constructor
- definition
- checked statement
- constructor
- definition
- checked statement
- constructor
- definition
- checked statement
- constructor
- definition
- checked statement
- constructor
- definition
- checked statement
- 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
- recursor
- definition
- 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
- inductive
- definition
- instance
- constructor
- definition
- checked statement
- constructor
- definition
- checked statement
- definition
- constructor
- definition
- checked statement
- constructor
- definition
- checked statement
- constructor
- definition
- checked statement
- constructor
- definition
- checked statement
- definition
- definition
- definition
- constructor
- definition
- checked statement
- constructor
- definition
- checked statement
- constructor
- definition
- checked statement
- constructor
- definition
- checked statement
- constructor
- definition
- checked statement
- constructor
- definition
- checked statement
- constructor
- definition
- checked statement
- constructor
- definition
- checked statement
- constructor
- definition
- checked statement
- constructor
- definition
- checked statement
- constructor
- definition
- checked statement
- constructor
- definition
- checked statement
- constructor
- definition
- checked statement
- constructor
- definition
- checked statement
- constructor
- definition
- checked statement
- constructor
- definition
- checked statement
- constructor
- definition
- checked statement
- constructor
- definition
- checked statement
- constructor
- definition
- checked statement
- constructor
- definition
- checked statement
- constructor
- definition
- checked statement
- constructor
- definition
- checked statement
- constructor
- definition
- checked statement
- constructor
- definition
- checked statement
- constructor
- definition
- checked statement
- constructor
- definition
- checked statement
- 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
- recursor
- definition
- 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
- inductive
- definition
- instance
- constructor
- definition
- checked statement
- 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
- constructor
- definition
- checked statement
- constructor
- definition
- checked statement
- constructor
- definition
- checked statement
- definition
- definition
- definition
- checked statement
- recursor
- definition
- constructor
- definition
- checked statement
- definition
- constructor
- definition
- checked statement
- constructor
- definition
- checked statement
- definition
- definition
- definition
- definition
- definition
- definition
- checked statement
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- checked statement
- definition
- definition
- definition
- definition
- instance
- checked statement
- checked statement
- instance
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- checked statement
- checked statement
- definition
- inductive
- definition
- instance
- 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
- constructor
- definition
- checked statement
- recursor
- definition
- constructor
- definition
- checked statement
- definition
- constructor
- definition
- checked statement
- inductive
- definition
- instance
- definition
- constructor
- definition
- checked statement
- constructor
- definition
- checked statement
- definition
- definition
- definition
- constructor
- definition
- checked statement
- constructor
- definition
- checked statement
- constructor
- definition
- checked statement
- constructor
- definition
- checked statement
- constructor
- definition
- checked statement
- definition
- definition
- constructor
- definition
- checked statement
- definition
- checked statement
- constructor
- definition
- checked statement
- recursor
- definition
- definition
- structure
- definition
- instance
- checked statement
- checked statement
- checked statementRaw paper-local inputs construct every Lieb-Robinson route in source order.
- definition
- checked statement
- checked statement
- definition
- checked statement
- checked statement
- definition
- checked statement
- definition
- definition
- definition
- definition
- checked statement
- checked statement
- checked statement
- constructor
- definition
- checked statement
- checked statement
- definition
- checked statement
- definition
- definition
- checked statement
- checked statement
- recursor
- definition
- checked statementNo completed route certificate is needed to cover a route identifier.
- checked statement
- checked statement
- inductive
- definition
- instance
- constructor
- definition
- checked statement
- 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
- 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
- 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
- definition
- definition
- checked statement
- checked statement
- checked statement
- definition
- definition
- checked statement
- definition
- checked statement
- checked statement
- definition
- checked statement
- definition
- checked statement
- checked statement
- definition
- 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
- checked statement
- definition
- definition
- checked statement
- definition
- definition
- definition
- definition
- checked statement
- definition
- checked statement
- checked statement
- checked statement
- definition
- checked statement
- definition
- definition
- checked statement
- definition
- checked statement
- checked statement
- checked statement
- checked statement
- checked statement
- checked statement
Checked statements: parameters, hypotheses, and interpretation
- checked statement
- checked statement
- checked statement
- checked statement
- checked statement
- checked statement
- checked statement
- checked statement
- checked statement
- checked statement
- checked statement
- checked statement
- checked statement
- checked statement
- checked statement
- checked statement
- checked statement
- checked statement
- checked statement
- checked statement
- checked statement
- checked statement
- checked statement
- checked statement
- checked statement
- checked statement
- checked statement
- checked statement
- checked statement
- checked statement
- checked statement
- checked statement
- checked statement
- checked statement
- checked statement
- checked statement
- checked statement
- checked statement
- checked statement
- checked statement
- checked statement
- checked statement
- checked statement
- checked statement
- checked statement
- checked statement
- checked statement
- checked statement
- checked statement
- checked statement
- checked statement
- checked statement
- checked statement
- checked statement
- checked statement
- checked statement
- checked statement
- checked statement
- checked statement
- checked statement
- checked statement
- checked statement
- checked statement
- checked statement
- checked statement
- checked statement
- checked statement
- checked statement
- checked statement
- checked statement
- checked statement
- checked statement
- checked statement
- checked statement
- checked statement
- checked statement
- checked statement
- checked statement
- checked statement
- checked statement
- checked statement
- checked statement
- checked statement
- checked statement
- checked statement
- checked statement
- checked statement
- checked statement
- checked statement
- checked statement
- checked statement
- checked statement
- checked statement
- checked statement
- checked statement
- checked statement
- checked statement
- checked statement
- checked statement
- checked statement
- checked statement
- checked statement
- checked statement
- checked statement
- checked statement
- checked statement
- checked statement
- checked statement
- checked statement
- checked statement
- checked statement
- checked statement
- checked statement
- checked statement
- checked statement
- checked statement
- checked statement
- checked statement
- checked statement
- checked statement
- checked statement
- checked statement
- checked statement
- checked statement
- checked statement
- checked statement
- checked statement
- checked statement
- checked statement
- checked statement
- checked statement
- checked statement
- checked statement
- checked statement
- checked statement
- checked statement
- checked statement
- checked statement
- checked statement
- checked statement
- checked statement
- checked statement
- checked statement
- checked statement
- checked statement
- checked statement
- checked statement
- checked statement
- checked statement
- checked statement
- checked statement
- checked statement
- checked statement
- checked statement
- checked statement
- checked statement
- checked statement
- checked statement
- checked statement
- checked statement
- checked statement
- checked statement
- checked statement
- checked statement
- checked statement
- checked statement
- checked statement
- checked statement
- checked statement
- checked statement
- checked statement
- checked statement
- checked statement
- checked statement
- checked statement
- checked statement
- checked 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 finite control tests the locality distinction, not the infinite-lattice theorem.
- checked statement
- checked statement
- checked statement
- checked statement
- checked statement
- checked statement
- checked statement
- checked statement
- checked statement
- checked statement
- checked statement
- checked statement
- checked statement
- checked statement
- checked statement
- checked statement
- checked statement
- checked statement
- checked statement
- checked statement
- checked statement
- checked statement
- checked statement
- checked statement
- checked statement
- checked statement
- checked statement
- checked statement
- checked statement
- checked statement
- checked statement
- checked statement
- checked statement
- checked statement
- checked statement
- checked statement
- checked statement
- checked statement
- checked statement
- checked statement
- checked statement
- checked statement
- checked statement
- checked 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 original report gives exponential exterior-cone suppression, not exact relativistic signal exclusion. The independently inhabited shared countermodel makes the missing implication formally explicit.
- checked statement
- checked statement
- checked statementThe original local-commutator calculation and its finite-information reading directly realize the shared structural explanation. This remains an approximate cone statement, not exact signal exclusion or a universal light speed. Primary-source anchors: original report pp. 5 and 8-9.
- checked statementGround the selected Lieb-Robinson dynamics model from exact retained semantics and the local-dynamics setup, without using the commutator calculation or finite-information-velocity interpretation.
- checked statement
- checked statement
- checked statement
- checked statementThe original report p. 5 selects strictly local observables and states the finite group-velocity theorem; pp. 8-9 derive the positive Green-function and Fourier-contour estimate producing state-independent exterior-cone suppression. Together with the paper's finite-information interpretation, these inputs realize every physical relation in the shared route.
- checked statement
- checked statement
- checked statement
- checked statementExecute the original one-site, differential, Green-function, and contour route directly into the shared model. No paper-level or shared terminal cone result is consumed.
- checked statement
- checked statement
- checked 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 strict-local cone retains the report's actual p. 5 asymptotic formula, not merely a named exponential-suppression predicate.
- checked statement
- checked statement
- checked statement
- checked statement
- checked statement
- checked statement
- checked statement
- checked statement
- checked statement
- checked statement
- checked statement
- checked statement
- checked statement
- checked statement
- checked statement
- checked statement
- checked statement
- checked statement
- checked statement
- checked statement
- checked statement
- checked statement
- checked statement
- checked statement
- checked statement
- checked statement
- 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
- 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
- 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
- recursor
- constructor
- constructor
- constructor
- constructor
- constructor
- constructor
- constructor
- constructor
- constructor
- recursor
- constructor
- constructor
- constructor
- constructor
- constructor
- constructor
- constructor
- constructor
- constructor
- recursor
- constructor
- constructor
- constructor
- recursor
- constructor
- constructor
- constructor
- constructor
- constructor
- constructor
- constructor
- constructor
- constructor
- constructor
- constructor
- constructor
- recursor
- constructor
- constructor
- constructor
- constructor
- constructor
- constructor
- constructor
- constructor
- constructor
- constructor
- constructor
- constructor
- constructor
- 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
- recursor
- constructor
- recursor
- constructor
- recursor
- constructor
- recursor
- constructor
- recursor
- constructor
- recursor
- constructor
- recursor
- constructor
- recursor
- constructor
- constructor
- constructor
- constructor
- constructor
External mathematical declarations
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- 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 statement below comes only from LiebRobinson1972.lean, SourceMap.lean, and Coverage.lean. The earlier dynamics construction, local matrix estimates, differential inequality, Green-function comparison, contour deformation, two tail refinements, invariant-mean lemma, and decomposition theorem remain named proposition-valued inputs. The original report p. 5 asymptotic exterior-cone limit is now value-level Lean content with explicit displacement and commutator-norm readouts, positive decreasing decay rate, nonvacuous outside-cone domain, and Filter.Tendsto limit. No later pointwise prefactor form is substituted for the 1972 theorem.
The commutator cone is the hub of four different downstream questions
One root constructs the finite-range quasi-local time evolution, and its dependent local-commutator route supplies the finite-velocity cone. The exponential-tail and slower-tail remarks are separate roots because they reuse a proof pattern rather than consume the finite-range theorem's result. The velocity assessment and quasi-local route do consume the certified finite-range cone; the latter continues through invariant-state representation theory. The final result conjoins all eight substantive outputs without upgrading any deferred calculation or open question.
| Transition | Status | Retained boundary |
|---|---|---|
| Finite-range setup to quasi-local dynamics | imported result | The earlier dynamics construction is a named theorem input. |
| Local equations to an exponential commutator cone | paper calculation chain | Finite range alone does not supply the estimate. |
| Exponential cone to finite group velocity | physical interpretation | The bound is state independent but neither exact zero nor a universal light speed. |
| Admissible exponential-tail class to a cone | deferred calculation + interpretation | Class membership and defined dynamics are explicit; the refinement is not displayed. |
| Admissible slower-tail class to commutator decay | deferred calculation | The result is tail-linked and nonexponential; the refinement is not displayed. |
| Computed threshold to physical group velocity | crude upper bound | Hierarchy truncations give upper bounds and improvement is proposed, but convergence is not established. |
| Asymptotic abelianness to G-abelianness | imported cone-mean lemma | The mean lemma is not supplied by asymptotic abelianness itself. |
| G-abelianness to unique state decomposition | imported decomposition theorem | The operator-algebra theorem remains an explicit input. |
The propagation estimate begins only after quasi-local dynamics has been imported
The kinematics consist of a cubic lattice, finite-dimensional on-site spaces, finite-region matrix algebras ordered by inclusion, their quasi-local norm completion, and spatial translations acting by automorphisms. The selected interaction is Hermitian, translation invariant, finite range, and gives finite-volume Hamiltonians.
+ Hermitian translation-invariant finite-range interaction.
FiniteRangeDynamicsSetup; report pp. 3–4
(1)
A result recalled from earlier work then supplies strongly continuous time automorphisms, preservation of products and norm, analytic local evolution, and convergence of finite-volume dynamics to quasi-local dynamics.
The cone proof consumes this established dynamics; it does not reconstruct the infinite-system evolution locally.
earlier_dynamics_construction_establishes_quasi_local_time_evolution · quasi_local_dynamics_route_is_semantically_realizedBasis reduction, a differential inequality, and a contour shift build the cone
Choose two strictly local observables and their translated unequal-time commutator. Arbitrary local observables are reduced to products of a finite one-site matrix basis. The equations of motion and finite interaction neighborhood then yield a differential inequality.
→ Green-function domination of the commutator → Fourier-contour exterior-cone estimate. report pp. 5–9; four independently supplied calculation contracts (2)
The contour estimate provides a finite threshold velocity and a decay rate that is positive and decreasing above threshold. The commutator estimate is independent of the state.
v > VΦ, μ(v) positive and decreasing, for all strictly local A and B.
OriginalStrictLocalCommutatorConeFormulaAt; nonvacuous exterior domain; original report p. 5 theorem; asymptotic form retained without a modernized prefactor
(3)
strict_local_cone_retains_original_asymptotic_formula projects the literal asymptotic formula from the established cone. The theorem's force is operator-norm and state independent. exterior_cone_setup_does_not_supply_original_asymptotic_suppression keeps a finite threshold, a strictly faster tested velocity, and an unbounded sequence of exterior-cone points whose scaled commutator remains one, while a separate countermodel keeps zero state expectation with nonzero operator norm.
Finite information velocity is an interpretation with two explicit limits
The paper interprets exponential suppression outside the cone as finite velocity for information propagation. The formal result stores this interpretation alongside, but not inside, the commutator estimate.
The independent local-operation review now derives an operational readout bound from the actual unitary-preparation change U* A(t) U - A(t). A normalized vector provides positivity and a contracting expectation functional. A two-qubit Hamiltonian then exhibits a nonzero but arbitrarily small early-time response under a first-site operation. This diagnostic is not attributed to the paper and does not replace its infinite-lattice estimates or assert relativistic spacelike signalling. Human semantic review remains pending.
⟹ finite information/group velocity,
but not exact commutator zero and not a universal light speed.
EstablishedFiniteGroupVelocity; report pp. 1–5
(4)
The exact-zero limitation is a proposition in the result: exact commutator vanishing outside the cone is not established. The threshold belongs to the selected interaction and bound; the formal countermodel blocks promotion to a universal speed.
Exponential and slower interaction tails have different conclusions
For an unspecified admissible class of Hermitian translation-invariant infinite-range interactions that decrease exponentially and possess the required dynamics, the paper says a simple refinement preserves a finite threshold, positive decreasing rate, and exponential exterior-cone suppression. Exponential decrease alone does not define that class. The calculation is not displayed, so the formal route keeps class membership, setup, refinement contract, direct cone result, interpretation, and omission scope distinct.
⟹ exponential commutator cone ⟹ finite information velocity.
ExponentialTailRefinement; report p. 9
(5)
For a separately qualified class of interactions decreasing more slowly than exponentially, another omitted refinement yields that commutator decrease tracks the interaction tail and is nonexponential. This is a positive physical claim about the decay form, not merely an editorial claim that exponential decay was unproved.
and the decrease is nonexponential.
EstablishedSlowerTailAssessment; report p. 9
(6)
The velocity is computable, deliberately crude, and not known to converge to the true value
The paper classifies its threshold as a crude upper bound and notes that it can be computed for the nearest-neighbor Heisenberg model. Every truncation of the proposed commutator hierarchy gives an upper bound; using the hierarchy to improve the estimate is retained as a proposal rather than a proved monotone sequence.
but convergence to the true group velocity is not established.
VelocityEstimateAssessment; report p. 10
(7)
The Lean semantics therefore does not manufacture a monotone numeric sequence. It stores the truncation-level upper-bound claim, the proposal to improve the estimate, and the open convergence claim separately. A countermodel confirms that crude upper bounds need not converge to the true velocity.
Norm density extends strict-local suppression to quasi-local asymptotic abelianness
The strict-local cone does not automatically cover arbitrary quasi-local observables. The extension route adds two selected quasi-local observables, norm density of strictly local observables in the quasi-local algebra, and norm preservation by time evolution. A norm-approximation calculation then establishes asymptotic abelianness in the exterior cone.
⟹ quasi-local algebra asymptotically abelian in the cone exterior.
QuasiLocalExtensionCalculation; report p. 11
(8)
A formal countermodel blocks the shortcut from the local cone bound to this quasi-local conclusion without the norm-density extension.
An invariant mean compresses the algebra, and a second theorem decomposes invariant states
Choose a spacetime-translation-invariant state, its representation, a unitary implementation of spacetime translations, and the projector onto the invariant subspace. An imported lemma identifies the weak cone mean of the implementing unitaries with that projector.
⟹ compressed observable algebra abelian + quasi-local algebra G-abelian.
ConeMeanCalculation + GAbelianInference; report p. 11
(9)
Asymptotic abelianness alone does not provide the invariant-mean lemma; a formal countermodel records that gap. Finally, an imported decomposition theorem acts on the established G-abelian setup.
⟹ unique barycentric decomposition into extremal invariant states.
InvariantStateDecompositionTheorem; report pp. 11–12
(10)
+ qualified velocity estimate + quasi-local abelianness + G-abelianness + unique state decomposition.
CompleteScopedResult; eight-result conjunction
(11)
Concept guide
Quasi-local dynamics
The imported strongly continuous, product- and norm-preserving time automorphisms and finite-volume limit.
EstablishedFiniteRangeDynamicsStrict-local commutator problem
Two local observables reduced to a one-site matrix basis before the equations-of-motion estimate.
LocalCommutatorSetupGreen-function comparison
The nonnegative analytic adjoint Green function dominating local commutators and enabling the contour shift.
GreenFunctionCalculationState-independent exponential cone
The finite threshold, positive decreasing decay rate, exponential suppression, and independence from the state.
EstablishedStrictLocalCommutatorConeFinite information velocity
The physical interpretation of the cone, with neither exact zero nor universal-speed status.
EstablishedFiniteGroupVelocityInteraction-tail extensions
The deferred exponential-tail refinement and the weaker tail-linked conclusion for slower decay.
EstablishedExponentialTailFiniteVelocityQualified velocity estimate
The computable crude upper bound, truncation-level upper bounds, proposed improvement, and unresolved convergence to the true velocity.
EstablishedQualifiedVelocityEstimateQuasi-local asymptotic abelianness
The norm-density extension from strict-local suppression to the full quasi-local algebra.
EstablishedQuasiLocalAsymptoticAbeliannessG-abelianness
The invariant representation, imported cone mean, abelian compressed algebra, and G-abelian conclusion.
EstablishedGAbeliannessInvariant-state decomposition
The imported consequence giving a unique barycentric decomposition into extremal invariant states.
EstablishedUniqueInvariantStateDecompositionShared commutator-cone model
The reusable local dynamics, spatial separation, decay control, state-independent cone, interpretation, and grounding semantics.
finiteVelocityCommutatorModelComplete route inventory, blocked shortcuts, and provenance
The source map declares nine routes, forty-four claims, and forty-four sourced steps. Coverage interprets every atom, certifies every route, and proves exhaustive realization. The complete scoped result is the declared main conclusion.
| Route | Direct dependencies | Declared outputs | Profile |
|---|---|---|---|
| Quasi-local dynamics | — | Established finite-range time evolution | imported root |
| Local commutator cone | Quasi-local dynamics | Finite group velocity and physical interpretation | calculation + interpretation |
| Exponential-tail extension | Local commutator cone | Exponential cone and finite velocity | deferred calculation |
| Slower-tail assessment | Local commutator cone | Tail-linked, non-exponential result | deferred + qualified |
| Velocity estimate assessment | Local commutator cone | Crude computable bound and open convergence | qualified estimate |
| Quasi-local asymptotic abelianness | Local commutator cone | Exterior-cone asymptotic abelianness | norm-density extension |
| G-abelianness | Quasi-local asymptotic abelianness | Abelian compression and G-abelian algebra | imported mean |
| Invariant-state decomposition | G-abelianness | Unique extremal decomposition | imported theorem |
| Complete scoped result | All eight routes | Eight-result conjunction | formal main route |
Dynamics · quasi_local_dynamics_route_is_semantically_realized
Local cone · local_commutator_cone_route_is_semantically_realized
Exponential tails · exponential_tail_extension_route_is_semantically_realized
Slower tails · slower_tail_assessment_route_is_semantically_realized
Velocity assessment · velocity_estimate_assessment_route_is_semantically_realized
Quasi-local extension · quasi_local_asymptotic_abelianness_route_is_semantically_realized
G-abelianness · g_abelianness_route_is_semantically_realized
State decomposition · invariant_state_decomposition_route_is_semantically_realized
Complete result · complete_scoped_result_route_is_semantically_realized
Eleven value-level countermodels
| Available fact | Conclusion not supplied | Lean witness |
|---|---|---|
| Unbounded exterior-cone sequence with scaled commutator equal to one | Original asymptotic suppression | exterior_cone_setup_does_not_supply_original_asymptotic_suppression |
| Interaction terms vanishing beyond a positive finite range | Commutator estimate | finite_range_assumption_does_not_supply_commutator_estimate |
| Positive exponentially suppressed commutator | Exact zero outside the cone | exponentially_small_commutator_is_not_exact_zero |
| Two distinct finite interaction velocities | Universal light speed | finite_group_velocity_is_not_a_universal_light_speed |
| Zero state expectation with nonzero operator norm | State-independent operator-norm bound | state_level_weak_correlation_does_not_supply_operator_norm_bound |
| Strict-local bound with uniformly positive approximation error | Quasi-local extension | local_cone_bound_does_not_supply_quasi_local_extension |
| Exponential interaction tail with nonzero class residual | Refinement-class membership | exponential_tail_does_not_supply_refinement_class_membership |
| Inverse-distance interaction tail with nonzero class residual | Slower-tail refinement-class membership | slower_tail_does_not_supply_refinement_class_membership |
| Deferred implication with failed class/dynamics setup | Direct cone result | deferred_tail_contract_without_setup_has_no_direct_cone_result |
| Vanishing asymptotic commutator with nonzero mean residual | Invariant cone-mean lemma | asymptotic_abelianness_does_not_supply_invariant_mean_lemma |
| Strictly improving upper bounds with a positive asymptotic gap | Convergence to the true velocity | crude_upper_bounds_need_not_converge_to_true_velocity |
Epistemic-status audits
dynamics_result_retains_imported_status, finite_velocity_result_retains_interpretive_status, exponential_tail_result_retains_deferred_and_interpretive_status, slower_tail_result_retains_deferred_status, qualified_velocity_result_retains_open_status, g_abelian_result_retains_imported_mean_status, decomposition_result_retains_imported_status, and complete_result_retains_deferred_interpretive_and_open_scope prevent any downstream route from erasing its imported, deferred, interpretive, or open dependencies.
Machine-checked audit boundary
argument_wellFormed, argument_auditable, and routes_wellFormed certify graph structure. Exact-graph, independent-contract, local-result-consumption, tail-route, and transitive-predecessor theorems guard the source order. every_source_claim_has_semantics covers all forty-four claims, and route_semantic_realization_is_exhaustive covers all nine routes. The strict-local result separately realizes and grounds the shared finite-velocity commutator model and transfers every shared claim.
Lean-encoded bibliographic record
E. H. Lieb and D. W. Robinson, The Finite Group Velocity of Quantum Spin Systems, Centre de Physique Théorique report 72/P.457 (April 1972); Communications in Mathematical Physics 28 (1972), 251–257.
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 (105)
euclidean_vector_injectiveeuclidean_vector_zeroeuclidean_vector_sublength_zerolength_eq_zero_ifflength_nonnegativesingle_axis_lengthlengths_are_unboundedexterior_domain_is_nonvacuouszero_dimensional_lengths_vanishzero_dimensional_lattice_has_no_positive_velocity_exteriorsite_distance_is_coordinate_lengthsingleton_support_distancepositive_support_distance_implies_disjointtranslate_site_coordinatestranslate_site_zerotranslate_site_addtranslate_site_neg_canceltranslated_site_mem_translated_supporttranslate_support_addtranslate_support_zerotranslate_support_neg_canceltranslate_operator_zerotranslate_operator_addtranslation_preserves_nonzero_interactiontranslated_interaction_neighborhoodfinite_origin_range_is_uniformfinite_volume_hamiltonian_is_translation_covariantfinite_volume_evolution_is_translation_covariantactual_finite_volume_limit_derives_spacetime_covarianceactual_site_translationactual_support_translationactual_operator_translationactual_originactual_coordinate_lengthshifted_support_cardshifted_support_pairshifted_support_cancelshifted_support_diameternearest_neighbor_pair_is_translation_invariantnearest_neighbor_interaction_is_translation_invariantexponential_pair_interaction_is_translation_invariantscalar_interactions_are_local_selfadjointnearest_neighbor_origin_neighborhoodnearest_neighbor_has_source_finite_rangeexponential_pair_origin_neighborhoodexponential_pair_has_infinite_rangeexponential_pair_has_original_two_body_decayoriginal_exponential_decay_does_not_imply_finite_rangeorigin_blind_interaction_has_empty_origin_neighborhoodorigin_blind_interaction_has_source_origin_finite_rangeorigin_blind_interaction_has_infinite_range_at_oneorigin_blind_interaction_is_not_translation_invariantfinite_origin_range_without_translation_invariance_is_not_uniformscalar_spatial_action_is_not_faithfullawful_spatial_action_need_not_be_faithfulzero_dimensional_coordinates_do_not_supply_unbounded_exterioractual_time_automorphisms_preserve_products_and_normactual_translated_commutator_has_state_independent_trivial_boundspin_setup_retains_actual_operator_kinematicsspin_setup_retains_actual_cubic_latticeactual_cubic_lattice_algebras_realize_spin_kinematicsactual_cubic_interaction_realizes_finite_range_setupactual_operator_regularity_realizes_dynamics_constructionestablished_dynamics_retains_actual_operator_realizationestablished_dynamics_derives_actual_spacetime_covarianceearlier_dynamics_construction_establishes_quasi_local_time_evolutionactual_cubic_lattice_has_unbounded_exterior_domainoriginal_asymptotic_formula_from_actual_cubic_latticestrict_local_cone_retains_original_asymptotic_formulastrict_local_cone_retains_actual_operator_dynamicslocal_matrix_estimates_establish_finite_group_velocityfinite_velocity_commutator_model_retains_paper_semanticsfinite_velocity_source_inputs_make_shared_route_applicablefinite_velocity_result_realizes_shared_setupfinite_velocity_result_realizes_shared_calculationfinite_velocity_result_realizes_shared_interpretationfinite_velocity_inputs_make_shared_route_applicablefinite_velocity_inputs_realize_structural_information_propagation_explanationfinite_group_velocity_does_not_supply_exact_signal_exclusion_bridgelocal_commutator_source_inputs_realize_source_structural_information_propagation_explanationfinite_velocity_result_establishes_shared_commutator_conefinite_velocity_result_exhibits_nonvacuous_shared_commutator_conefinite_velocity_model_inputs_establish_shared_groundingfinite_velocity_result_establishes_grounded_shared_commutator_conegrounded_finite_velocity_result_transfers_every_shared_claimexponential_tail_refinement_preserves_finite_velocity_conclusionslower_tail_refinement_yields_tail_linked_not_exponential_controlfinite_velocity_proof_yields_computable_but_crude_upper_boundnorm_density_extends_local_cone_to_quasi_local_asymptotic_abeliannesscone_mean_and_asymptotic_abelianness_establish_g_abeliannessg_abelianness_yields_unique_extremal_invariant_state_decompositionindependent_routes_establish_complete_scoped_resultactual_finite_spin_hamiltonian_does_not_imply_exact_coneexterior_cone_setup_does_not_supply_original_asymptotic_suppressionfinite_range_assumption_does_not_supply_commutator_estimateexponentially_small_commutator_is_not_exact_zerofinite_group_velocity_is_not_a_universal_light_speedstate_level_weak_correlation_does_not_supply_operator_norm_boundlocal_cone_bound_does_not_supply_quasi_local_extensionexponential_tail_does_not_supply_refinement_class_membershipslower_tail_does_not_supply_refinement_class_membershipdeferred_tail_contract_without_setup_has_no_direct_cone_resultasymptotic_abelianness_does_not_supply_invariant_mean_lemmacrude_upper_bounds_need_not_converge_to_true_velocity
Coverage theorems (15)
every_source_claim_has_semanticsquasi_local_dynamics_route_is_semantically_realizedactual_operator_regularity_realizes_source_dynamics_routeactual_cubic_lattice_inputs_realize_source_dynamics_routecertified_dynamics_retains_actual_cubic_latticelocal_commutator_cone_route_is_semantically_realizedexponential_tail_extension_route_is_semantically_realizedslower_tail_assessment_route_is_semantically_realizedvelocity_estimate_assessment_route_is_semantically_realizedquasi_local_asymptotic_abelianness_route_is_semantically_realizedg_abelianness_route_is_semantically_realizedinvariant_state_decomposition_route_is_semantically_realizedcomplete_scoped_result_route_is_semantically_realizedall_routes_are_semantically_realizableroute_semantic_realization_is_exhaustive
Source-map audit theorems (17)
argument_wellFormedargument_auditableroutes_wellFormedroutes_have_exact_predecessor_graphcalculation_contracts_are_independent_hypothesesinterpretation_scope_and_open_inputs_are_independent_hypotheseslocal_calculation_results_consume_selected_inputstail_extensions_apply_qualified_independent_contractsdependent_routes_consume_certified_predecessor_outputsdynamics_result_retains_imported_statusfinite_velocity_result_retains_interpretive_statusexponential_tail_result_retains_deferred_and_interpretive_statusslower_tail_result_retains_deferred_statusqualified_velocity_result_retains_open_statusg_abelian_result_retains_imported_mean_statusdecomposition_result_retains_imported_statuscomplete_result_retains_deferred_interpretive_and_open_scope
Semantic atoms (44)
dynamicsSetupdynamicsConstructiondynamicsResultlocalSetupbasisReductionCalculationbasisReductionResultdifferentialInequalityCalculationdifferentialInequalityResultgreenFunctionCalculationgreenFunctionResultcontourEstimateCalculationcontourEstimateResultlocalConeBoundphysicalInterpretationBridgefiniteInformationVelocityexactZeroScopefiniteGroupVelocityexponentialTailSetupexponentialTailRefinementexponentialTailConeResultexponentialTailInterpretationBridgeexponentialTailVelocityexponentialTailCalculationScopeexponentialTailResultslowerTailSetupslowerTailRefinementslowerTailDecreaseResultslowerTailCalculationScopeslowerTailAssessmentvelocityUpperBoundCalculationvelocityUpperBoundAssessmenthierarchyConvergenceOpenqualifiedVelocityAssessmentquasiLocalSetupquasiLocalCalculationquasiLocalResultinvariantRepresentationSetupconeMeanCalculationgAbelianInferencegAbelianResultdecompositionSetupdecompositionTheoremdecompositionResultcompleteScopedResult
Claim identifiers (44)
dynamicsSetupdynamicsConstructiondynamicsResultlocalSetupbasisReductionCalculationbasisReductionResultdifferentialInequalityCalculationdifferentialInequalityResultgreenFunctionCalculationgreenFunctionResultcontourEstimateCalculationcontourEstimateResultlocalConeBoundphysicalInterpretationBridgefiniteInformationVelocityexactZeroScopefiniteGroupVelocityexponentialTailSetupexponentialTailRefinementexponentialTailConeResultexponentialTailInterpretationBridgeexponentialTailVelocityexponentialTailCalculationScopeexponentialTailResultslowerTailSetupslowerTailRefinementslowerTailDecreaseResultslowerTailCalculationScopeslowerTailAssessmentvelocityUpperBoundCalculationvelocityUpperBoundAssessmenthierarchyConvergenceOpenqualifiedVelocityAssessmentquasiLocalSetupquasiLocalCalculationquasiLocalResultinvariantRepresentationSetupconeMeanCalculationgAbelianInferencegAbelianResultdecompositionSetupdecompositionTheoremdecompositionResultcompleteResult
Step identifiers (44)
stateDynamicsSetupsupplyDynamicsConstructionderiveDynamicsResultstateLocalSetupsupplyBasisReductionCalculationderiveBasisReductionResultsupplyDifferentialInequalityCalculationderiveDifferentialInequalityResultsupplyGreenFunctionCalculationderiveGreenFunctionResultsupplyContourEstimateCalculationderiveContourEstimateResultassembleLocalConeBoundstatePhysicalInterpretationBridgederiveFiniteInformationVelocityrecordExactZeroScopederiveFiniteGroupVelocitystateExponentialTailSetupdeferExponentialTailRefinementderiveExponentialTailConeResultstateExponentialTailInterpretationBridgederiveExponentialTailVelocityrecordExponentialTailCalculationScopederiveExponentialTailResultstateSlowerTailSetupdeferSlowerTailRefinementderiveSlowerTailDecreaseResultrecordSlowerTailCalculationScopederiveSlowerTailAssessmentsupplyVelocityUpperBoundCalculationderiveVelocityUpperBoundAssessmentrecordHierarchyConvergenceOpenderiveQualifiedVelocityAssessmentstateQuasiLocalSetupsupplyQuasiLocalExtensionCalculationderiveQuasiLocalResultstateInvariantRepresentationSetupsupplyConeMeanCalculationsupplyGAbelianInferencederiveGAbelianResultstateDecompositionSetupsupplyDecompositionTheoremderiveDecompositionResultassembleCompleteResult
Route identifiers (9)
quasiLocalDynamicslocalCommutatorConeexponentialTailExtensionslowerTailAssessmentvelocityEstimateAssessmentquasiLocalAsymptoticAbeliannessgAbeliannessinvariantStateDecompositioncompleteScopedResult
Route kinds (9)
importedDynamicsConstructionequationsOfMotionConeEstimatedeferredExponentialTailRefinementqualifiedSlowerTailRefinementcrudeVelocityBoundAssessmentnormDensityExtensioninvariantMeanCompressionextremalStateDecompositioncompletePaperAssessment
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.
quasiLocalDynamics
Logical kind: importedDynamicsConstruction.
Required predecessor routes: none.
Ordered inference steps: stateDynamicsSetup, supplyDynamicsConstruction, deriveDynamicsResult.
Exported conclusions: dynamicsResult.
localCommutatorCone
Logical kind: equationsOfMotionConeEstimate.
Required predecessor routes: quasiLocalDynamics.
Ordered inference steps: stateLocalSetup, supplyBasisReductionCalculation, deriveBasisReductionResult, supplyDifferentialInequalityCalculation, deriveDifferentialInequalityResult, supplyGreenFunctionCalculation, deriveGreenFunctionResult, supplyContourEstimateCalculation, deriveContourEstimateResult, assembleLocalConeBound, statePhysicalInterpretationBridge, deriveFiniteInformationVelocity, recordExactZeroScope, deriveFiniteGroupVelocity.
Exported conclusions: localConeBound, finiteInformationVelocity, finiteGroupVelocity.
exponentialTailExtension
Logical kind: deferredExponentialTailRefinement.
Required predecessor routes: none.
Ordered inference steps: stateExponentialTailSetup, deferExponentialTailRefinement, deriveExponentialTailConeResult, stateExponentialTailInterpretationBridge, deriveExponentialTailVelocity, recordExponentialTailCalculationScope, deriveExponentialTailResult.
Exported conclusions: exponentialTailResult.
slowerTailAssessment
Logical kind: qualifiedSlowerTailRefinement.
Required predecessor routes: none.
Ordered inference steps: stateSlowerTailSetup, deferSlowerTailRefinement, deriveSlowerTailDecreaseResult, recordSlowerTailCalculationScope, deriveSlowerTailAssessment.
Exported conclusions: slowerTailAssessment.
velocityEstimateAssessment
Logical kind: crudeVelocityBoundAssessment.
Required predecessor routes: localCommutatorCone.
Ordered inference steps: supplyVelocityUpperBoundCalculation, deriveVelocityUpperBoundAssessment, recordHierarchyConvergenceOpen, deriveQualifiedVelocityAssessment.
Exported conclusions: qualifiedVelocityAssessment.
quasiLocalAsymptoticAbelianness
Logical kind: normDensityExtension.
Required predecessor routes: localCommutatorCone.
Ordered inference steps: stateQuasiLocalSetup, supplyQuasiLocalExtensionCalculation, deriveQuasiLocalResult.
Exported conclusions: quasiLocalResult.
gAbelianness
Logical kind: invariantMeanCompression.
Required predecessor routes: quasiLocalAsymptoticAbelianness.
Ordered inference steps: stateInvariantRepresentationSetup, supplyConeMeanCalculation, supplyGAbelianInference, deriveGAbelianResult.
Exported conclusions: gAbelianResult.
invariantStateDecomposition
Logical kind: extremalStateDecomposition.
Required predecessor routes: gAbelianness.
Ordered inference steps: stateDecompositionSetup, supplyDecompositionTheorem, deriveDecompositionResult.
Exported conclusions: decompositionResult.
completeScopedResult
Logical kind: completePaperAssessment.
Required predecessor routes: quasiLocalDynamics, localCommutatorCone, exponentialTailExtension, slowerTailAssessment, velocityEstimateAssessment, quasiLocalAsymptoticAbelianness, gAbelianness, invariantStateDecomposition.
Ordered inference steps: assembleCompleteResult.
Exported conclusions: completeResult.