The two cones: the record cone inside a kinematic cone

Category: 3-Local (CV; continuous variables — relativistic structure forced, not defined). BACKLOG #98, out of #39.

The corpus had two cone structures that were never related:

• the record cone — graphBall on the coupling graph, and the Lieb–Robinson bound ★★ record_lightcone of FibredArenaBridge.lean, whose error term is (2‖S‖t)^d / d! at graph separation d;
• the kinematic cone of DispersionEarned.lean, where ★ cone_preserving_is_boost earns the boost group and ★★ cone_symmetry_characterises_omega then selects ω = √(p² + m²).

Three facts about the starting point, established by reading the corpus rather than assumed:

1. There was no cone object anywhere. record_lightcone and FieldStructuredFlow.lightcone are theorem names; DispersionEarned's "cone" is the pair of light rays E = ±p, entering only as the hypotheses a + b = c + d and a − b = d − c. There was nothing with a slope for the record cone to sit inside. forwardCone is that object.
2. There was no map from sites to space. graphBall lives on Fin K with integer hop counts, and the coupling graph carries no geometry. SiteEmbedding posits one, with a bound hop on the length of an edge. ⚠️ Note that Fin K is read as a momentum label in Dispersion.lean and as a graph site label in SupportSpreading.lean; everything here takes the site reading, and the embedding is of sites into position space.
3. The factorial bound needed is already in Mathlib: Stirling.le_factorial_stirling, which holds for all n with no largeness hypothesis.

What is proved

• forwardCone V v — {(t, x) | ‖x‖ ≤ v·t, 0 ≤ t}, the forward cone of slope v over any seminormed space, with forwardCone_mono in the slope;
• ★ exists_dist_le_of_mem_graphBall — the geometric containment: a site d hops from R is within d · hop of R in the embedding, by induction on hops. Hence ★★ mem_forwardCone_of_mem_graphBall: with a time step τ > 0, the n-step record cone embeds in the forward cone of slope hop/τ, which is the statement #98 asked for;
• ★ disjoint_graphBall_of_separated — the contrapositive, and the usable direction: sites Euclidean-far from R are outside the graph ball, so record_lightcone's hypothesis is discharged by geometry;
• ★ pow_div_factorial_le — x^d/d! ≤ (e·x/d)^d, from Stirling.le_factorial_stirling; hence ★★ lr_bound_le_half_pow: once d ≥ lrVelocity · t the Lieb–Robinson error is at most 2^{-d}. lrVelocity F = 4e‖S‖ is the cone's slope in hops per unit time;
• ★★★ record_influence_le_of_separated — the capstone: a record written in R cannot be steered from a region whose sites are farther than d · hop from R, to within L_h L_g · 2 · 2^{-d} · ‖A‖, whenever d ≥ lrVelocity · t. Geometric separation in the embedding gives geometric suppression, with the velocity appearing as a slope;
• ★★ forwardCone_eq_nonnegSpan and ★★ mapsTo_forwardCone_of_rays — the cone of slope v is the non-negative span of its two null rays, so a linear map fixing both rays forward preserves the cone;
• ★★★ forwardCone_rays_is_boost — the link to DispersionEarned: rescaling x ↦ x/v carries the slope-v cone to the slope-1 cone, so a unimodular ray-preserving map of the slope-v cone is a boost at some rapidity. This is what makes the containment touch the kinematic side at theorem level rather than in prose;
• ★★★ slope_cone_symmetry_characterises_omega — and therefore the slope is immaterial to P4: for any v > 0, covariance under the unimodular symmetries of the slope-v cone plus rest energy m forces ω = omega m. So the Lieb–Robinson velocity can be the kinematic cone's slope without changing the dispersion that P4 selects.

Honest scope

⚠️ This is a containment, never an identification. The record cone is shown to sit inside a kinematic cone and the two cones' symmetry groups are shown to be the same group; the two cones are not identified, and nothing here says the Lieb–Robinson velocity is a limiting speed. An identification needs a continuum limit of the graph dynamics that the corpus does not have, and must not be read into any statement below.

⚠️ The embedding is posited, and so is the time step. SiteEmbedding is data supplied by the user of these theorems, not constructed: nothing derives a spatial arrangement of the coupling graph from the dynamics, and τ is a conversion factor, not a derived lattice spacing in time. Every "slope" below is therefore hop/τ or 4e‖S‖ in whatever units the embedding was given.

⚠️ lrVelocity is an upper bound with a model-dependent constant, read off record_lightcone's own error term. The 4e is what the Stirling bound gives at the chosen suppression 2^{-d}; it is not sharp, and Stirling.factorial_isEquivalent_stirling would be the route to a sharper constant. No claim is made that it is the smallest velocity that works.

