import Mathlib.Analysis.SpecialFunctions.Exp import Mathlib.Analysis.InnerProductSpace.PiL2 import Mathlib.Order.Filter.AtTopBot.Map import Mathlib.Data.Real.Basic import Mathlib.Topology.Instances.Real.Lemmas import Mathlib.Topology.MetricSpace.Bounded import Mathlib.Topology.MetricSpace.IsometricSMul import PhysicsLogic.Framework.FiniteVelocityCommutatorCone /-! # Formal Logic of the Lieb-Robinson Finite-Velocity Paper This module parses Elliott H. Lieb and Derek W. Robinson's 1972 paper *The Finite Group Velocity of Quantum Spin Systems*. The local matrix estimates, differential inequality, Green-function calculation, contour deformation, invariant-mean lemma, and the imported decomposition theorem remain explicit proposition-valued inputs. Lean checks how those inputs establish a state-independent exponential commutator cone, its finite-information-velocity interpretation, the quasi-local extension, `G`-abelianness, and unique decomposition of invariant states. -/ set_option autoImplicit false noncomputable section namespace PhysicsLogic.Papers.LiebRobinson1972 open PhysicsLogic.Framework structure Interaction where label : Nat deriving DecidableEq, Repr structure SpinSystem where label : Nat deriving DecidableEq, Repr structure Observable where label : Nat deriving DecidableEq, Repr structure DynamicsDescription where label : Nat deriving DecidableEq, Repr structure SpatialRegion where label : Nat deriving DecidableEq, Repr section CubicLatticeSemantics set_option backward.isDefEq.respectTransparency false /-! Original report pp. 3-5: cubic-lattice coordinates, support translations, local matrix algebras, translation-covariant interactions, and the finite neighborhood of the origin are actual mathematical objects and predicates. -/ abbrev LatticeDisplacement (dimension : Nat) := Fin dimension → Int namespace LatticeDisplacement def euclideanVector {dimension : Nat} (displacement : LatticeDisplacement dimension) : EuclideanSpace Real (Fin dimension) := WithLp.toLp 2 (fun coordinate => (displacement coordinate : Real)) def length {dimension : Nat} (displacement : LatticeDisplacement dimension) : Real := ‖euclideanVector displacement‖ theorem euclidean_vector_injective {dimension : Nat} : Function.Injective (euclideanVector (dimension := dimension)) := by intro first second equal funext coordinate have entry := congrArg (fun vector : EuclideanSpace Real (Fin dimension) => vector coordinate) equal exact Int.cast_injective (by simpa [euclideanVector] using entry) @[simp] theorem euclidean_vector_zero (dimension : Nat) : euclideanVector (0 : LatticeDisplacement dimension) = 0 := by ext coordinate simp [euclideanVector] theorem euclidean_vector_sub {dimension : Nat} (first second : LatticeDisplacement dimension) : euclideanVector (first - second) = euclideanVector first - euclideanVector second := by ext coordinate simp [euclideanVector] @[simp] theorem length_zero (dimension : Nat) : length (0 : LatticeDisplacement dimension) = 0 := by simp [length] theorem length_eq_zero_iff {dimension : Nat} (displacement : LatticeDisplacement dimension) : length displacement = 0 ↔ displacement = 0 := by rw [length, norm_eq_zero, ← euclidean_vector_zero dimension] exact euclidean_vector_injective.eq_iff theorem length_nonnegative {dimension : Nat} (displacement : LatticeDisplacement dimension) : 0 ≤ length displacement := norm_nonneg _ theorem single_axis_length {dimension : Nat} (coordinate : Fin dimension) (amount : Int) : length (Pi.single coordinate amount) = |(amount : Real)| := by have vector : euclideanVector (Pi.single coordinate amount) = EuclideanSpace.single coordinate (amount : Real) := by ext index simp [euclideanVector, EuclideanSpace.single_apply, Pi.single_apply] rw [length, vector, EuclideanSpace.norm_single, Real.norm_eq_abs] theorem lengths_are_unbounded (dimension : Nat) (positive : 0 < dimension) (bound : Real) : ∃ displacement : LatticeDisplacement dimension, bound < length displacement := by obtain ⟨amount, large⟩ := exists_nat_gt bound refine ⟨Pi.single ⟨0, positive⟩ (amount : Int), ?_⟩ rw [single_axis_length] simpa using large def ExteriorPointAt (dimension : Nat) (velocity : Real) := {point : LatticeDisplacement dimension × Real // velocity * |point.2| < length point.1} theorem exterior_domain_is_nonvacuous (dimension : Nat) (positive : 0 < dimension) (velocity scale : Real) : ∃ point : ExteriorPointAt dimension velocity, scale < |point.1.2| := by let time : Real := |scale| + 1 have timePositive : 0 < time := by dsimp [time]; positivity obtain ⟨displacement, exterior⟩ := lengths_are_unbounded dimension positive (velocity * |time|) refine ⟨⟨(displacement, time), exterior⟩, ?_⟩ change scale < |time| rw [abs_of_pos timePositive] dsimp [time] linarith [le_abs_self scale] theorem zero_dimensional_lengths_vanish (displacement : LatticeDisplacement 0) : length displacement = 0 := by rw [show displacement = 0 from Subsingleton.elim _ _, length_zero] theorem zero_dimensional_lattice_has_no_positive_velocity_exterior (velocity : Real) (nonnegative : 0 ≤ velocity) : IsEmpty (ExteriorPointAt 0 velocity) := by refine ⟨fun point => ?_⟩ have zero : point.1.1 = 0 := Subsingleton.elim _ _ have exterior := point.2 rw [zero, length_zero] at exterior exact (not_lt_of_ge (mul_nonneg nonnegative (abs_nonneg _))) exterior end LatticeDisplacement structure CubicLatticeOperatorGeometry {Interaction Observable Region : Type} (model : QuantumSpinOperatorModel Interaction Observable Region) where dimension : Nat onsiteDimension : Nat siteCoordinates : model.Site ≃ LatticeDisplacement dimension spaceAction : letI := model.operatorAlgebra Multiplicative (LatticeDisplacement dimension) →* (model.Operator ≃⋆ₐ[Complex] model.Operator) namespace CubicLatticeOperatorGeometry variable {Interaction Observable Region : Type} variable {model : QuantumSpinOperatorModel Interaction Observable Region} variable (geometry : CubicLatticeOperatorGeometry model) local instance : CStarAlgebra model.Operator := model.operatorAlgebra abbrev Displacement := LatticeDisplacement geometry.dimension def origin : model.Site := geometry.siteCoordinates.symm 0 def siteMetric : MetricSpace model.Site := MetricSpace.induced (fun site => LatticeDisplacement.euclideanVector (geometry.siteCoordinates site)) (LatticeDisplacement.euclidean_vector_injective.comp geometry.siteCoordinates.injective) inferInstance def siteDistance (first second : model.Site) : Real := letI := geometry.siteMetric dist first second theorem site_distance_is_coordinate_length (first second : model.Site) : geometry.siteDistance first second = LatticeDisplacement.length (geometry.siteCoordinates first - geometry.siteCoordinates second) := by letI := geometry.siteMetric have isometry : Isometry (fun site => LatticeDisplacement.euclideanVector (geometry.siteCoordinates site)) := MetricSpace.isometry_induced _ (LatticeDisplacement.euclidean_vector_injective.comp geometry.siteCoordinates.injective) have sameDistance := isometry.dist_eq first second rw [dist_eq_norm, ← LatticeDisplacement.euclidean_vector_sub] at sameDistance exact sameDistance.symm def supportDistance (first second : Finset model.Site) : Real := by classical exact if inhabited : (first ×ˢ second).Nonempty then (first ×ˢ second).inf' inhabited (fun pair => geometry.siteDistance pair.1 pair.2) else 0 theorem singleton_support_distance (first second : model.Site) : geometry.supportDistance {first} {second} = geometry.siteDistance first second := by classical simp [supportDistance] theorem positive_support_distance_implies_disjoint (first second : Finset model.Site) (positive : 0 < geometry.supportDistance first second) : Disjoint first second := by classical letI := geometry.siteMetric apply Finset.disjoint_left.mpr intro site firstMem secondMem have member : (site, site) ∈ first ×ˢ second := Finset.mem_product.mpr ⟨firstMem, secondMem⟩ have inhabited : (first ×ˢ second).Nonempty := ⟨(site, site), member⟩ have bound := Finset.inf'_le (fun pair : model.Site × model.Site => geometry.siteDistance pair.1 pair.2) member have selfDistance : geometry.siteDistance site site = 0 := by simp [siteDistance] rw [selfDistance] at bound rw [supportDistance, dif_pos inhabited] at positive exact (not_lt_of_ge bound) positive def translateSite (displacement : geometry.Displacement) : model.Site ≃ model.Site := (geometry.siteCoordinates.trans (Equiv.addRight displacement)).trans geometry.siteCoordinates.symm def translateSupport (displacement : geometry.Displacement) : Finset model.Site ≃o Finset model.Site where toEquiv := (geometry.translateSite displacement).finsetCongr map_rel_iff' := by intro first second exact Finset.map_subset_map def translateOperator (displacement : geometry.Displacement) : model.Operator ≃⋆ₐ[Complex] model.Operator := geometry.spaceAction (Multiplicative.ofAdd displacement) @[simp] theorem translate_site_coordinates (displacement : geometry.Displacement) (site : model.Site) : geometry.siteCoordinates (geometry.translateSite displacement site) = geometry.siteCoordinates site + displacement := by simp [translateSite] @[simp] theorem translate_site_zero (site : model.Site) : geometry.translateSite 0 site = site := by apply geometry.siteCoordinates.injective simp theorem translate_site_add (first second : geometry.Displacement) (site : model.Site) : geometry.translateSite (first + second) site = geometry.translateSite second (geometry.translateSite first site) := by apply geometry.siteCoordinates.injective simp [add_assoc] @[simp] theorem translate_site_neg_cancel (displacement : geometry.Displacement) (site : model.Site) : geometry.translateSite (-displacement) (geometry.translateSite displacement site) = site := by rw [← translate_site_add] simp @[simp] theorem translated_site_mem_translated_support (displacement : geometry.Displacement) (site : model.Site) (support : Finset model.Site) : geometry.translateSite displacement site ∈ geometry.translateSupport displacement support ↔ site ∈ support := by change geometry.translateSite displacement site ∈ support.map (geometry.translateSite displacement).toEmbedding ↔ _ simp theorem translate_support_add (first second : geometry.Displacement) (support : Finset model.Site) : geometry.translateSupport (first + second) support = geometry.translateSupport second (geometry.translateSupport first support) := by change support.map (geometry.translateSite (first + second)).toEmbedding = (support.map (geometry.translateSite first).toEmbedding).map (geometry.translateSite second).toEmbedding rw [Finset.map_map] congr 1 ext site exact geometry.translate_site_add first second site @[simp] theorem translate_support_zero (support : Finset model.Site) : geometry.translateSupport 0 support = support := by change support.map (geometry.translateSite 0).toEmbedding = support have identity : geometry.translateSite 0 = Equiv.refl model.Site := by ext site exact geometry.translate_site_zero site rw [identity] simp @[simp] theorem translate_support_neg_cancel (displacement : geometry.Displacement) (support : Finset model.Site) : geometry.translateSupport (-displacement) (geometry.translateSupport displacement support) = support := by rw [← translate_support_add] simp @[simp] theorem translate_operator_zero (observable : model.Operator) : geometry.translateOperator 0 observable = observable := by simp [translateOperator] theorem translate_operator_add (first second : geometry.Displacement) (observable : model.Operator) : geometry.translateOperator (first + second) observable = geometry.translateOperator first (geometry.translateOperator second observable) := by simp [translateOperator, ofAdd_add, map_mul] def FullMatrixLocalAlgebrasAt : Prop := 0 < geometry.onsiteDimension ∧ ∀ support : Finset model.Site, Nonempty ((model.localAlgebra support) ≃⋆ₐ[Complex] Matrix (Fin (geometry.onsiteDimension ^ support.card)) (Fin (geometry.onsiteDimension ^ support.card)) Complex) def LocalAlgebraCovarianceAt : Prop := ∀ (displacement : geometry.Displacement) (support : Finset model.Site), (model.localAlgebra support).map (StarAlgHomClass.toStarAlgHom (geometry.translateOperator displacement)) = model.localAlgebra (geometry.translateSupport displacement support) def FaithfulSpatialActionAt : Prop := Function.Injective geometry.spaceAction def TranslationInvariantAt (interaction : Interaction) : Prop := ∀ (displacement : geometry.Displacement) (support : Finset model.Site), model.interactionTerm interaction (geometry.translateSupport displacement support) = geometry.translateOperator displacement (model.interactionTerm interaction support) def FiniteRangeAt (interaction : Interaction) : Prop := (model.interactionNeighborhood interaction geometry.origin).Finite /-- Original report p. 9, Remark 1: the displayed two-body decay example. -/ def TwoBodyExponentialDecreaseAt [DecidableEq model.Site] (interaction : Interaction) (rate : Real) : Prop := 0 < rate ∧ (∀ support : Finset model.Site, support.card ≠ 2 → model.interactionTerm interaction support = 0) ∧ ∀ site : model.Site, ‖model.interactionTerm interaction {geometry.origin, site}‖ ≤ Real.exp (-rate * LatticeDisplacement.length (geometry.siteCoordinates site)) theorem translation_preserves_nonzero_interaction (interaction : Interaction) (invariant : geometry.TranslationInvariantAt interaction) (displacement : geometry.Displacement) (support : Finset model.Site) : model.interactionTerm interaction (geometry.translateSupport displacement support) ≠ 0 ↔ model.interactionTerm interaction support ≠ 0 := by rw [invariant displacement support] exact not_congr (map_eq_zero_iff (geometry.translateOperator displacement) (geometry.translateOperator displacement).injective) theorem translated_interaction_neighborhood (interaction : Interaction) (invariant : geometry.TranslationInvariantAt interaction) (displacement : geometry.Displacement) (center : model.Site) : model.interactionNeighborhood interaction (geometry.translateSite displacement center) = geometry.translateSite displacement '' model.interactionNeighborhood interaction center := by ext site constructor · rintro ⟨support, centerMem, nonzero, siteMem⟩ refine ⟨geometry.translateSite (-displacement) site, ?_, ?_⟩ · refine ⟨geometry.translateSupport (-displacement) support, ?_, ?_, ?_⟩ · have translated := (geometry.translated_site_mem_translated_support (-displacement) (geometry.translateSite displacement center) support).mpr centerMem simpa using translated · exact (geometry.translation_preserves_nonzero_interaction interaction invariant (-displacement) support).mpr nonzero · exact (geometry.translated_site_mem_translated_support (-displacement) site support).mpr siteMem · simpa using geometry.translate_site_neg_cancel (-displacement) site · rintro ⟨original, ⟨support, centerMem, nonzero, siteMem⟩, rfl⟩ exact ⟨geometry.translateSupport displacement support, (geometry.translated_site_mem_translated_support displacement center support).mpr centerMem, (geometry.translation_preserves_nonzero_interaction interaction invariant displacement support).mpr nonzero, (geometry.translated_site_mem_translated_support displacement original support).mpr siteMem⟩ theorem finite_origin_range_is_uniform (interaction : Interaction) (invariant : geometry.TranslationInvariantAt interaction) (finiteRange : geometry.FiniteRangeAt interaction) (center : model.Site) : (model.interactionNeighborhood interaction center).Finite := by have centerEq : geometry.translateSite (geometry.siteCoordinates center) geometry.origin = center := by apply geometry.siteCoordinates.injective simp [origin] rw [← centerEq, geometry.translated_interaction_neighborhood interaction invariant] exact finiteRange.image _ theorem finite_volume_hamiltonian_is_translation_covariant (interaction : Interaction) (invariant : geometry.TranslationInvariantAt interaction) (displacement : geometry.Displacement) (volume : Finset model.Site) : model.finiteVolumeHamiltonian interaction (geometry.translateSupport displacement volume) = geometry.translateOperator displacement (model.finiteVolumeHamiltonian interaction volume) := by classical unfold QuantumSpinOperatorModel.finiteVolumeHamiltonian rw [map_sum] symm apply Finset.sum_equiv (geometry.translateSupport displacement).toEquiv · intro support simp only [Finset.mem_powerset, OrderIso.coe_toEquiv] exact (geometry.translateSupport displacement).le_iff_le.symm · intro support _ exact (invariant displacement support).symm theorem finite_volume_evolution_is_translation_covariant (interaction : Interaction) (invariant : geometry.TranslationInvariantAt interaction) (displacement : geometry.Displacement) (volume : Finset model.Site) (time : Real) (observable : model.Operator) : geometry.translateOperator displacement (QuantumCommutator.finiteVolumeHeisenberg (model.finiteVolumeHamiltonian interaction volume) time observable) = QuantumCommutator.finiteVolumeHeisenberg (model.finiteVolumeHamiltonian interaction (geometry.translateSupport displacement volume)) time (geometry.translateOperator displacement observable) := by rw [QuantumCommutator.automorphism_maps_finite_volume_heisenberg, ← geometry.finite_volume_hamiltonian_is_translation_covariant interaction invariant] def DynamicsTranslationCovariantAt (interaction : Interaction) : Prop := ∀ (displacement : geometry.Displacement) (time : Real) (observable : model.Operator), geometry.translateOperator displacement (QuantumCommutator.evolve (model.timeEvolution interaction) time observable) = QuantumCommutator.evolve (model.timeEvolution interaction) time (geometry.translateOperator displacement observable) theorem actual_finite_volume_limit_derives_spacetime_covariance (interaction : Interaction) (invariant : geometry.TranslationInvariantAt interaction) (convergence : model.FiniteVolumeConvergenceAt interaction) : geometry.DynamicsTranslationCovariantAt interaction := by intro displacement time observable have translatedLimit := ((StarAlgEquiv.isometry (geometry.translateOperator displacement)).continuous |>.tendsto _).comp (convergence time observable) have translatedVolumes := (convergence time (geometry.translateOperator displacement observable)).comp (geometry.translateSupport displacement).tendsto_atTop have sameFunctions : (fun volume : Finset model.Site => geometry.translateOperator displacement (QuantumCommutator.finiteVolumeHeisenberg (model.finiteVolumeHamiltonian interaction volume) time observable)) = (fun volume : Finset model.Site => QuantumCommutator.finiteVolumeHeisenberg (model.finiteVolumeHamiltonian interaction (geometry.translateSupport displacement volume)) time (geometry.translateOperator displacement observable)) := by funext volume exact geometry.finite_volume_evolution_is_translation_covariant interaction invariant displacement volume time observable have transported : Filter.Tendsto (fun volume : Finset model.Site => QuantumCommutator.finiteVolumeHeisenberg (model.finiteVolumeHamiltonian interaction (geometry.translateSupport displacement volume)) time (geometry.translateOperator displacement observable)) Filter.atTop (nhds (geometry.translateOperator displacement (QuantumCommutator.evolve (model.timeEvolution interaction) time observable))) := by rw [← sameFunctions] exact translatedLimit exact tendsto_nhds_unique transported translatedVolumes end CubicLatticeOperatorGeometry /-! These scalar interactions on the infinite integer lattice test the independence of the original spatial assumptions. Their operator action is not faithful, so they are not witnesses for the complete nontrivial quantum-spin theorem. -/ namespace CubicLatticeControls open PhysicsLogic.Framework open scoped ComplexOrder inductive InteractionProfile where | nearestNeighbor | exponentialPair | originBlindLongRange deriving DecidableEq def shiftedSupport (amount : Int) (support : Finset Int) : Finset Int := support.map (Equiv.addRight amount).toEmbedding def pairDiameter (support : Finset Int) : Real := Metric.diam (support : Set Int) def interactionTerm (profile : InteractionProfile) (support : Finset Int) : Complex := by classical exact match profile with | .nearestNeighbor => if ∃ site : Int, support = {site, site + 1} then 1 else 0 | .exponentialPair => if support.card = 2 then (Real.exp (-pairDiameter support) : Complex) else 0 | .originBlindLongRange => if support.card = 2 ∧ 1 ∈ support ∧ 0 ∉ support then 1 else 0 abbrev scalarModel : QuantumSpinOperatorModel InteractionProfile Complex (Finset Int) where Site := Int Operator := Complex operatorAlgebra := inferInstance sites := id observable := id localAlgebra _ := ⊤ interactionTerm := interactionTerm timeEvolution _ := 1 abbrev geometry : CubicLatticeOperatorGeometry scalarModel where dimension := 1 onsiteDimension := 1 siteCoordinates := (Equiv.funUnique (Fin 1) Int).symm spaceAction := 1 theorem actual_site_translation (displacement : geometry.Displacement) (site : Int) : geometry.translateSite displacement site = site + displacement 0 := by have coordinates := congrArg (fun point : LatticeDisplacement 1 => point 0) (geometry.translate_site_coordinates displacement site) simpa [geometry, Equiv.funUnique] using coordinates theorem actual_support_translation (displacement : geometry.Displacement) (support : Finset Int) : geometry.translateSupport displacement support = shiftedSupport (displacement 0) support := by change support.map (geometry.translateSite displacement).toEmbedding = support.map (Equiv.addRight (displacement 0)).toEmbedding congr 1 theorem actual_operator_translation (displacement : geometry.Displacement) (observable : Complex) : geometry.translateOperator displacement observable = observable := by simp [CubicLatticeOperatorGeometry.translateOperator, geometry] theorem actual_origin : geometry.origin = (0 : Int) := rfl theorem actual_coordinate_length (site : Int) : LatticeDisplacement.length (geometry.siteCoordinates site) = |(site : Real)| := by have coordinate : geometry.siteCoordinates site = Pi.single (0 : Fin 1) site := by ext index have indexZero : index = (0 : Fin 1) := Subsingleton.elim _ _ subst index simp [geometry, Equiv.funUnique] rw [coordinate, LatticeDisplacement.single_axis_length] theorem shifted_support_card (amount : Int) (support : Finset Int) : (shiftedSupport amount support).card = support.card := by simp [shiftedSupport] theorem shifted_support_pair (amount first second : Int) : shiftedSupport amount {first, second} = {first + amount, second + amount} := by simp [shiftedSupport] theorem shifted_support_cancel (amount : Int) (support : Finset Int) : shiftedSupport (-amount) (shiftedSupport amount support) = support := by have cancel : (Equiv.addRight amount).toEmbedding.trans (Equiv.addRight (-amount)).toEmbedding = Function.Embedding.refl Int := by ext site simp simp only [shiftedSupport, Finset.map_map, cancel, Finset.map_refl] theorem shifted_support_diameter (amount : Int) (support : Finset Int) : pairDiameter (shiftedSupport amount support) = pairDiameter support := by unfold pairDiameter shiftedSupport rw [Finset.coe_map] exact (isometry_add_right amount).diam_image _ theorem nearest_neighbor_pair_is_translation_invariant (amount : Int) (support : Finset Int) : (∃ site : Int, shiftedSupport amount support = {site, site + 1}) ↔ ∃ site : Int, support = {site, site + 1} := by constructor · rintro ⟨site, equal⟩ have back := congrArg (shiftedSupport (-amount)) equal rw [shifted_support_cancel, shifted_support_pair] at back refine ⟨site - amount, ?_⟩ simpa only [sub_eq_add_neg, add_assoc, add_comm 1 (-amount)] using back · rintro ⟨site, rfl⟩ refine ⟨site + amount, ?_⟩ rw [shifted_support_pair] rw [show site + 1 + amount = site + amount + 1 by omega] theorem nearest_neighbor_interaction_is_translation_invariant : geometry.TranslationInvariantAt .nearestNeighbor := by classical intro displacement support rw [actual_support_translation, actual_operator_translation] change (if ∃ site : Int, shiftedSupport (displacement 0) support = {site, site + 1} then (1 : Complex) else 0) = (if ∃ site : Int, support = {site, site + 1} then 1 else 0) rw [nearest_neighbor_pair_is_translation_invariant] theorem exponential_pair_interaction_is_translation_invariant : geometry.TranslationInvariantAt .exponentialPair := by intro displacement support rw [actual_support_translation, actual_operator_translation] simp only [scalarModel, interactionTerm, shifted_support_card, shifted_support_diameter] theorem scalar_interactions_are_local_selfadjoint (profile : InteractionProfile) : scalarModel.LocalSelfAdjointInteractionAt profile := by intro support change interactionTerm profile support ∈ (⊤ : StarSubalgebra Complex Complex) ∧ IsSelfAdjoint (interactionTerm profile support) constructor · trivial · cases profile <;> simp only [interactionTerm] <;> split_ifs all_goals first | exact isSelfAdjoint_one | exact isSelfAdjoint_zero | exact Complex.conj_ofReal _ theorem nearest_neighbor_origin_neighborhood : scalarModel.interactionNeighborhood .nearestNeighbor 0 = ({-1, 0, 1} : Set Int) := by ext site constructor · rintro ⟨support, originMem, nonzero, siteMem⟩ change interactionTerm .nearestNeighbor support ≠ 0 at nonzero have pair : ∃ start : Int, support = {start, start + 1} := by by_contra absent simp [interactionTerm, absent] at nonzero obtain ⟨start, rfl⟩ := pair simp only [Finset.mem_insert, Finset.mem_singleton] at originMem siteMem simp only [Set.mem_insert_iff, Set.mem_singleton_iff] omega · intro member simp only [Set.mem_insert_iff, Set.mem_singleton_iff] at member rcases member with rfl | rfl | rfl · refine ⟨{-1, 0}, by simp, ?_, by simp⟩ change interactionTerm .nearestNeighbor {-1, 0} ≠ 0 have pair : ∃ start : Int, ({-1, 0} : Finset Int) = {start, start + 1} := ⟨-1, by norm_num⟩ simp [interactionTerm, pair] · refine ⟨{0, 1}, by simp, ?_, by simp⟩ change interactionTerm .nearestNeighbor {0, 1} ≠ 0 have pair : ∃ start : Int, ({0, 1} : Finset Int) = {start, start + 1} := ⟨0, by norm_num⟩ simp [interactionTerm, pair] · refine ⟨{0, 1}, by simp, ?_, by simp⟩ change interactionTerm .nearestNeighbor {0, 1} ≠ 0 have pair : ∃ start : Int, ({0, 1} : Finset Int) = {start, start + 1} := ⟨0, by norm_num⟩ simp [interactionTerm, pair] theorem nearest_neighbor_has_source_finite_range : geometry.FiniteRangeAt .nearestNeighbor := by rw [CubicLatticeOperatorGeometry.FiniteRangeAt, actual_origin, nearest_neighbor_origin_neighborhood] exact Set.toFinite _ theorem exponential_pair_origin_neighborhood : scalarModel.interactionNeighborhood .exponentialPair 0 = Set.univ := by ext site simp only [Set.mem_univ, iff_true] by_cases zero : site = 0 · subst site refine ⟨{0, 1}, by simp, ?_, by simp⟩ change interactionTerm .exponentialPair {0, 1} ≠ 0 simp [interactionTerm] · refine ⟨{0, site}, by simp, ?_, by simp⟩ change interactionTerm .exponentialPair {0, site} ≠ 0 simp [interactionTerm, Ne.symm zero] theorem exponential_pair_has_infinite_range : ¬ geometry.FiniteRangeAt .exponentialPair := by rw [CubicLatticeOperatorGeometry.FiniteRangeAt, actual_origin, exponential_pair_origin_neighborhood] exact Set.infinite_univ theorem exponential_pair_has_original_two_body_decay : geometry.TwoBodyExponentialDecreaseAt .exponentialPair 1 := by refine ⟨by norm_num, ?_, ?_⟩ · intro support notPair change interactionTerm .exponentialPair support = 0 simp [interactionTerm, notPair] · intro site rw [actual_origin, actual_coordinate_length] change ‖interactionTerm .exponentialPair {0, site}‖ ≤ Real.exp (-1 * |(site : Real)|) by_cases zero : site = 0 · subst site simp [interactionTerm] · have diameter : pairDiameter {0, site} = |(site : Real)| := by simp [pairDiameter, Metric.diam_pair, Int.dist_eq] rw [show interactionTerm .exponentialPair {0, site} = (Real.exp (-|(site : Real)|) : Complex) by simp [interactionTerm, Ne.symm zero, diameter]] simpa only [Complex.norm_real, Real.norm_eq_abs, abs_of_pos (Real.exp_pos _), neg_one_mul] using (le_refl (Real.exp (-|(site : Real)|))) theorem original_exponential_decay_does_not_imply_finite_range : (scalarModel.LocalSelfAdjointInteractionAt .exponentialPair ∧ geometry.TranslationInvariantAt .exponentialPair ∧ geometry.TwoBodyExponentialDecreaseAt .exponentialPair 1) ∧ ¬ geometry.FiniteRangeAt .exponentialPair := ⟨⟨scalar_interactions_are_local_selfadjoint _, exponential_pair_interaction_is_translation_invariant, exponential_pair_has_original_two_body_decay⟩, exponential_pair_has_infinite_range⟩ theorem origin_blind_interaction_has_empty_origin_neighborhood : scalarModel.interactionNeighborhood .originBlindLongRange 0 = ∅ := by ext site simp only [Set.mem_empty_iff_false, iff_false] rintro ⟨support, originMem, nonzero, _siteMem⟩ change interactionTerm .originBlindLongRange support ≠ 0 at nonzero simp [interactionTerm, originMem] at nonzero theorem origin_blind_interaction_has_source_origin_finite_range : geometry.FiniteRangeAt .originBlindLongRange := by rw [CubicLatticeOperatorGeometry.FiniteRangeAt, actual_origin, origin_blind_interaction_has_empty_origin_neighborhood] exact Set.finite_empty theorem origin_blind_interaction_has_infinite_range_at_one : (scalarModel.interactionNeighborhood .originBlindLongRange 1).Infinite := by apply Set.infinite_of_injective_forall_mem (f := fun index : Nat => (index : Int) + 2) · intro first second equal exact Nat.cast_injective (add_right_cancel equal) · intro index have awayZero : (index : Int) + 2 ≠ 0 := by omega have awayOne : (index : Int) + 2 ≠ 1 := by omega refine ⟨{1, (index : Int) + 2}, by simp, ?_, by simp⟩ change interactionTerm .originBlindLongRange {1, (index : Int) + 2} ≠ 0 simp [interactionTerm, Ne.symm awayZero, Ne.symm awayOne] theorem origin_blind_interaction_is_not_translation_invariant : ¬ geometry.TranslationInvariantAt .originBlindLongRange := by intro invariant have finite := geometry.finite_origin_range_is_uniform .originBlindLongRange invariant origin_blind_interaction_has_source_origin_finite_range 1 exact origin_blind_interaction_has_infinite_range_at_one finite theorem finite_origin_range_without_translation_invariance_is_not_uniform : (scalarModel.LocalSelfAdjointInteractionAt .originBlindLongRange ∧ geometry.FiniteRangeAt .originBlindLongRange) ∧ ¬ (∀ center : Int, (scalarModel.interactionNeighborhood .originBlindLongRange center).Finite) := by refine ⟨⟨scalar_interactions_are_local_selfadjoint _, origin_blind_interaction_has_source_origin_finite_range⟩, ?_⟩ intro uniform exact origin_blind_interaction_has_infinite_range_at_one (uniform 1) theorem scalar_spatial_action_is_not_faithful : ¬ geometry.FaithfulSpatialActionAt := by intro faithful have equal : (Multiplicative.ofAdd (fun _ : Fin 1 => (1 : Int)) : Multiplicative geometry.Displacement) = Multiplicative.ofAdd 0 := faithful (by rfl) have coordinate := congrArg (fun displacement : Multiplicative geometry.Displacement => displacement.toAdd 0) equal norm_num at coordinate theorem lawful_spatial_action_need_not_be_faithful : (geometry.TranslationInvariantAt .nearestNeighbor ∧ geometry.FiniteRangeAt .nearestNeighbor ∧ geometry.translateSite (fun _ => 1) 0 = 1) ∧ ¬ geometry.FaithfulSpatialActionAt := by refine ⟨⟨nearest_neighbor_interaction_is_translation_invariant, nearest_neighbor_has_source_finite_range, ?_⟩, scalar_spatial_action_is_not_faithful⟩ simpa only [zero_add] using actual_site_translation (fun _ : Fin 1 => (1 : Int)) 0 theorem zero_dimensional_coordinates_do_not_supply_unbounded_exterior : (∀ displacement : LatticeDisplacement 0, LatticeDisplacement.length displacement = 0) ∧ ¬ Nonempty (LatticeDisplacement.ExteriorPointAt 0 1) := by refine ⟨LatticeDisplacement.zero_dimensional_lengths_vanish, ?_⟩ rintro ⟨point⟩ exact (LatticeDisplacement.zero_dimensional_lattice_has_no_positive_velocity_exterior 1 (by norm_num)).false point end CubicLatticeControls end CubicLatticeSemantics structure DynamicalRegime where label : Nat deriving DecidableEq, Repr structure InvariantState where label : Nat deriving DecidableEq, Repr structure Representation where label : Nat deriving DecidableEq, Repr structure Projection where label : Nat deriving DecidableEq, Repr /-- The 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 PropagationBound where thresholdVelocity : Real decayRateAt : Real → Real /-- Typed token for the original finite-range commutator-cone derivation. -/ inductive LiebRobinsonFiniteVelocityDerivation where | oneSiteDifferentialGreenFunctionAndContour deriving DecidableEq, Repr /-- Paper-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 PaperFramework where selectedDescription : DynamicsDescription selectedSystem : SpinSystem finiteRangeInteraction : Interaction exponentialTailInteraction : Interaction slowerTailInteraction : Interaction localObservableA : Observable localObservableB : Observable sourceRegion : SpatialRegion targetRegion : SpatialRegion selectedRegime : DynamicalRegime quasiLocalObservableA : Observable quasiLocalObservableB : Observable localBound : PropagationBound exponentialTailBound : PropagationBound operatorModel : QuantumSpinOperatorModel Interaction Observable SpatialRegion latticeGeometry : CubicLatticeOperatorGeometry operatorModel selectedInvariantState : InvariantState selectedRepresentation : Representation invariantProjection : Projection interactionHasExponentialTail : Interaction → Prop interactionHasSlowerTail : Interaction → Prop interactionBelongsToExponentialRefinementClass : Interaction → Prop interactionBelongsToSlowerTailRefinementClass : Interaction → Prop localTimeEvolutionIsAnalytic : Interaction → Prop oneSiteBasisReductionValid : Interaction → Observable → Observable → Prop equationsOfMotionYieldDifferentialInequality : Interaction → Observable → Observable → Prop greenFunctionIsNonnegative : Interaction → Prop greenFunctionIsRealAnalytic : Interaction → Prop greenFunctionDominatesLocalCommutators : Interaction → Observable → Observable → Prop contourShiftBoundsGreenFunctionOutsideCone : Interaction → PropagationBound → Prop boundHasFiniteThreshold : PropagationBound → Prop decayRateIsPositiveAndDecreasingAboveThreshold : PropagationBound → Prop strictlyLocalCommutatorsDecayExponentiallyOutsideCone : Interaction → PropagationBound → Prop commutatorEstimateIsIndependentOfState : Interaction → PropagationBound → Prop informationPropagationHasFiniteGroupVelocity : Interaction → PropagationBound → Prop exactCommutatorVanishingOutsideConeEstablished : Interaction → PropagationBound → Prop descriptionValidInRegime : DynamicsDescription → DynamicalRegime → Prop descriptionModelsSystem : DynamicsDescription → SpinSystem → DynamicalRegime → Prop interactionGovernsSystemAt : Interaction → SpinSystem → DynamicalRegime → Prop commutatorDecreaseTracksInteractionTail : Interaction → Prop commutatorDecreaseIsNonexponential : Interaction → Prop exponentialTailRefinementCalculationDisplayedFor : Interaction → Prop slowerTailRefinementCalculationDisplayedFor : Interaction → Prop velocityEstimateIsCrudeUpperBound : Interaction → PropagationBound → Prop velocityUpperBoundComputableForNearestNeighborHeisenberg : PropagationBound → Prop commutatorHierarchyTruncationsGiveUpperBounds : Interaction → Prop commutatorHierarchyProposedToImproveEstimate : Interaction → Prop hierarchyConvergenceToTrueVelocityEstablished : Interaction → Prop quasiLocalAlgebraIsAsymptoticallyAbelianInCone : Interaction → PropagationBound → Prop stateIsInvariantUnderSpacetimeTranslations : InvariantState → Interaction → Prop representationComesFromInvariantState : Representation → InvariantState → Prop spacetimeTranslationsHaveUnitaryImplementation : Representation → Interaction → Prop projectionSelectsInvariantSubspace : Projection → Representation → Prop weakConeMeanEqualsInvariantProjection : Representation → Projection → Interaction → Prop compressedObservableAlgebraIsAbelian : Representation → Projection → Prop quasiLocalAlgebraIsGAbelian : InvariantState → Interaction → Prop invariantStateHasUniqueBarycentricDecomposition : InvariantState → Interaction → Prop namespace PaperFramework variable (framework : PaperFramework) abbrev Displacement := LatticeDisplacement framework.latticeGeometry.dimension def spaceTranslation (displacement : framework.Displacement) := framework.latticeGeometry.translateOperator displacement def spatialDisplacementNormValue (displacement : framework.Displacement) : Real := LatticeDisplacement.length displacement def cubicLatticeSpinKinematics (system : SpinSystem) : Prop := system = framework.selectedSystem ∧ 0 < framework.latticeGeometry.dimension def finiteDimensionalOnSiteSpaces (system : SpinSystem) : Prop := letI := framework.operatorModel.operatorAlgebra system = framework.selectedSystem ∧ 0 < framework.latticeGeometry.onsiteDimension ∧ ∀ site : framework.operatorModel.Site, Nonempty ((framework.operatorModel.localAlgebra {site}) ≃⋆ₐ[Complex] Matrix (Fin framework.latticeGeometry.onsiteDimension) (Fin framework.latticeGeometry.onsiteDimension) Complex) def finiteRegionMatrixAlgebras (system : SpinSystem) : Prop := system = framework.selectedSystem ∧ framework.latticeGeometry.FullMatrixLocalAlgebrasAt ∧ framework.operatorModel.DisjointTensorGeneration def localAlgebrasAreIsotone (system : SpinSystem) : Prop := system = framework.selectedSystem ∧ framework.operatorModel.LocalAlgebraIsotony def quasiLocalAlgebraIsNormCompletion (system : SpinSystem) : Prop := system = framework.selectedSystem ∧ framework.operatorModel.NormDenseLocalAlgebra def spaceTranslationsActByAutomorphisms (system : SpinSystem) : Prop := system = framework.selectedSystem ∧ framework.latticeGeometry.LocalAlgebraCovarianceAt ∧ framework.latticeGeometry.FaithfulSpatialActionAt def interactionIsTranslationInvariant (interaction : Interaction) : Prop := framework.latticeGeometry.TranslationInvariantAt interaction def interactionHasFiniteRange (interaction : Interaction) : Prop := framework.latticeGeometry.FiniteRangeAt interaction def regionsMetricSeparatedAt (source target : SpatialRegion) (regime : DynamicalRegime) : Prop := regime = framework.selectedRegime ∧ 0 < framework.latticeGeometry.supportDistance (framework.operatorModel.sites source) (framework.operatorModel.sites target) def strictlyLocalObservablesAreNormDenseInQuasiLocalAlgebra (system : SpinSystem) : Prop := framework.quasiLocalAlgebraIsNormCompletion system def translatedTimeEvolvedCommutatorNormValueAt (interaction : Interaction) (source target : Observable) (displacement : framework.Displacement) (time : Real) : Real := letI := framework.operatorModel.operatorAlgebra QuantumCommutator.commutatorNorm (framework.operatorModel.timeEvolution interaction) (framework.spaceTranslation displacement (framework.operatorModel.observable source)) (framework.operatorModel.observable target) time def strictlyLocal (observable : Observable) : Prop := framework.operatorModel.StrictlyLocalAt observable def quasiLocal (observable : Observable) : Prop := framework.operatorModel.QuasiLocalAt observable def observableLocalizedIn (observable : Observable) (region : SpatialRegion) : Prop := framework.operatorModel.LocalizedIn observable region def interactionTermsAreHermitian (interaction : Interaction) : Prop := letI := framework.operatorModel.operatorAlgebra ∀ support, IsSelfAdjoint (framework.operatorModel.interactionTerm interaction support) def finiteVolumeHamiltoniansAreDefined (interaction : Interaction) : Prop := framework.operatorModel.LocalSelfAdjointInteractionAt interaction def stronglyContinuousTimeAutomorphisms (interaction : Interaction) : Prop := framework.operatorModel.StronglyContinuousAt interaction def timeAutomorphismsPreserveProducts (interaction : Interaction) : Prop := letI := framework.operatorModel.operatorAlgebra ∀ (time : Real) (first second : framework.operatorModel.Operator), QuantumCommutator.evolve (framework.operatorModel.timeEvolution interaction) time (first * second) = QuantumCommutator.evolve (framework.operatorModel.timeEvolution interaction) time first * QuantumCommutator.evolve (framework.operatorModel.timeEvolution interaction) time second def timeAutomorphismsPreserveNorm (interaction : Interaction) : Prop := letI := framework.operatorModel.operatorAlgebra ∀ (time : Real) (observable : framework.operatorModel.Operator), ‖QuantumCommutator.evolve (framework.operatorModel.timeEvolution interaction) time observable‖ = ‖observable‖ def finiteVolumeDynamicsConvergesToQuasiLocalDynamics (interaction : Interaction) : Prop := framework.operatorModel.FiniteVolumeConvergenceAt interaction def OperatorKinematicsAt : Prop := framework.operatorModel.LocalAlgebraIsotony ∧ framework.operatorModel.DisjointLocality ∧ framework.operatorModel.NormDenseLocalAlgebra def CubicLatticeKinematicsAt : Prop := 0 < framework.latticeGeometry.dimension ∧ framework.latticeGeometry.FullMatrixLocalAlgebrasAt ∧ framework.operatorModel.DisjointTensorGeneration ∧ framework.latticeGeometry.LocalAlgebraCovarianceAt ∧ framework.latticeGeometry.FaithfulSpatialActionAt theorem actual_time_automorphisms_preserve_products_and_norm (interaction : Interaction) : framework.timeAutomorphismsPreserveProducts interaction ∧ framework.timeAutomorphismsPreserveNorm interaction := by letI := framework.operatorModel.operatorAlgebra exact ⟨fun time first second => map_mul (framework.operatorModel.timeEvolution interaction (Multiplicative.ofAdd time)) first second, QuantumCommutator.evolve_norm (framework.operatorModel.timeEvolution interaction)⟩ theorem actual_translated_commutator_has_state_independent_trivial_bound (interaction : Interaction) (source target : Observable) (displacement : framework.Displacement) (time : Real) : framework.translatedTimeEvolvedCommutatorNormValueAt interaction source target displacement time ≤ 2 * framework.operatorModel.observableNorm source * framework.operatorModel.observableNorm target := by letI := framework.operatorModel.operatorAlgebra simpa only [translatedTimeEvolvedCommutatorNormValueAt, QuantumSpinOperatorModel.observableNorm, StarAlgEquiv.norm_map] using QuantumCommutator.evolved_commutator_norm_le (framework.operatorModel.timeEvolution interaction) (framework.spaceTranslation displacement (framework.operatorModel.observable source)) (framework.operatorModel.observable target) time def SpinSystemKinematics : Prop := framework.cubicLatticeSpinKinematics framework.selectedSystem ∧ framework.finiteDimensionalOnSiteSpaces framework.selectedSystem ∧ framework.finiteRegionMatrixAlgebras framework.selectedSystem ∧ framework.localAlgebrasAreIsotone framework.selectedSystem ∧ framework.quasiLocalAlgebraIsNormCompletion framework.selectedSystem ∧ framework.spaceTranslationsActByAutomorphisms framework.selectedSystem ∧ framework.OperatorKinematicsAt def FiniteRangeDynamicsSetup : Prop := framework.SpinSystemKinematics ∧ framework.interactionTermsAreHermitian framework.finiteRangeInteraction ∧ framework.interactionIsTranslationInvariant framework.finiteRangeInteraction ∧ framework.interactionHasFiniteRange framework.finiteRangeInteraction ∧ framework.finiteVolumeHamiltoniansAreDefined framework.finiteRangeInteraction theorem spin_setup_retains_actual_operator_kinematics (setup : framework.SpinSystemKinematics) : framework.OperatorKinematicsAt := by rcases setup with ⟨_lattice, _dimensions, _matrices, _isotone, _completion, _translations, actual⟩ exact actual theorem spin_setup_retains_actual_cubic_lattice (setup : framework.SpinSystemKinematics) : framework.CubicLatticeKinematicsAt := by rcases setup with ⟨cubic, _onsite, matrices, _isotony, _completion, translations, _operators⟩ exact ⟨cubic.2, matrices.2.1, matrices.2.2, translations.2.1, translations.2.2⟩ theorem actual_cubic_lattice_algebras_realize_spin_kinematics (operators : framework.OperatorKinematicsAt) (lattice : framework.CubicLatticeKinematicsAt) : framework.SpinSystemKinematics := by letI := framework.operatorModel.operatorAlgebra rcases lattice with ⟨positive, matrices, tensor, covariance, faithful⟩ have onsite : framework.finiteDimensionalOnSiteSpaces framework.selectedSystem := by refine ⟨rfl, matrices.1, ?_⟩ intro site have oneSite := matrices.2 ({site} : Finset framework.operatorModel.Site) rw [Finset.card_singleton, pow_one] at oneSite exact oneSite exact ⟨⟨rfl, positive⟩, onsite, ⟨rfl, matrices, tensor⟩, ⟨rfl, operators.1⟩, ⟨rfl, operators.2.2⟩, ⟨rfl, covariance, faithful⟩, operators⟩ theorem actual_cubic_interaction_realizes_finite_range_setup (operators : framework.OperatorKinematicsAt) (lattice : framework.CubicLatticeKinematicsAt) (interaction : framework.operatorModel.LocalSelfAdjointInteractionAt framework.finiteRangeInteraction) (invariant : framework.latticeGeometry.TranslationInvariantAt framework.finiteRangeInteraction) (finiteRange : framework.latticeGeometry.FiniteRangeAt framework.finiteRangeInteraction) : framework.FiniteRangeDynamicsSetup := ⟨framework.actual_cubic_lattice_algebras_realize_spin_kinematics operators lattice, fun support => (interaction support).2, invariant, finiteRange, interaction⟩ /-- The dynamics construction is recalled from Robinson's earlier work. Its exact output is exposed here as an imported theorem hypothesis. -/ def DynamicsConstruction : Prop := framework.FiniteRangeDynamicsSetup → framework.stronglyContinuousTimeAutomorphisms framework.finiteRangeInteraction ∧ framework.timeAutomorphismsPreserveProducts framework.finiteRangeInteraction ∧ framework.timeAutomorphismsPreserveNorm framework.finiteRangeInteraction ∧ framework.localTimeEvolutionIsAnalytic framework.finiteRangeInteraction ∧ framework.finiteVolumeDynamicsConvergesToQuasiLocalDynamics framework.finiteRangeInteraction def EstablishedFiniteRangeDynamics : Prop := framework.FiniteRangeDynamicsSetup ∧ framework.stronglyContinuousTimeAutomorphisms framework.finiteRangeInteraction ∧ framework.timeAutomorphismsPreserveProducts framework.finiteRangeInteraction ∧ framework.timeAutomorphismsPreserveNorm framework.finiteRangeInteraction ∧ framework.localTimeEvolutionIsAnalytic framework.finiteRangeInteraction ∧ framework.finiteVolumeDynamicsConvergesToQuasiLocalDynamics framework.finiteRangeInteraction theorem actual_operator_regularity_realizes_dynamics_construction (regularity : framework.FiniteRangeDynamicsSetup → framework.operatorModel.StronglyContinuousAt framework.finiteRangeInteraction ∧ framework.localTimeEvolutionIsAnalytic framework.finiteRangeInteraction ∧ framework.operatorModel.FiniteVolumeConvergenceAt framework.finiteRangeInteraction) : framework.DynamicsConstruction := by intro setup have actual := regularity setup have algebra := framework.actual_time_automorphisms_preserve_products_and_norm framework.finiteRangeInteraction exact ⟨actual.1, algebra.1, algebra.2, actual.2.1, actual.2.2⟩ theorem established_dynamics_retains_actual_operator_realization (dynamics : framework.EstablishedFiniteRangeDynamics) : framework.operatorModel.AdmissibleDynamicsAt framework.finiteRangeInteraction := by have kinematics := framework.spin_setup_retains_actual_operator_kinematics dynamics.1.1 exact ⟨kinematics.1, kinematics.2.1, dynamics.1.2.2.2.2, dynamics.2.1, dynamics.2.2.2.2.2⟩ theorem established_dynamics_derives_actual_spacetime_covariance (dynamics : framework.EstablishedFiniteRangeDynamics) : framework.CubicLatticeKinematicsAt ∧ framework.latticeGeometry.TranslationInvariantAt framework.finiteRangeInteraction ∧ framework.latticeGeometry.FiniteRangeAt framework.finiteRangeInteraction ∧ framework.latticeGeometry.DynamicsTranslationCovariantAt framework.finiteRangeInteraction := ⟨framework.spin_setup_retains_actual_cubic_lattice dynamics.1.1, dynamics.1.2.2.1, dynamics.1.2.2.2.1, framework.latticeGeometry.actual_finite_volume_limit_derives_spacetime_covariance framework.finiteRangeInteraction dynamics.1.2.2.1 dynamics.2.2.2.2.2⟩ theorem earlier_dynamics_construction_establishes_quasi_local_time_evolution (setup : framework.FiniteRangeDynamicsSetup) (construction : framework.DynamicsConstruction) : framework.EstablishedFiniteRangeDynamics := by exact ⟨setup, construction setup⟩ def LocalCommutatorLocalSetup : Prop := framework.strictlyLocal framework.localObservableA ∧ framework.strictlyLocal framework.localObservableB def LocalCommutatorSetup : Prop := framework.EstablishedFiniteRangeDynamics ∧ framework.LocalCommutatorLocalSetup def OneSiteBasisReductionResult : Prop := framework.oneSiteBasisReductionValid framework.finiteRangeInteraction framework.localObservableA framework.localObservableB def OneSiteBasisReductionCalculation : Prop := framework.LocalCommutatorSetup → framework.OneSiteBasisReductionResult def DifferentialInequalityResult : Prop := framework.equationsOfMotionYieldDifferentialInequality framework.finiteRangeInteraction framework.localObservableA framework.localObservableB def DifferentialInequalityCalculation : Prop := framework.LocalCommutatorSetup → framework.OneSiteBasisReductionResult → framework.DifferentialInequalityResult def GreenFunctionResult : Prop := framework.greenFunctionIsNonnegative framework.finiteRangeInteraction ∧ framework.greenFunctionIsRealAnalytic framework.finiteRangeInteraction ∧ framework.greenFunctionDominatesLocalCommutators framework.finiteRangeInteraction framework.localObservableA framework.localObservableB def GreenFunctionCalculation : Prop := framework.DifferentialInequalityResult → framework.GreenFunctionResult /-- One 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. -/ def ExteriorConePointAt (framework : PaperFramework) (velocity : Real) := { point : framework.Displacement × Real // velocity * abs point.2 < framework.spatialDisplacementNormValue point.1 } /-- The exterior-cone filter is not allowed to become vacuous: for every time scale there is a farther translated point still satisfying `|x| > v |t|`. -/ def ExteriorConeDomainNonvacuousAt (framework : PaperFramework) (velocity : Real) : Prop := ∀ scale : Real, ∃ point : framework.ExteriorConePointAt velocity, scale < abs point.1.2 theorem actual_cubic_lattice_has_unbounded_exterior_domain (positive : 0 < framework.latticeGeometry.dimension) (velocity : Real) : framework.ExteriorConeDomainNonvacuousAt velocity := LatticeDisplacement.exterior_domain_is_nonvacuous framework.latticeGeometry.dimension positive velocity /-- Original 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. -/ def OriginalStrictLocalCommutatorConeFormulaAt : Prop := let threshold := framework.localBound.thresholdVelocity let mu := framework.localBound.decayRateAt (∀ displacement, 0 ≤ framework.spatialDisplacementNormValue displacement) ∧ (∀ source target displacement time, 0 ≤ framework.translatedTimeEvolvedCommutatorNormValueAt framework.finiteRangeInteraction source target displacement time) ∧ (∀ velocity, threshold < velocity → 0 < mu velocity) ∧ (∀ velocityOne velocityTwo, threshold < velocityOne → velocityOne ≤ velocityTwo → mu velocityTwo ≤ mu velocityOne) ∧ (∀ velocity, threshold < velocity → framework.ExteriorConeDomainNonvacuousAt velocity) ∧ ∀ velocity, threshold < velocity → ∀ source target, framework.strictlyLocal source → framework.strictlyLocal target → Filter.Tendsto (fun point : framework.ExteriorConePointAt velocity => Real.exp (mu velocity * abs point.1.2) * framework.translatedTimeEvolvedCommutatorNormValueAt framework.finiteRangeInteraction source target point.1.1 point.1.2) (Filter.comap (fun point : framework.ExteriorConePointAt velocity => abs point.1.2) Filter.atTop) (nhds 0) theorem original_asymptotic_formula_from_actual_cubic_lattice (setup : framework.SpinSystemKinematics) (positiveDecay : ∀ velocity, framework.localBound.thresholdVelocity < velocity → 0 < framework.localBound.decayRateAt velocity) (decreasingDecay : ∀ first second, framework.localBound.thresholdVelocity < first → first ≤ second → framework.localBound.decayRateAt second ≤ framework.localBound.decayRateAt first) (estimate : ∀ velocity, framework.localBound.thresholdVelocity < velocity → ∀ source target, framework.strictlyLocal source → framework.strictlyLocal target → Filter.Tendsto (fun point : framework.ExteriorConePointAt velocity => Real.exp (framework.localBound.decayRateAt velocity * abs point.1.2) * framework.translatedTimeEvolvedCommutatorNormValueAt framework.finiteRangeInteraction source target point.1.1 point.1.2) (Filter.comap (fun point : framework.ExteriorConePointAt velocity => abs point.1.2) Filter.atTop) (nhds 0)) : framework.OriginalStrictLocalCommutatorConeFormulaAt := by letI := framework.operatorModel.operatorAlgebra refine ⟨LatticeDisplacement.length_nonnegative, fun _ _ _ _ => norm_nonneg _, positiveDecay, decreasingDecay, ?_, estimate⟩ intro velocity _aboveThreshold exact framework.actual_cubic_lattice_has_unbounded_exterior_domain (framework.spin_setup_retains_actual_cubic_lattice setup).1 velocity def ContourEstimateResult : Prop := framework.contourShiftBoundsGreenFunctionOutsideCone framework.finiteRangeInteraction framework.localBound ∧ framework.boundHasFiniteThreshold framework.localBound ∧ framework.decayRateIsPositiveAndDecreasingAboveThreshold framework.localBound ∧ framework.strictlyLocalCommutatorsDecayExponentiallyOutsideCone framework.finiteRangeInteraction framework.localBound ∧ framework.commutatorEstimateIsIndependentOfState framework.finiteRangeInteraction framework.localBound ∧ framework.OriginalStrictLocalCommutatorConeFormulaAt def ContourEstimateCalculation : Prop := framework.GreenFunctionResult → framework.ContourEstimateResult def LocalConePhysicalInterpretation : Prop := framework.ContourEstimateResult → framework.informationPropagationHasFiniteGroupVelocity framework.finiteRangeInteraction framework.localBound def LocalConeScopeAssessment : Prop := ¬framework.exactCommutatorVanishingOutsideConeEstablished framework.finiteRangeInteraction framework.localBound def EstablishedStrictLocalCommutatorCone : Prop := framework.LocalCommutatorSetup ∧ framework.oneSiteBasisReductionValid framework.finiteRangeInteraction framework.localObservableA framework.localObservableB ∧ framework.equationsOfMotionYieldDifferentialInequality framework.finiteRangeInteraction framework.localObservableA framework.localObservableB ∧ framework.greenFunctionIsNonnegative framework.finiteRangeInteraction ∧ framework.greenFunctionIsRealAnalytic framework.finiteRangeInteraction ∧ framework.greenFunctionDominatesLocalCommutators framework.finiteRangeInteraction framework.localObservableA framework.localObservableB ∧ framework.contourShiftBoundsGreenFunctionOutsideCone framework.finiteRangeInteraction framework.localBound ∧ framework.boundHasFiniteThreshold framework.localBound ∧ framework.decayRateIsPositiveAndDecreasingAboveThreshold framework.localBound ∧ framework.strictlyLocalCommutatorsDecayExponentiallyOutsideCone framework.finiteRangeInteraction framework.localBound ∧ framework.commutatorEstimateIsIndependentOfState framework.finiteRangeInteraction framework.localBound ∧ framework.OriginalStrictLocalCommutatorConeFormulaAt /-- The strict-local cone retains the report's actual p. 5 asymptotic formula, not merely a named exponential-suppression predicate. -/ theorem strict_local_cone_retains_original_asymptotic_formula (cone : framework.EstablishedStrictLocalCommutatorCone) : framework.OriginalStrictLocalCommutatorConeFormulaAt := by rcases cone with ⟨_setup, _basis, _differential, _greenNonnegative, _greenAnalytic, _greenDominates, _contour, _finiteThreshold, _decay, _suppressed, _stateIndependent, formula⟩ exact formula theorem strict_local_cone_retains_actual_operator_dynamics (cone : framework.EstablishedStrictLocalCommutatorCone) : framework.operatorModel.AdmissibleDynamicsAt framework.finiteRangeInteraction := framework.established_dynamics_retains_actual_operator_realization cone.1.1 def EstablishedFiniteGroupVelocity : Prop := framework.EstablishedStrictLocalCommutatorCone ∧ framework.informationPropagationHasFiniteGroupVelocity framework.finiteRangeInteraction framework.localBound ∧ framework.LocalConeScopeAssessment theorem local_matrix_estimates_establish_finite_group_velocity (setup : framework.LocalCommutatorSetup) (basis : framework.OneSiteBasisReductionCalculation) (differential : framework.DifferentialInequalityCalculation) (green : framework.GreenFunctionCalculation) (contour : framework.ContourEstimateCalculation) (interpretation : framework.LocalConePhysicalInterpretation) (scope : framework.LocalConeScopeAssessment) : framework.EstablishedFiniteGroupVelocity := by have basisResult := basis setup have differentialResult := differential setup basisResult have greenResult := green differentialResult have contourResult := contour greenResult have localCone : framework.EstablishedStrictLocalCommutatorCone := ⟨setup, basisResult, differentialResult, greenResult.1, greenResult.2.1, greenResult.2.2, contourResult.1, contourResult.2.1, contourResult.2.2.1, contourResult.2.2.2.1, contourResult.2.2.2.2.1, contourResult.2.2.2.2.2⟩ exact ⟨localCone, interpretation contourResult, scope⟩ /-- Raw 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. -/ def LiebRobinsonFiniteVelocityDerivationObtains (framework : PaperFramework) : LiebRobinsonFiniteVelocityDerivation -> Prop | .oneSiteDifferentialGreenFunctionAndContour => framework.LocalCommutatorSetup ∧ framework.OneSiteBasisReductionCalculation ∧ framework.DifferentialInequalityCalculation ∧ framework.GreenFunctionCalculation ∧ framework.ContourEstimateCalculation ∧ framework.LocalConePhysicalInterpretation ∧ framework.LocalConeScopeAssessment ∧ framework.descriptionValidInRegime framework.selectedDescription framework.selectedRegime ∧ framework.descriptionModelsSystem framework.selectedDescription framework.selectedSystem framework.selectedRegime ∧ framework.interactionGovernsSystemAt framework.finiteRangeInteraction framework.selectedSystem framework.selectedRegime ∧ framework.observableLocalizedIn framework.localObservableA framework.sourceRegion ∧ framework.observableLocalizedIn framework.localObservableB framework.targetRegion ∧ framework.regionsMetricSeparatedAt framework.sourceRegion framework.targetRegion framework.selectedRegime def toFiniteVelocityCommutatorConeContext : FiniteVelocityCommutatorConeContext DynamicsDescription SpinSystem Interaction Observable SpatialRegion PropagationBound DynamicalRegime where selectedDescription := framework.selectedDescription selectedSystem := framework.selectedSystem selectedInteraction := framework.finiteRangeInteraction selectedSourceObservable := framework.localObservableA selectedTargetObservable := framework.localObservableB selectedSourceRegion := framework.sourceRegion selectedTargetRegion := framework.targetRegion selectedBound := framework.localBound selectedRegime := framework.selectedRegime validity := { validAt := framework.descriptionValidInRegime } localizedIn := framework.observableLocalizedIn descriptionModelsSystem := framework.descriptionModelsSystem interactionGovernsSystem := framework.interactionGovernsSystemAt dynamicsDefinedFor := fun description interaction regime => description = framework.selectedDescription ∧ interaction = framework.finiteRangeInteraction ∧ regime = framework.selectedRegime ∧ framework.EstablishedFiniteRangeDynamics regionsMetricSeparatedAt := framework.regionsMetricSeparatedAt interactionDecayControlledAt := fun interaction regime => interaction = framework.finiteRangeInteraction ∧ regime = framework.selectedRegime ∧ framework.interactionHasFiniteRange interaction commutatorConeCalculatedFor := fun description interaction source target sourceRegion targetRegion bound regime => description = framework.selectedDescription ∧ interaction = framework.finiteRangeInteraction ∧ source = framework.localObservableA ∧ target = framework.localObservableB ∧ sourceRegion = framework.sourceRegion ∧ targetRegion = framework.targetRegion ∧ bound = framework.localBound ∧ regime = framework.selectedRegime ∧ framework.EstablishedStrictLocalCommutatorCone commutatorBoundStateIndependent := fun bound regime => bound = framework.localBound ∧ regime = framework.selectedRegime ∧ framework.commutatorEstimateIsIndependentOfState framework.finiteRangeInteraction bound commutatorSuppressedOutsideCone := fun bound sourceRegion targetRegion regime => bound = framework.localBound ∧ sourceRegion = framework.sourceRegion ∧ targetRegion = framework.targetRegion ∧ regime = framework.selectedRegime ∧ framework.strictlyLocalCommutatorsDecayExponentiallyOutsideCone framework.finiteRangeInteraction bound finiteInformationVelocityFor := fun system interaction bound regime => system = framework.selectedSystem ∧ interaction = framework.finiteRangeInteraction ∧ bound = framework.localBound ∧ regime = framework.selectedRegime ∧ framework.informationPropagationHasFiniteGroupVelocity interaction bound def finiteVelocityCommutatorModel : FiniteVelocityCommutatorModel DynamicsDescription SpinSystem Interaction Observable SpatialRegion PropagationBound DynamicalRegime := framework.toFiniteVelocityCommutatorConeContext.selectedModel theorem finite_velocity_commutator_model_retains_paper_semantics : framework.toFiniteVelocityCommutatorConeContext |>.SelectedFiniteVelocityCommutatorSemanticsAt framework.finiteVelocityCommutatorModel := rfl /-- Execute 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. -/ theorem finite_velocity_source_inputs_make_shared_route_applicable (setup : framework.LocalCommutatorSetup) (basis : framework.OneSiteBasisReductionCalculation) (differential : framework.DifferentialInequalityCalculation) (green : framework.GreenFunctionCalculation) (contour : framework.ContourEstimateCalculation) (interpretation : framework.LocalConePhysicalInterpretation) (descriptionValid : framework.descriptionValidInRegime framework.selectedDescription framework.selectedRegime) (descriptionModels : framework.descriptionModelsSystem framework.selectedDescription framework.selectedSystem framework.selectedRegime) (interactionGoverns : framework.interactionGovernsSystemAt framework.finiteRangeInteraction framework.selectedSystem framework.selectedRegime) (sourceLocalized : framework.observableLocalizedIn framework.localObservableA framework.sourceRegion) (targetLocalized : framework.observableLocalizedIn framework.localObservableB framework.targetRegion) (separated : framework.regionsMetricSeparatedAt framework.sourceRegion framework.targetRegion framework.selectedRegime) : framework.toFiniteVelocityCommutatorConeContext |>.FiniteVelocityCommutatorRouteApplicableAt framework.finiteVelocityCommutatorModel := by have basisResult := basis setup have differentialResult := differential setup basisResult have greenResult := green differentialResult have contourResult := contour greenResult have localCone : framework.EstablishedStrictLocalCommutatorCone := ⟨setup, basisResult, differentialResult, greenResult.1, greenResult.2.1, greenResult.2.2, contourResult.1, contourResult.2.1, contourResult.2.2.1, contourResult.2.2.2.1, contourResult.2.2.2.2.1, contourResult.2.2.2.2.2⟩ have sharedSetup : framework.toFiniteVelocityCommutatorConeContext.LocalDynamicsSetupAt framework.finiteVelocityCommutatorModel := ⟨descriptionValid, descriptionModels, interactionGoverns, ⟨rfl, rfl, rfl, setup.1⟩, sourceLocalized, targetLocalized, separated, ⟨rfl, rfl, setup.1.1.2.2.2.1⟩⟩ have sharedCalculation : framework.toFiniteVelocityCommutatorConeContext |>.CommutatorConeCalculationAt framework.finiteVelocityCommutatorModel := by intro _ exact ⟨⟨rfl, rfl, rfl, rfl, rfl, rfl, rfl, rfl, localCone⟩, ⟨rfl, rfl, contourResult.2.2.2.2.1⟩, ⟨rfl, rfl, rfl, rfl, contourResult.2.2.2.1⟩⟩ have sharedInterpretation : framework.toFiniteVelocityCommutatorConeContext |>.FiniteVelocityInterpretationAt framework.finiteVelocityCommutatorModel := by intro _ _ _ _ exact ⟨rfl, rfl, rfl, rfl, interpretation contourResult⟩ exact framework.toFiniteVelocityCommutatorConeContext |>.setup_calculation_and_interpretation_make_route_applicable framework.finite_velocity_commutator_model_retains_paper_semantics sharedSetup sharedCalculation sharedInterpretation /-- Interpret 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. -/ def toFiniteVelocityCommutatorInterpretation : FiniteVelocityCommutatorInterpretation PaperFramework SpinSystem DynamicsDescription SpinSystem Interaction Observable SpatialRegion PropagationBound DynamicalRegime where theoryUsesCommutatorModel := fun theory model => theory = framework ∧ model = framework.finiteVelocityCommutatorModel ∧ (framework.toFiniteVelocityCommutatorConeContext |>.SelectedFiniteVelocityCommutatorSemanticsAt model) ∧ (framework.toFiniteVelocityCommutatorConeContext |>.LocalDynamicsSetupAt model) commutatorModelRepresentsWorld := fun model world => world = framework.selectedSystem ∧ model = framework.finiteVelocityCommutatorModel ∧ (framework.toFiniteVelocityCommutatorConeContext |>.SelectedFiniteVelocityCommutatorSemanticsAt model) ∧ (framework.toFiniteVelocityCommutatorConeContext |>.LocalDynamicsSetupAt model) ∧ framework.descriptionModelsSystem model.description world model.regime theoryClaim := fun theory model claim => theory = framework ∧ framework.toFiniteVelocityCommutatorConeContext.claimHoldsAt model claim physicalClaim := fun world model claim => world = model.system ∧ framework.toFiniteVelocityCommutatorConeContext.claimHoldsAt model claim theorem finite_velocity_result_realizes_shared_setup (finiteVelocity : framework.EstablishedFiniteGroupVelocity) (descriptionValid : framework.descriptionValidInRegime framework.selectedDescription framework.selectedRegime) (descriptionModels : framework.descriptionModelsSystem framework.selectedDescription framework.selectedSystem framework.selectedRegime) (interactionGoverns : framework.interactionGovernsSystemAt framework.finiteRangeInteraction framework.selectedSystem framework.selectedRegime) (sourceLocalized : framework.observableLocalizedIn framework.localObservableA framework.sourceRegion) (targetLocalized : framework.observableLocalizedIn framework.localObservableB framework.targetRegion) (separated : framework.regionsMetricSeparatedAt framework.sourceRegion framework.targetRegion framework.selectedRegime) : framework.toFiniteVelocityCommutatorConeContext.LocalDynamicsSetupAt framework.finiteVelocityCommutatorModel := by exact ⟨descriptionValid, descriptionModels, interactionGoverns, ⟨rfl, rfl, rfl, finiteVelocity.1.1.1⟩, sourceLocalized, targetLocalized, separated, ⟨rfl, rfl, finiteVelocity.1.1.1.1.2.2.2.1⟩⟩ theorem finite_velocity_result_realizes_shared_calculation (finiteVelocity : framework.EstablishedFiniteGroupVelocity) : framework.toFiniteVelocityCommutatorConeContext.CommutatorConeCalculationAt framework.finiteVelocityCommutatorModel := by have localCone := finiteVelocity.1 rcases localCone with ⟨_setup, _basis, _differential, _greenNonnegative, _greenAnalytic, _greenDominates, _contour, _finiteThreshold, _decay, suppressed, stateIndependent, _formula⟩ intro _ exact ⟨⟨rfl, rfl, rfl, rfl, rfl, rfl, rfl, rfl, finiteVelocity.1⟩, ⟨rfl, rfl, stateIndependent⟩, ⟨rfl, rfl, rfl, rfl, suppressed⟩⟩ theorem finite_velocity_result_realizes_shared_interpretation (finiteVelocity : framework.EstablishedFiniteGroupVelocity) : framework.toFiniteVelocityCommutatorConeContext.FiniteVelocityInterpretationAt framework.finiteVelocityCommutatorModel := by intro _ _ _ _ exact ⟨rfl, rfl, rfl, rfl, finiteVelocity.2.1⟩ theorem finite_velocity_inputs_make_shared_route_applicable (finiteVelocity : framework.EstablishedFiniteGroupVelocity) (descriptionValid : framework.descriptionValidInRegime framework.selectedDescription framework.selectedRegime) (descriptionModels : framework.descriptionModelsSystem framework.selectedDescription framework.selectedSystem framework.selectedRegime) (interactionGoverns : framework.interactionGovernsSystemAt framework.finiteRangeInteraction framework.selectedSystem framework.selectedRegime) (sourceLocalized : framework.observableLocalizedIn framework.localObservableA framework.sourceRegion) (targetLocalized : framework.observableLocalizedIn framework.localObservableB framework.targetRegion) (separated : framework.regionsMetricSeparatedAt framework.sourceRegion framework.targetRegion framework.selectedRegime) : framework.toFiniteVelocityCommutatorConeContext |>.FiniteVelocityCommutatorRouteApplicableAt framework.finiteVelocityCommutatorModel := framework.toFiniteVelocityCommutatorConeContext |>.setup_calculation_and_interpretation_make_route_applicable framework.finite_velocity_commutator_model_retains_paper_semantics (framework.finite_velocity_result_realizes_shared_setup finiteVelocity descriptionValid descriptionModels interactionGoverns sourceLocalized targetLocalized separated) (framework.finite_velocity_result_realizes_shared_calculation finiteVelocity) (framework.finite_velocity_result_realizes_shared_interpretation finiteVelocity) /-- The 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. -/ theorem finite_velocity_inputs_realize_structural_information_propagation_explanation (finiteVelocity : framework.EstablishedFiniteGroupVelocity) (descriptionValid : framework.descriptionValidInRegime framework.selectedDescription framework.selectedRegime) (descriptionModels : framework.descriptionModelsSystem framework.selectedDescription framework.selectedSystem framework.selectedRegime) (interactionGoverns : framework.interactionGovernsSystemAt framework.finiteRangeInteraction framework.selectedSystem framework.selectedRegime) (sourceLocalized : framework.observableLocalizedIn framework.localObservableA framework.sourceRegion) (targetLocalized : framework.observableLocalizedIn framework.localObservableB framework.targetRegion) (separated : framework.regionsMetricSeparatedAt framework.sourceRegion framework.targetRegion framework.selectedRegime) : framework.toFiniteVelocityCommutatorConeContext |>.RouteStructuralFiniteInformationPropagationExplanationAt framework.finiteVelocityCommutatorModel := framework.toFiniteVelocityCommutatorConeContext |>.applicable_route_realizes_structural_finite_information_propagation (framework.finite_velocity_inputs_make_shared_route_applicable finiteVelocity descriptionValid descriptionModels interactionGoverns sourceLocalized targetLocalized separated) /-- The original report gives exponential exterior-cone suppression, not exact relativistic signal exclusion. The independently inhabited shared countermodel makes the missing implication formally explicit. -/ theorem finite_group_velocity_does_not_supply_exact_signal_exclusion_bridge (finiteVelocity : framework.EstablishedFiniteGroupVelocity) : framework.EstablishedFiniteGroupVelocity ∧ ¬(FiniteVelocityCommutatorConeContext.Countermodels.approximateConeContext |>.ExactSignalExclusionBridgeForConeAt FiniteVelocityCommutatorConeContext.Countermodels.controlledModel FiniteVelocityCommutatorConeContext.Countermodels.exactSignallingPropagation) := ⟨finiteVelocity, FiniteVelocityCommutatorConeContext.Countermodels.approximate_commutator_cone_refutes_exact_signal_exclusion_bridge⟩ /- Source: original report pp. 5-9. The one-site basis reduction and equations of motion produce a differential inequality, the positive analytic Green function dominates the commutator, and the Fourier contour estimate yields state-independent exponential suppression before the finite-velocity reading. -/ theorem local_commutator_source_inputs_realize_source_structural_information_propagation_explanation (setup : framework.LocalCommutatorSetup) (basis : framework.OneSiteBasisReductionCalculation) (differential : framework.DifferentialInequalityCalculation) (green : framework.GreenFunctionCalculation) (contour : framework.ContourEstimateCalculation) (interpretation : framework.LocalConePhysicalInterpretation) (scope : framework.LocalConeScopeAssessment) (descriptionValid : framework.descriptionValidInRegime framework.selectedDescription framework.selectedRegime) (descriptionModels : framework.descriptionModelsSystem framework.selectedDescription framework.selectedSystem framework.selectedRegime) (interactionGoverns : framework.interactionGovernsSystemAt framework.finiteRangeInteraction framework.selectedSystem framework.selectedRegime) (sourceLocalized : framework.observableLocalizedIn framework.localObservableA framework.sourceRegion) (targetLocalized : framework.observableLocalizedIn framework.localObservableB framework.targetRegion) (separated : framework.regionsMetricSeparatedAt framework.sourceRegion framework.targetRegion framework.selectedRegime) : framework.toFiniteVelocityCommutatorConeContext |>.SourceStructuralFiniteInformationPropagationExplanationAt framework.finiteVelocityCommutatorModel .oneSiteDifferentialGreenFunctionAndContour framework.LiebRobinsonFiniteVelocityDerivationObtains := by have applicable := framework.finite_velocity_source_inputs_make_shared_route_applicable setup basis differential green contour interpretation descriptionValid descriptionModels interactionGoverns sourceLocalized targetLocalized separated exact framework.toFiniteVelocityCommutatorConeContext |>.source_derivation_and_applicable_route_realize_source_structural_finite_information_propagation .oneSiteDifferentialGreenFunctionAndContour framework.LiebRobinsonFiniteVelocityDerivationObtains ⟨setup, basis, differential, green, contour, interpretation, scope, descriptionValid, descriptionModels, interactionGoverns, sourceLocalized, targetLocalized, separated⟩ applicable theorem finite_velocity_result_establishes_shared_commutator_cone (finiteVelocity : framework.EstablishedFiniteGroupVelocity) (descriptionValid : framework.descriptionValidInRegime framework.selectedDescription framework.selectedRegime) (descriptionModels : framework.descriptionModelsSystem framework.selectedDescription framework.selectedSystem framework.selectedRegime) (interactionGoverns : framework.interactionGovernsSystemAt framework.finiteRangeInteraction framework.selectedSystem framework.selectedRegime) (sourceLocalized : framework.observableLocalizedIn framework.localObservableA framework.sourceRegion) (targetLocalized : framework.observableLocalizedIn framework.localObservableB framework.targetRegion) (separated : framework.regionsMetricSeparatedAt framework.sourceRegion framework.targetRegion framework.selectedRegime) : framework.toFiniteVelocityCommutatorConeContext |>.EstablishedFiniteVelocityCommutatorConeAt framework.finiteVelocityCommutatorModel := framework.toFiniteVelocityCommutatorConeContext |>.applicable_route_establishes_finite_velocity_commutator_cone (framework.finite_velocity_inputs_make_shared_route_applicable finiteVelocity descriptionValid descriptionModels interactionGoverns sourceLocalized targetLocalized separated) /-- The 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. -/ theorem finite_velocity_result_exhibits_nonvacuous_shared_commutator_cone (finiteVelocity : framework.EstablishedFiniteGroupVelocity) (descriptionValid : framework.descriptionValidInRegime framework.selectedDescription framework.selectedRegime) (descriptionModels : framework.descriptionModelsSystem framework.selectedDescription framework.selectedSystem framework.selectedRegime) (interactionGoverns : framework.interactionGovernsSystemAt framework.finiteRangeInteraction framework.selectedSystem framework.selectedRegime) (sourceLocalized : framework.observableLocalizedIn framework.localObservableA framework.sourceRegion) (targetLocalized : framework.observableLocalizedIn framework.localObservableB framework.targetRegion) (separated : framework.regionsMetricSeparatedAt framework.sourceRegion framework.targetRegion framework.selectedRegime) : framework.finiteVelocityCommutatorModel |>.NonvacuousFiniteVelocityCommutatorConeAt := framework.toFiniteVelocityCommutatorConeContext |>.established_cone_exhibits_nonvacuous_finite_velocity_route (framework.finite_velocity_result_establishes_shared_commutator_cone finiteVelocity descriptionValid descriptionModels interactionGoverns sourceLocalized targetLocalized separated) /-- Ground 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. -/ theorem finite_velocity_model_inputs_establish_shared_grounding (setup : framework.toFiniteVelocityCommutatorConeContext |>.LocalDynamicsSetupAt framework.finiteVelocityCommutatorModel) : framework.toFiniteVelocityCommutatorConeContext |>.TheoryModelGroundingAt framework.toFiniteVelocityCommutatorInterpretation framework framework.selectedSystem framework.finiteVelocityCommutatorModel := by apply framework.toFiniteVelocityCommutatorConeContext |>.theory_model_inputs_establish_grounding framework.toFiniteVelocityCommutatorInterpretation framework framework.selectedSystem framework.finiteVelocityCommutatorModel · exact framework.finite_velocity_commutator_model_retains_paper_semantics · exact setup · exact ⟨rfl, rfl, framework.finite_velocity_commutator_model_retains_paper_semantics, setup⟩ · exact ⟨rfl, rfl, framework.finite_velocity_commutator_model_retains_paper_semantics, setup, setup.2.1⟩ · intro _claim modelClaim exact ⟨rfl, modelClaim⟩ · intro _claim modelClaim exact ⟨rfl, modelClaim⟩ theorem finite_velocity_result_establishes_grounded_shared_commutator_cone (finiteVelocity : framework.EstablishedFiniteGroupVelocity) (descriptionValid : framework.descriptionValidInRegime framework.selectedDescription framework.selectedRegime) (descriptionModels : framework.descriptionModelsSystem framework.selectedDescription framework.selectedSystem framework.selectedRegime) (interactionGoverns : framework.interactionGovernsSystemAt framework.finiteRangeInteraction framework.selectedSystem framework.selectedRegime) (sourceLocalized : framework.observableLocalizedIn framework.localObservableA framework.sourceRegion) (targetLocalized : framework.observableLocalizedIn framework.localObservableB framework.targetRegion) (separated : framework.regionsMetricSeparatedAt framework.sourceRegion framework.targetRegion framework.selectedRegime) : framework.toFiniteVelocityCommutatorConeContext |>.TheoryModelGroundedFiniteVelocityCommutatorConeAt framework.toFiniteVelocityCommutatorInterpretation framework framework.selectedSystem framework.finiteVelocityCommutatorModel := by have established := framework.finite_velocity_result_establishes_shared_commutator_cone finiteVelocity descriptionValid descriptionModels interactionGoverns sourceLocalized targetLocalized separated have setup := framework.finite_velocity_result_realizes_shared_setup finiteVelocity descriptionValid descriptionModels interactionGoverns sourceLocalized targetLocalized separated exact framework.toFiniteVelocityCommutatorConeContext |>.established_cone_and_grounding_establish_grounded_cone framework.toFiniteVelocityCommutatorInterpretation established (framework |>.finite_velocity_model_inputs_establish_shared_grounding setup) theorem grounded_finite_velocity_result_transfers_every_shared_claim (grounded : framework.toFiniteVelocityCommutatorConeContext |>.TheoryModelGroundedFiniteVelocityCommutatorConeAt framework.toFiniteVelocityCommutatorInterpretation framework framework.selectedSystem framework.finiteVelocityCommutatorModel) : ∀ claim : FiniteVelocityCommutatorClaim, (framework.toFiniteVelocityCommutatorConeContext.toTheoryModelContext framework.toFiniteVelocityCommutatorInterpretation |>.theoryEntails (FiniteVelocityCommutatorConeContext.theoryAt framework framework.finiteVelocityCommutatorModel) claim ()) ∧ (framework.toFiniteVelocityCommutatorConeContext.toTheoryModelContext framework.toFiniteVelocityCommutatorInterpretation |>.trueIn (FiniteVelocityCommutatorConeContext.worldAt framework.selectedSystem framework.finiteVelocityCommutatorModel) claim ()) := framework.toFiniteVelocityCommutatorConeContext |>.grounded_cone_transfers_all_claims_to_theory_and_world framework.toFiniteVelocityCommutatorInterpretation grounded def ExponentialTailSetup : Prop := framework.SpinSystemKinematics ∧ framework.interactionTermsAreHermitian framework.exponentialTailInteraction ∧ framework.interactionIsTranslationInvariant framework.exponentialTailInteraction ∧ framework.interactionHasExponentialTail framework.exponentialTailInteraction ∧ framework.interactionBelongsToExponentialRefinementClass framework.exponentialTailInteraction ∧ framework.finiteVolumeHamiltoniansAreDefined framework.exponentialTailInteraction ∧ framework.stronglyContinuousTimeAutomorphisms framework.exponentialTailInteraction ∧ framework.timeAutomorphismsPreserveProducts framework.exponentialTailInteraction ∧ framework.timeAutomorphismsPreserveNorm framework.exponentialTailInteraction ∧ framework.localTimeEvolutionIsAnalytic framework.exponentialTailInteraction ∧ framework.finiteVolumeDynamicsConvergesToQuasiLocalDynamics framework.exponentialTailInteraction def ExponentialTailConeResult : Prop := framework.boundHasFiniteThreshold framework.exponentialTailBound ∧ framework.decayRateIsPositiveAndDecreasingAboveThreshold framework.exponentialTailBound ∧ framework.strictlyLocalCommutatorsDecayExponentiallyOutsideCone framework.exponentialTailInteraction framework.exponentialTailBound /-- The paper states that a refinement of the finite-range proof covers a class of exponentially decreasing infinite-range interactions, but omits the calculation. -/ def ExponentialTailRefinement : Prop := framework.ExponentialTailSetup → framework.ExponentialTailConeResult def ExponentialTailPhysicalInterpretation : Prop := framework.ExponentialTailConeResult → framework.informationPropagationHasFiniteGroupVelocity framework.exponentialTailInteraction framework.exponentialTailBound def ExponentialTailCalculationScope : Prop := ¬framework.exponentialTailRefinementCalculationDisplayedFor framework.exponentialTailInteraction def EstablishedExponentialTailFiniteVelocity : Prop := framework.ExponentialTailSetup ∧ framework.ExponentialTailConeResult ∧ framework.informationPropagationHasFiniteGroupVelocity framework.exponentialTailInteraction framework.exponentialTailBound ∧ framework.ExponentialTailCalculationScope theorem exponential_tail_refinement_preserves_finite_velocity_conclusion (setup : framework.ExponentialTailSetup) (refinement : framework.ExponentialTailRefinement) (interpretation : framework.ExponentialTailPhysicalInterpretation) (scope : framework.ExponentialTailCalculationScope) : framework.EstablishedExponentialTailFiniteVelocity := by have result := refinement setup exact ⟨setup, result, interpretation result, scope⟩ def SlowerTailSetup : Prop := framework.SpinSystemKinematics ∧ framework.interactionTermsAreHermitian framework.slowerTailInteraction ∧ framework.interactionIsTranslationInvariant framework.slowerTailInteraction ∧ framework.interactionHasSlowerTail framework.slowerTailInteraction ∧ framework.interactionBelongsToSlowerTailRefinementClass framework.slowerTailInteraction ∧ framework.finiteVolumeHamiltoniansAreDefined framework.slowerTailInteraction ∧ framework.stronglyContinuousTimeAutomorphisms framework.slowerTailInteraction ∧ framework.timeAutomorphismsPreserveProducts framework.slowerTailInteraction ∧ framework.timeAutomorphismsPreserveNorm framework.slowerTailInteraction ∧ framework.localTimeEvolutionIsAnalytic framework.slowerTailInteraction ∧ framework.finiteVolumeDynamicsConvergesToQuasiLocalDynamics framework.slowerTailInteraction def SlowerTailResult : Prop := framework.commutatorDecreaseTracksInteractionTail framework.slowerTailInteraction ∧ framework.commutatorDecreaseIsNonexponential framework.slowerTailInteraction def SlowerTailRefinement : Prop := framework.SlowerTailSetup → framework.SlowerTailResult def SlowerTailScopeAssessment : Prop := ¬framework.slowerTailRefinementCalculationDisplayedFor framework.slowerTailInteraction def EstablishedSlowerTailAssessment : Prop := framework.SlowerTailSetup ∧ framework.SlowerTailResult ∧ framework.SlowerTailScopeAssessment theorem slower_tail_refinement_yields_tail_linked_not_exponential_control (setup : framework.SlowerTailSetup) (refinement : framework.SlowerTailRefinement) (scope : framework.SlowerTailScopeAssessment) : framework.EstablishedSlowerTailAssessment := ⟨setup, refinement setup, scope⟩ def VelocityUpperBoundAssessment : Prop := framework.velocityEstimateIsCrudeUpperBound framework.finiteRangeInteraction framework.localBound ∧ framework.velocityUpperBoundComputableForNearestNeighborHeisenberg framework.localBound ∧ framework.commutatorHierarchyTruncationsGiveUpperBounds framework.finiteRangeInteraction ∧ framework.commutatorHierarchyProposedToImproveEstimate framework.finiteRangeInteraction def VelocityUpperBoundAssessmentCalculation : Prop := framework.EstablishedFiniteGroupVelocity → framework.VelocityUpperBoundAssessment def HierarchyConvergenceOpen : Prop := ¬framework.hierarchyConvergenceToTrueVelocityEstablished framework.finiteRangeInteraction def VelocityEstimateAssessment : Prop := framework.VelocityUpperBoundAssessment ∧ framework.HierarchyConvergenceOpen def EstablishedQualifiedVelocityEstimate : Prop := framework.EstablishedFiniteGroupVelocity ∧ framework.VelocityEstimateAssessment theorem finite_velocity_proof_yields_computable_but_crude_upper_bound (finiteVelocity : framework.EstablishedFiniteGroupVelocity) (calculation : framework.VelocityUpperBoundAssessmentCalculation) (convergenceOpen : framework.HierarchyConvergenceOpen) : framework.EstablishedQualifiedVelocityEstimate := ⟨finiteVelocity, calculation finiteVelocity, convergenceOpen⟩ def QuasiLocalExtensionLocalSetup : Prop := framework.quasiLocal framework.quasiLocalObservableA ∧ framework.quasiLocal framework.quasiLocalObservableB ∧ framework.strictlyLocalObservablesAreNormDenseInQuasiLocalAlgebra framework.selectedSystem ∧ framework.timeAutomorphismsPreserveNorm framework.finiteRangeInteraction def QuasiLocalExtensionSetup : Prop := framework.EstablishedStrictLocalCommutatorCone ∧ framework.QuasiLocalExtensionLocalSetup def QuasiLocalExtensionCalculation : Prop := framework.QuasiLocalExtensionSetup → framework.quasiLocalAlgebraIsAsymptoticallyAbelianInCone framework.finiteRangeInteraction framework.localBound def EstablishedQuasiLocalAsymptoticAbelianness : Prop := framework.QuasiLocalExtensionSetup ∧ framework.quasiLocalAlgebraIsAsymptoticallyAbelianInCone framework.finiteRangeInteraction framework.localBound theorem norm_density_extends_local_cone_to_quasi_local_asymptotic_abelianness (setup : framework.QuasiLocalExtensionSetup) (calculation : framework.QuasiLocalExtensionCalculation) : framework.EstablishedQuasiLocalAsymptoticAbelianness := ⟨setup, calculation setup⟩ def InvariantRepresentationLocalSetup : Prop := framework.stateIsInvariantUnderSpacetimeTranslations framework.selectedInvariantState framework.finiteRangeInteraction ∧ framework.representationComesFromInvariantState framework.selectedRepresentation framework.selectedInvariantState ∧ framework.spacetimeTranslationsHaveUnitaryImplementation framework.selectedRepresentation framework.finiteRangeInteraction ∧ framework.projectionSelectsInvariantSubspace framework.invariantProjection framework.selectedRepresentation def InvariantRepresentationSetup : Prop := framework.EstablishedQuasiLocalAsymptoticAbelianness ∧ framework.InvariantRepresentationLocalSetup def ConeMeanCalculation : Prop := framework.InvariantRepresentationSetup → framework.weakConeMeanEqualsInvariantProjection framework.selectedRepresentation framework.invariantProjection framework.finiteRangeInteraction def GAbelianInference : Prop := framework.InvariantRepresentationSetup → framework.weakConeMeanEqualsInvariantProjection framework.selectedRepresentation framework.invariantProjection framework.finiteRangeInteraction → framework.compressedObservableAlgebraIsAbelian framework.selectedRepresentation framework.invariantProjection ∧ framework.quasiLocalAlgebraIsGAbelian framework.selectedInvariantState framework.finiteRangeInteraction def EstablishedGAbelianness : Prop := framework.InvariantRepresentationSetup ∧ framework.weakConeMeanEqualsInvariantProjection framework.selectedRepresentation framework.invariantProjection framework.finiteRangeInteraction ∧ framework.compressedObservableAlgebraIsAbelian framework.selectedRepresentation framework.invariantProjection ∧ framework.quasiLocalAlgebraIsGAbelian framework.selectedInvariantState framework.finiteRangeInteraction theorem cone_mean_and_asymptotic_abelianness_establish_g_abelianness (setup : framework.InvariantRepresentationSetup) (meanCalculation : framework.ConeMeanCalculation) (inference : framework.GAbelianInference) : framework.EstablishedGAbelianness := by have meanResult := meanCalculation setup have result := inference setup meanResult exact ⟨setup, meanResult, result.1, result.2⟩ def InvariantStateDecompositionSetup : Prop := framework.EstablishedGAbelianness def InvariantStateDecompositionTheorem : Prop := framework.InvariantStateDecompositionSetup → framework.invariantStateHasUniqueBarycentricDecomposition framework.selectedInvariantState framework.finiteRangeInteraction def EstablishedUniqueInvariantStateDecomposition : Prop := framework.InvariantStateDecompositionSetup ∧ framework.invariantStateHasUniqueBarycentricDecomposition framework.selectedInvariantState framework.finiteRangeInteraction theorem g_abelianness_yields_unique_extremal_invariant_state_decomposition (setup : framework.InvariantStateDecompositionSetup) (decomposition : framework.InvariantStateDecompositionTheorem) : framework.EstablishedUniqueInvariantStateDecomposition := ⟨setup, decomposition setup⟩ def CompleteScopedResult : Prop := framework.EstablishedFiniteRangeDynamics ∧ framework.EstablishedFiniteGroupVelocity ∧ framework.EstablishedExponentialTailFiniteVelocity ∧ framework.EstablishedSlowerTailAssessment ∧ framework.EstablishedQualifiedVelocityEstimate ∧ framework.EstablishedQuasiLocalAsymptoticAbelianness ∧ framework.EstablishedGAbelianness ∧ framework.EstablishedUniqueInvariantStateDecomposition theorem independent_routes_establish_complete_scoped_result (dynamics : framework.EstablishedFiniteRangeDynamics) (finiteVelocity : framework.EstablishedFiniteGroupVelocity) (exponentialTail : framework.EstablishedExponentialTailFiniteVelocity) (slowerTail : framework.EstablishedSlowerTailAssessment) (velocityAssessment : framework.EstablishedQualifiedVelocityEstimate) (quasiLocal : framework.EstablishedQuasiLocalAsymptoticAbelianness) (gAbelian : framework.EstablishedGAbelianness) (decomposition : framework.EstablishedUniqueInvariantStateDecomposition) : framework.CompleteScopedResult := ⟨dynamics, finiteVelocity, exponentialTail, slowerTail, velocityAssessment, quasiLocal, gAbelian, decomposition⟩ namespace Countermodels /-- The finite control tests the locality distinction, not the infinite-lattice theorem. -/ theorem actual_finite_spin_hamiltonian_does_not_imply_exact_cone : QuantumCommutator.TwoSpin.ActualSeparatedLocalHamiltonian ∧ ¬ QuantumCommutator.TwoSpin.ExactSeparatedCone 1 1 := QuantumCommutator.TwoSpin.actual_local_hamiltonian_does_not_imply_exact_cone 1 structure ReducedStrictLocalExteriorConeReadout where thresholdVelocity : ℝ testedVelocity : ℝ timeAt : ℕ → ℝ displacementAt : ℕ → ℝ scaledCommutatorNormAt : ℕ → ℝ def strictLocalExteriorConeSetup (readout : ReducedStrictLocalExteriorConeReadout) : Prop := 0 ≤ readout.thresholdVelocity ∧ readout.thresholdVelocity < readout.testedVelocity ∧ ∀ sample, 0 < readout.timeAt sample ∧ readout.testedVelocity * readout.timeAt sample < readout.displacementAt sample ∧ 0 ≤ readout.scaledCommutatorNormAt sample def originalAsymptoticSuppression (readout : ReducedStrictLocalExteriorConeReadout) : Prop := ∀ tolerance : ℝ, 0 < tolerance → ∃ cutoff : ℕ, ∀ sample : ℕ, cutoff ≤ sample → readout.scaledCommutatorNormAt sample < tolerance def exteriorConeWithoutAsymptoticSuppression : ReducedStrictLocalExteriorConeReadout := { thresholdVelocity := 1 testedVelocity := 2 timeAt := fun sample => sample + 1 displacementAt := fun sample => 3 * (sample + 1) scaledCommutatorNormAt := fun _ => 1 } theorem exterior_cone_setup_does_not_supply_original_asymptotic_suppression : strictLocalExteriorConeSetup exteriorConeWithoutAsymptoticSuppression ∧ ¬originalAsymptoticSuppression exteriorConeWithoutAsymptoticSuppression := by constructor · constructor · norm_num [exteriorConeWithoutAsymptoticSuppression] constructor · norm_num [exteriorConeWithoutAsymptoticSuppression] · intro sample have nonnegative : 0 ≤ (sample : ℝ) := by positivity norm_num [exteriorConeWithoutAsymptoticSuppression] constructor <;> nlinarith · intro suppression obtain ⟨cutoff, bounded⟩ := suppression (1 / 2) (by norm_num) have impossible := bounded cutoff (le_refl cutoff) norm_num [exteriorConeWithoutAsymptoticSuppression] at impossible structure ReducedFiniteRangeCommutatorReadout where interactionRange : ℕ interactionTermNormAt : ℕ → ℝ commutatorNorm : ℝ claimedCommutatorBound : ℝ def finiteRangeInteraction (readout : ReducedFiniteRangeCommutatorReadout) : Prop := 0 < readout.interactionRange ∧ ∀ separation : ℕ, readout.interactionRange < separation → readout.interactionTermNormAt separation = 0 def commutatorEstimate (readout : ReducedFiniteRangeCommutatorReadout) : Prop := 0 ≤ readout.claimedCommutatorBound ∧ readout.commutatorNorm ≤ readout.claimedCommutatorBound def finiteRangeWithoutCommutatorEstimate : ReducedFiniteRangeCommutatorReadout := { interactionRange := 1 interactionTermNormAt := fun _ => 0 commutatorNorm := 1 claimedCommutatorBound := 0 } theorem finite_range_assumption_does_not_supply_commutator_estimate : finiteRangeInteraction finiteRangeWithoutCommutatorEstimate ∧ ¬commutatorEstimate finiteRangeWithoutCommutatorEstimate := by constructor · constructor · norm_num [finiteRangeWithoutCommutatorEstimate] · intro separation outsideRange norm_num [finiteRangeWithoutCommutatorEstimate] · norm_num [commutatorEstimate, finiteRangeWithoutCommutatorEstimate] structure ReducedExteriorCommutatorReadout where propagationVelocity : ℝ timeValue : ℝ displacementValue : ℝ decayRate : ℝ prefactor : ℝ commutatorNorm : ℝ def exponentiallySuppressedOutsideCone (readout : ReducedExteriorCommutatorReadout) : Prop := 0 < readout.propagationVelocity ∧ 0 < readout.timeValue ∧ readout.propagationVelocity * readout.timeValue < readout.displacementValue ∧ 0 < readout.decayRate ∧ 0 < readout.prefactor ∧ 0 < readout.commutatorNorm ∧ readout.commutatorNorm ≤ readout.prefactor * Real.exp (-readout.decayRate * (readout.displacementValue - readout.propagationVelocity * readout.timeValue)) def exactlyZeroOutsideCone (readout : ReducedExteriorCommutatorReadout) : Prop := readout.commutatorNorm = 0 noncomputable def exponentiallySmallNonzeroCommutator : ReducedExteriorCommutatorReadout := { propagationVelocity := 1 timeValue := 1 displacementValue := 2 decayRate := 1 prefactor := 1 commutatorNorm := Real.exp (-1) } theorem exponentially_small_commutator_is_not_exact_zero : exponentiallySuppressedOutsideCone exponentiallySmallNonzeroCommutator ∧ ¬exactlyZeroOutsideCone exponentiallySmallNonzeroCommutator := by constructor · norm_num [exponentiallySuppressedOutsideCone, exponentiallySmallNonzeroCommutator, Real.exp_pos] exact le_rfl · have positive : 0 < Real.exp (-1 : ℝ) := Real.exp_pos _ change Real.exp (-1 : ℝ) ≠ 0 exact positive.ne' structure ReducedInteractionVelocityReadout where firstInteractionVelocity : ℝ secondInteractionVelocity : ℝ proposedUniversalVelocity : ℝ def finiteInteractionDependentVelocities (readout : ReducedInteractionVelocityReadout) : Prop := 0 < readout.firstInteractionVelocity ∧ 0 < readout.secondInteractionVelocity ∧ readout.firstInteractionVelocity ≠ readout.secondInteractionVelocity def universalVelocity (readout : ReducedInteractionVelocityReadout) : Prop := readout.firstInteractionVelocity = readout.proposedUniversalVelocity ∧ readout.secondInteractionVelocity = readout.proposedUniversalVelocity def twoInteractionsWithDifferentVelocities : ReducedInteractionVelocityReadout := { firstInteractionVelocity := 1 secondInteractionVelocity := 2 proposedUniversalVelocity := 1 } theorem finite_group_velocity_is_not_a_universal_light_speed : finiteInteractionDependentVelocities twoInteractionsWithDifferentVelocities ∧ ¬universalVelocity twoInteractionsWithDifferentVelocities := by norm_num [finiteInteractionDependentVelocities, universalVelocity, twoInteractionsWithDifferentVelocities] structure ReducedStateCorrelationReadout where stateCommutatorExpectation : ℝ stateTolerance : ℝ operatorCommutatorNorm : ℝ claimedOperatorNormBound : ℝ def weakStateCorrelation (readout : ReducedStateCorrelationReadout) : Prop := 0 ≤ readout.stateTolerance ∧ abs readout.stateCommutatorExpectation ≤ readout.stateTolerance def stateIndependentOperatorNormBound (readout : ReducedStateCorrelationReadout) : Prop := 0 ≤ readout.claimedOperatorNormBound ∧ readout.operatorCommutatorNorm ≤ readout.claimedOperatorNormBound def weakStateCorrelationWithLargeOperatorNorm : ReducedStateCorrelationReadout := { stateCommutatorExpectation := 0 stateTolerance := 0 operatorCommutatorNorm := 1 claimedOperatorNormBound := 0 } theorem state_level_weak_correlation_does_not_supply_operator_norm_bound : weakStateCorrelation weakStateCorrelationWithLargeOperatorNorm ∧ ¬stateIndependentOperatorNormBound weakStateCorrelationWithLargeOperatorNorm := by norm_num [weakStateCorrelation, stateIndependentOperatorNormBound, weakStateCorrelationWithLargeOperatorNorm] structure ReducedQuasiLocalExtensionReadout where strictLocalCommutatorNorm : ℝ strictLocalBound : ℝ approximationErrorAt : ℕ → ℝ def strictLocalConeBound (readout : ReducedQuasiLocalExtensionReadout) : Prop := 0 ≤ readout.strictLocalCommutatorNorm ∧ readout.strictLocalCommutatorNorm ≤ readout.strictLocalBound def quasiLocalNormApproximation (readout : ReducedQuasiLocalExtensionReadout) : Prop := ∀ tolerance : ℝ, 0 < tolerance → ∃ approximant : ℕ, abs (readout.approximationErrorAt approximant) < tolerance def strictLocalConeWithoutNormDensity : ReducedQuasiLocalExtensionReadout := { strictLocalCommutatorNorm := 0 strictLocalBound := 0 approximationErrorAt := fun _ => 1 } theorem local_cone_bound_does_not_supply_quasi_local_extension : strictLocalConeBound strictLocalConeWithoutNormDensity ∧ ¬quasiLocalNormApproximation strictLocalConeWithoutNormDensity := by constructor · norm_num [strictLocalConeBound, strictLocalConeWithoutNormDensity] · intro approximation obtain ⟨approximant, impossible⟩ := approximation (1 / 2) (by norm_num) norm_num [strictLocalConeWithoutNormDensity] at impossible structure ReducedExponentialTailReadout where nearDistance : ℝ farDistance : ℝ nearInteractionNorm : ℝ farInteractionNorm : ℝ decayRate : ℝ refinementAdmissibilityResidual : ℝ def exponentialInteractionTail (readout : ReducedExponentialTailReadout) : Prop := 0 ≤ readout.nearDistance ∧ readout.nearDistance < readout.farDistance ∧ 0 < readout.nearInteractionNorm ∧ 0 < readout.decayRate ∧ readout.farInteractionNorm = readout.nearInteractionNorm * Real.exp (-readout.decayRate * (readout.farDistance - readout.nearDistance)) def exponentialRefinementClassMembership (readout : ReducedExponentialTailReadout) : Prop := readout.refinementAdmissibilityResidual = 0 noncomputable def exponentialTailOutsideRefinementClass : ReducedExponentialTailReadout := { nearDistance := 0 farDistance := 1 nearInteractionNorm := 1 farInteractionNorm := Real.exp (-1) decayRate := 1 refinementAdmissibilityResidual := 1 } theorem exponential_tail_does_not_supply_refinement_class_membership : exponentialInteractionTail exponentialTailOutsideRefinementClass ∧ ¬exponentialRefinementClassMembership exponentialTailOutsideRefinementClass := by norm_num [exponentialInteractionTail, exponentialRefinementClassMembership, exponentialTailOutsideRefinementClass] structure ReducedSlowerTailReadout where nearDistance : ℝ farDistance : ℝ nearInteractionNorm : ℝ farInteractionNorm : ℝ powerLawAmplitude : ℝ refinementAdmissibilityResidual : ℝ def slowerPowerLawInteractionTail (readout : ReducedSlowerTailReadout) : Prop := 0 ≤ readout.nearDistance ∧ readout.nearDistance < readout.farDistance ∧ 0 < readout.powerLawAmplitude ∧ readout.nearInteractionNorm * (1 + readout.nearDistance) = readout.powerLawAmplitude ∧ readout.farInteractionNorm * (1 + readout.farDistance) = readout.powerLawAmplitude ∧ 0 < readout.farInteractionNorm ∧ readout.farInteractionNorm < readout.nearInteractionNorm def slowerTailRefinementClassMembership (readout : ReducedSlowerTailReadout) : Prop := readout.refinementAdmissibilityResidual = 0 noncomputable def slowerTailOutsideRefinementClass : ReducedSlowerTailReadout := { nearDistance := 1 farDistance := 4 nearInteractionNorm := 1 / 2 farInteractionNorm := 1 / 5 powerLawAmplitude := 1 refinementAdmissibilityResidual := 1 } theorem slower_tail_does_not_supply_refinement_class_membership : slowerPowerLawInteractionTail slowerTailOutsideRefinementClass ∧ ¬slowerTailRefinementClassMembership slowerTailOutsideRefinementClass := by norm_num [slowerPowerLawInteractionTail, slowerTailRefinementClassMembership, slowerTailOutsideRefinementClass] structure ReducedDeferredTailReadout where interactionNorm : ℝ classMembershipResidual : ℝ dynamicsResidual : ℝ coneResidual : ℝ def admissibleTailSetup (readout : ReducedDeferredTailReadout) : Prop := 0 < readout.interactionNorm ∧ readout.classMembershipResidual = 0 ∧ readout.dynamicsResidual = 0 def directTailConeResult (readout : ReducedDeferredTailReadout) : Prop := readout.coneResidual = 0 def deferredTailCalculation (readout : ReducedDeferredTailReadout) : Prop := admissibleTailSetup readout → directTailConeResult readout def tailWithoutAdmissibleSetupOrCone : ReducedDeferredTailReadout := { interactionNorm := 1 classMembershipResidual := 1 dynamicsResidual := 1 coneResidual := 1 } theorem deferred_tail_contract_without_setup_has_no_direct_cone_result : ¬admissibleTailSetup tailWithoutAdmissibleSetupOrCone ∧ deferredTailCalculation tailWithoutAdmissibleSetupOrCone ∧ ¬directTailConeResult tailWithoutAdmissibleSetupOrCone := by norm_num [admissibleTailSetup, deferredTailCalculation, directTailConeResult, tailWithoutAdmissibleSetupOrCone] structure ReducedAsymptoticAbelianReadout where commutatorNormAt : ℕ → ℝ invariantMeanResidual : ℝ def asymptoticallyAbelianInCone (readout : ReducedAsymptoticAbelianReadout) : Prop := ∀ tolerance : ℝ, 0 < tolerance → ∃ cutoff : ℕ, ∀ sample : ℕ, cutoff ≤ sample → abs (readout.commutatorNormAt sample) < tolerance def invariantMeanEqualsProjection (readout : ReducedAsymptoticAbelianReadout) : Prop := readout.invariantMeanResidual = 0 def abelianConeWithoutInvariantMean : ReducedAsymptoticAbelianReadout := { commutatorNormAt := fun _ => 0 invariantMeanResidual := 1 } theorem asymptotic_abelianness_does_not_supply_invariant_mean_lemma : asymptoticallyAbelianInCone abelianConeWithoutInvariantMean ∧ ¬invariantMeanEqualsProjection abelianConeWithoutInvariantMean := by constructor · intro tolerance positive refine ⟨0, ?_⟩ intro sample afterCutoff simpa [abelianConeWithoutInvariantMean] using positive · norm_num [invariantMeanEqualsProjection, abelianConeWithoutInvariantMean] structure ReducedVelocityHierarchyReadout where trueVelocity : ℝ upperBoundAt : ℕ → ℝ def improvingVelocityUpperBounds (readout : ReducedVelocityHierarchyReadout) : Prop := 0 < readout.trueVelocity ∧ ∀ order : ℕ, readout.trueVelocity ≤ readout.upperBoundAt (order + 1) ∧ readout.upperBoundAt (order + 1) < readout.upperBoundAt order def hierarchyConvergesToTrueVelocity (readout : ReducedVelocityHierarchyReadout) : Prop := ∀ tolerance : ℝ, 0 < tolerance → ∃ cutoff : ℕ, ∀ order : ℕ, cutoff ≤ order → abs (readout.upperBoundAt order - readout.trueVelocity) < tolerance noncomputable def improvingBoundsWithPositiveAsymptoticGap : ReducedVelocityHierarchyReadout := { trueVelocity := 1 upperBoundAt := fun order => 2 + (1 / 2 : ℝ) ^ order } theorem crude_upper_bounds_need_not_converge_to_true_velocity : improvingVelocityUpperBounds improvingBoundsWithPositiveAsymptoticGap ∧ ¬hierarchyConvergesToTrueVelocity improvingBoundsWithPositiveAsymptoticGap := by constructor · constructor · norm_num [improvingBoundsWithPositiveAsymptoticGap] · intro order have positive : 0 < (1 / 2 : ℝ) ^ order := by positivity constructor · have nextPositive : 0 < (1 / 2 : ℝ) ^ (order + 1) := by positivity simp only [improvingBoundsWithPositiveAsymptoticGap] nlinarith · simp only [improvingBoundsWithPositiveAsymptoticGap, pow_succ] nlinarith · intro convergence obtain ⟨cutoff, close⟩ := convergence (1 / 2) (by norm_num) have impossible := close cutoff (le_refl cutoff) have nonnegative : 0 ≤ (1 / 2 : ℝ) ^ cutoff := by positivity norm_num [improvingBoundsWithPositiveAsymptoticGap] at impossible have insideNonnegative : 0 ≤ 2 + (1 / 2 : ℝ) ^ cutoff - 1 := by nlinarith rw [abs_of_nonneg insideNonnegative] at impossible nlinarith end Countermodels end PaperFramework end PhysicsLogic.Papers.LiebRobinson1972