⚠️ One spatial dimension on the kinematic side. forwardCone is stated over any seminormed space, but the ray decomposition, the boost link and the ω corollary are V = ℝ: the (E, p) plane of DispersionEarned is two-dimensional, so the symmetry statements are 1 + 1. Nothing here extends the boost link to higher dimensions.

⚠️ The (E, p)/(t, x) relabelling is explicit, not a derivation. cone_preserving_is_boost is a statement about linear maps of a plane preserving two rays; applying it to (t, x) is a relabelling of that plane, exactly as DispersionEarned's own header warns. No duality between position and momentum space is constructed or needed.

References: records-to-spacetime-scoping.md; future-work.md; eft-pillars-plan.md P4; CV/DispersionEarned.lean, CV/FibredArenaBridge.lean, CV/SupportSpreading.lean, CV/RecordInfluence.lean; specs/BACKLOG.md #98, #39, #38.

The forward cone of slope v

def CSD.CV.forwardCone (V : Type u_1) [SeminormedAddCommGroup V] (v : ℝ) : Set (ℝ × V)

The forward cone of slope v over a seminormed space: the pairs (t, x) of an elapsed time and a displacement with ‖x‖ ≤ v · t. The object the corpus did not have — record_lightcone and cone_preserving_is_boost both speak of a cone without one.

Equations

• CSD.CV.forwardCone V v = {q : ℝ × V | ‖q.2‖ ≤ v * q.1 ∧ 0 ≤ q.1}

@[simp]

theorem CSD.CV.mem_forwardCone {V : Type u_1} [SeminormedAddCommGroup V] {v : ℝ} {q : ℝ × V} : q ∈ forwardCone V v ↔ ‖q.2‖ ≤ v * q.1 ∧ 0 ≤ q.1

theorem CSD.CV.forwardCone_mono {V : Type u_1} [SeminormedAddCommGroup V] {v w : ℝ} (h : v ≤ w) : forwardCone V v ⊆ forwardCone V w

theorem CSD.CV.zero_mem_forwardCone {V : Type u_1} [SeminormedAddCommGroup V] {v : ℝ} : (0, 0) ∈ forwardCone V v

A posited embedding of the coupling graph into space

structure CSD.CV.SiteEmbedding (K : ℕ) (V : Type u_2) [SeminormedAddCommGroup V] (edges : Finset (Fin K × Fin K)) : Type u_2

A spatial arrangement of the coupling graph. Positions for the sites and a bound hop on the length of a coupling edge. ⚠️ This is data, not a construction: nothing in the corpus derives a spatial arrangement from the dynamics, and the graph itself carries no geometry.

• pos : Fin K → V

  The position of each site.

• hop : ℝ

  The bound on the length of a coupling edge.

• hop_nonneg : 0 ≤ self.hop

  The bound is non-negative.

• edge_le (e : Fin K × Fin K) : e ∈ edges → ‖self.pos e.1 - self.pos e.2‖ ≤ self.hop

  Every coupling edge joins sites within hop of each other.

theorem CSD.CV.SiteEmbedding.edge_le' {K : ℕ} {V : Type u_1} [SeminormedAddCommGroup V] {edges : Finset (Fin K × Fin K)} (emb : SiteEmbedding K V edges) {e : Fin K × Fin K} (he : e ∈ edges) : ‖emb.pos e.2 - emb.pos e.1‖ ≤ emb.hop

The geometric containment

theorem CSD.CV.exists_dist_le_of_mem_graphBall {K : ℕ} {V : Type u_1} [SeminormedAddCommGroup V] {edges : Finset (Fin K × Fin K)} (emb : SiteEmbedding K V edges) (R : Finset (Fin K)) (n : ℕ) {k : Fin K} : k ∈ graphBall edges R n → ∃ r ∈ R, ‖emb.pos k - emb.pos r‖ ≤ ↑n * emb.hop

★ A site n hops from R is within n · hop of R in the embedding. Induction on hops: one step of graphNeighborhood either stays put or crosses one edge, and an edge is short by hypothesis. This is the whole geometric content of #98.

theorem CSD.CV.mem_forwardCone_of_mem_graphBall {K : ℕ} {V : Type u_1} [SeminormedAddCommGroup V] {edges : Finset (Fin K × Fin K)} (emb : SiteEmbedding K V edges) (R : Finset (Fin K)) {τ : ℝ} (hτ : 0 < τ) (n : ℕ) {k : Fin K} (hk : k ∈ graphBall edges R n) : ∃ r ∈ R, (↑n * τ, emb.pos k - emb.pos r) ∈ forwardCone V (emb.hop / τ)

★★ The record cone embeds in the forward cone of slope hop/τ. With a time step τ > 0, a site reached in n steps sits, relative to some site of R, at a displacement–time pair inside the forward cone whose slope is one hop per time step. This is #98's containment.

theorem CSD.CV.notMem_forwardCone_of_lt {V : Type u_1} [SeminormedAddCommGroup V] {v t : ℝ} {x : V} (h : v * t < ‖x‖) : (t, x) ∉ forwardCone V v

A displacement longer than the cone allows is outside the cone.

theorem CSD.CV.disjoint_graphBall_of_notMem_forwardCone {K : ℕ} {V : Type u_1} [SeminormedAddCommGroup V] {edges : Finset (Fin K × Fin K)} (emb : SiteEmbedding K V edges) (R Y : Finset (Fin K)) {τ : ℝ} (hτ : 0 < τ) (n : ℕ) (hout : ∀ y ∈ Y, ∀ r ∈ R, (↑n * τ, emb.pos y - emb.pos r) ∉ forwardCone V (emb.hop / τ)) : Disjoint (graphBall edges R n) Y

★★ Outside the cone is outside the record cone. The contrapositive of the containment, in cone language: a region no point of which is in the forward cone of slope hop/τ over R is disjoint from the n-step record cone. This is what discharges record_lightcone's Disjoint hypothesis geometrically.

theorem CSD.CV.disjoint_graphBall_of_separated {K : ℕ} {V : Type u_1} [SeminormedAddCommGroup V] {edges : Finset (Fin K × Fin K)} (emb : SiteEmbedding K V edges) (R Y : Finset (Fin K)) (n : ℕ) (hsep : ∀ y ∈ Y, ∀ r ∈ R, ↑n * emb.hop < ‖emb.pos y - emb.pos r‖) : Disjoint (graphBall edges R n) Y

★ Euclidean separation puts a region outside the record cone. The practical form of disjoint_graphBall_of_notMem_forwardCone: supply distances, not cone memberships. The time step cancels, so the condition is the hop-count one, n · hop.

The Lieb–Robinson velocity, from Stirling's bound

theorem CSD.CV.pow_div_factorial_le {x : ℝ} (hx : 0 ≤ x) {d : ℕ} (hd : 1 ≤ d) : x ^ d / ↑d.factorial ≤ (Real.exp 1 * x / ↑d) ^ d

★ x^d/d! ≤ (e·x/d)^d. The factorial lower bound is Stirling.le_factorial_stirling, which holds for every n; the √(2πd) factor is at least one for d ≥ 1 and is discarded.

noncomputable def CSD.CV.lrVelocity {K N : ℕ} (F : FieldStructuredFlow K N) : ℝ

The Lieb–Robinson velocity of a structured flow, in hops per unit time: the slope at which record_lightcone's error term is suppressed by 2^{-d}. ⚠️ An upper bound with the constant that the Stirling estimate happens to give at that suppression, not a sharp speed.

Equations

• CSD.CV.lrVelocity F = 4 * Real.exp 1 * ‖∑ e ∈ F.edges, F.piece e‖

theorem CSD.CV.lrVelocity_nonneg {K N : ℕ} (F : FieldStructuredFlow K N) : 0 ≤ lrVelocity F

theorem CSD.CV.lr_bound_le_half_pow {S t : ℝ} (hS : 0 ≤ S) (ht : 0 ≤ t) {d : ℕ} (hd : 1 ≤ d) (hvt : 4 * Real.exp 1 * S * t ≤ ↑d) : (2 * S * t) ^ d / ↑d.factorial ≤ (1 / 2) ^ d

★★ Outside the cone of slope lrVelocity, the Lieb–Robinson error is at most 2^{-d}. The inequality that turns record_lightcone's factorial bound into a statement about a cone: the suppression sets in exactly once the separation exceeds the velocity times the elapsed time.

The capstone: separation in space, suppression in the record

theorem CSD.CV.record_influence_le_of_separated {K N : ℕ} {V : Type u_1} [SeminormedAddCommGroup V] [NeZero N] (F : FieldStructuredFlow K N) {edges : Finset (Fin K × Fin K)} (hedges : edges = F.edges) (emb : SiteEmbedding K V edges) {R Y : Finset (Fin K)} {A : Matrix (FieldConfig K N) (FieldConfig K N) ℂ} (hA : SupportedOn R A) {W : ↥(Matrix.unitaryGroup (FieldConfig K N) ℂ)} (hW : SupportedOn Y ↑W) {d : ℕ} (hd : 1 ≤ d) (hsep : ∀ y ∈ Y, ∀ r ∈ R, ↑d * emb.hop < ‖emb.pos y - emb.pos r‖) {t : ℝ} (ht : 0 ≤ t) (hvt : lrVelocity F * t ≤ ↑d) {Lh Lg : NNReal} {h : RecordFibre → ℝ} (hh : LipschitzWith Lh h) {g : ℝ → RecordFibre} (hg : LipschitzWith Lg g) (ω : ℝ × ℝ) (x : FibredFieldArena K N) : |h (recordStroke A g (F.fibredFlow ω t (fibredKick W x))).2 - h (recordStroke A g (F.fibredFlow ω t x)).2| ≤ ↑Lh * ↑Lg * (2 * (1 / 2) ^ d * ‖A‖)

★★★ A record cannot be steered from outside the kinematic cone. The Lieb–Robinson cone of ★★ record_lightcone is here read through the embedding: if every site of the kicking region Y is farther than d · hop from the read region R, and the elapsed time satisfies lrVelocity F · t ≤ d, then the record readout differs from the unkicked one by at most L_h L_g · 2 · 2^{-d} · ‖A‖. Geometric separation in space gives geometric suppression in the record, and the velocity enters as the slope of the cone.

⚠️ Containment, not identification: this says the record cone sits inside a cone of slope lrVelocity F · hop, not that the two cones coincide, and not that lrVelocity is a limiting speed.

The cone's symmetries are the boosts, at every slope

theorem CSD.CV.forwardCone_eq_nonnegSpan {v : ℝ} (hv : 0 < v) (q : ℝ × ℝ) : q ∈ forwardCone ℝ v ↔ ∃ (s : ℝ) (u : ℝ), 0 ≤ s ∧ 0 ≤ u ∧ q = (s + u, v * s - v * u)

★★ The forward cone of slope v is the non-negative span of its two null rays. The decomposition that makes "fixes both rays" imply "preserves the cone".

theorem CSD.CV.mapsTo_forwardCone_of_rays {v : ℝ} (hv : 0 < v) {a b c d : ℝ} (hRpos : 0 < a + b * v) (hR : c + d * v = v * (a + b * v)) (hLpos : 0 < a - b * v) (hL : c - d * v = -v * (a - b * v)) : Set.MapsTo (fun (q : ℝ × ℝ) => (a * q.1 + b * q.2, c * q.1 + d * q.2)) (forwardCone ℝ v) (forwardCone ℝ v)

★★ A linear map fixing both null rays forward preserves the cone. The hypotheses say the map sends (1, v) to a positive multiple of itself and (1, −v) likewise; the cone is their non-negative span, so it is preserved.

theorem CSD.CV.forwardCone_rays_is_boost {v : ℝ} (hv : 0 < v) {a b c d : ℝ} (hR : c + d * v = v * (a + b * v)) (hRpos : 0 < a + b * v) (hL : c - d * v = -v * (a - b * v)) (hLpos : 0 < a - b * v) (hdet : a * d - b * c = 1) : ∃ (χ : ℝ), ∀ (t x : ℝ), a * t + b * x = boostE χ t (x / v) ∧ (c * t + d * x) / v = boostP χ t (x / v)

★★★ The symmetries of a cone of slope v are the boosts. Rescaling x ↦ x/v carries the slope-v cone to the slope-1 cone, and DispersionEarned.lean's ★ cone_preserving_is_boost then applies: a unimodular linear map fixing both null rays of the slope-v cone is the boost at some rapidity, read in the rescaled coordinate. This is the theorem-level link between the record cone's slope and the kinematic side.

⚠️ Reading the plane (t, x) as the (E, p) plane is a relabelling, exactly as DispersionEarned's own header says; no position/momentum duality is constructed.

theorem CSD.CV.slope_cone_symmetry_characterises_omega {ω : ℝ → ℝ} {m v : ℝ} (hm : 0 < m) (hv : 0 < v) (h0 : ω 0 = m) (hcov : ∀ (a b c d : ℝ), 0 < a + b * v → c + d * v = v * (a + b * v) → 0 < a - b * v → c - d * v = -v * (a - b * v) → a * d - b * c = 1 → ∀ (p : ℝ), a * ω p + b * v * p = ω (c / v * ω p + d * p)) : ω = omega m

★★★ The cone's slope is immaterial to the dispersion P4 selects. For any v > 0, a dispersion with rest energy m that is covariant under every unimodular symmetry of the slope-v cone is ω = √(p² + m²). So the Lieb–Robinson velocity may be taken as the kinematic cone's slope without changing what cone_symmetry_characterises_omega forces — which is what makes the containment of record_influence_le_of_separated compatible with P4 rather than merely adjacent to it.