P1: the field-structured flow — the definitional layer, stated against the bridge

Category: CV (continuous variables — P1's definitional half on top of the arena bridge).

eft-pillars-plan.md P1 asked for two things: the arena bridge (landed, CV/ArenaBridge.lean), and a definition — what it means for a flow to have field structure, i.e. a generator decomposing into mode-local pieces with a locality relation among them. This module supplies the definition and shows it is neither empty nor decorative:

• FieldStructuredFlow K N — a skew generator presented as a sum of graph-edge-supported pieces (piece_supported), with on-site terms as self-edges. F.gen, F.flow t (the one-parameter unitary family), and F.arenaFlow t (the induced flow on the record arena).
• flow_add / arenaFlow_add — the family is a genuine one-parameter flow, on the operators and on the arena alike (arenaKick_mul is the group-action law for kicks that makes the second follow from the first).
• ★★ FieldStructuredFlow.lightcone — the characterisation P1 asked for: every field-structured flow's arena action has the Lieb-Robinson cone. Not "the free flow" or "this drive": any flow admitting a local decomposition, as a property of the structure itself.
• Non-vacuity, twice, connected to the corpus's own drives rather than to toy witnesses: ★ freeFieldStructured with freeFieldStructured_flow_eq — the CV chain's free drive freeFieldU IS the flow of a field-structured generator (on-site pieces); and ★ graphStructured with graphStructured_flow_eq — the graph-interacting drive interactingU · (graphPotential E g) is likewise field-structured (on-site pieces plus one piece per coupling edge). So the flows the EFT chain has been studying all along are instances, and the arena light cone applies to them with no further hypotheses.

⚠️ Honest scope: this characterises flows whose generator is diagonal-local or edge-local in the given mode factorisation — field structure relative to a factorisation, which is all Route A can mean (the factorisation itself is epistemic; eft-pillars-plan.md P3). The fibre-active arenas are covered in CV/FibredArenaBridge.lean (the record stroke and its cone, 2026-08-20).

References

specs/eft-pillars-plan.md (P1); specs/arena-bridge-plan.md; CV/ArenaBridge.lean (the transport); CV/FreeFieldFloquet.lean (freeFieldU_eq_exp); CV/Interaction.lean (interactingU_eq_exp, interactionHamiltonian); CV/SupportSpreading.lean (graphPotential); CV/LocalAlgebra.lean (SupportedOn.smul).

Diagonal matrices are supported where they read

theorem CSD.CV.supportedOn_diagonal_pair {K N : ℕ} (a b : Fin K) (g : Fin N → Fin N → ℂ) : SupportedOn {a, b} (Matrix.diagonal fun (c : FieldConfig K N) => g (c a) (c b))

A diagonal matrix whose entry reads only modes a and b is supported on {a, b}. On-site terms are the case a = b.

theorem CSD.CV.matrix_real_smul {K N : ℕ} (r : ℝ) (M : Matrix (FieldConfig K N) (FieldConfig K N) ℂ) : r • M = ↑r • M

A real scalar action on a complex matrix is the complex action of its cast — the normal form the witness computations use.

theorem CSD.CV.skew_neg_I_smul_of_hermitian {K N : ℕ} (τ : ℝ) {H : Matrix (FieldConfig K N) (FieldConfig K N) ℂ} (hH : H.conjTranspose = H) : (-(Complex.I * ↑τ) • H).conjTranspose = -(-(Complex.I * ↑τ) • H)

The skew of a phase generator: (-(iτ)) • H is skew-Hermitian for Hermitian H.

The structure

structure CSD.CV.FieldStructuredFlow (K N : ℕ) : Type

A field-structured flow: a skew generator presented as a sum of graph-local pieces — one matrix per edge, each supported on its edge's two modes, with on-site terms as self-edges (k, k). This is P1's definitional object: what it means for a flow on the field to have field structure.

• edges : Finset (Fin K × Fin K)

  The interaction graph: coupling edges, with self-edges as on-site terms.

• piece : Fin K × Fin K → Matrix (FieldConfig K N) (FieldConfig K N) ℂ

  The local generator pieces, one per edge.

• piece_supported (e : Fin K × Fin K) : e ∈ self.edges → SupportedOn {e.1, e.2} (self.piece e)

  Each piece lives on its own edge.

• gen_skew : (∑ e ∈ self.edges, self.piece e).conjTranspose = -∑ e ∈ self.edges, self.piece e

  The assembled generator is skew-Hermitian.

noncomputable def CSD.CV.FieldStructuredFlow.gen {K N : ℕ} (F : FieldStructuredFlow K N) : Matrix (FieldConfig K N) (FieldConfig K N) ℂ

The assembled generator.

Equations

• F.gen = ∑ e ∈ F.edges, F.piece e

@[simp]

theorem CSD.CV.FieldStructuredFlow.gen_def {K N : ℕ} (F : FieldStructuredFlow K N) : F.gen = ∑ e ∈ F.edges, F.piece e

noncomputable def CSD.CV.FieldStructuredFlow.flow {K N : ℕ} (F : FieldStructuredFlow K N) (t : ℝ) : ↥(Matrix.unitaryGroup (FieldConfig K N) ℂ)

The one-parameter unitary family exp(t • gen).

Equations

• F.flow t = CSD.CV.flowU ⋯ t

@[simp]

theorem CSD.CV.FieldStructuredFlow.flow_val {K N : ℕ} (F : FieldStructuredFlow K N) (t : ℝ) : ↑(F.flow t) = NormedSpace.exp (t • ∑ e ∈ F.edges, F.piece e)

theorem CSD.CV.FieldStructuredFlow.flow_add {K N : ℕ} (F : FieldStructuredFlow K N) (s t : ℝ) : F.flow (s + t) = F.flow s * F.flow t

The family is a genuine one-parameter group.

noncomputable def CSD.CV.FieldStructuredFlow.arenaFlow {K N : ℕ} (F : FieldStructuredFlow K N) (t : ℝ) (p : FieldArena K N) : FieldArena K N

The induced flow on the record arena.

Equations

• F.arenaFlow t p = CSD.CV.arenaKick (F.flow t) p

Kicks compose, so the arena flow is a flow

theorem CSD.CV.arenaKick_mul {K N : ℕ} (U V : ↥(Matrix.unitaryGroup (FieldConfig K N) ℂ)) (p : FieldArena K N) : arenaKick (U * V) p = arenaKick U (arenaKick V p)

Kicks compose: the arena action respects the group law.

theorem CSD.CV.FieldStructuredFlow.arenaFlow_add {K N : ℕ} (F : FieldStructuredFlow K N) (s t : ℝ) (p : FieldArena K N) : F.arenaFlow (s + t) p = F.arenaFlow s (F.arenaFlow t p)

The arena flow is a one-parameter flow on the arena.

The characterisation: every field-structured flow has the cone

theorem CSD.CV.FieldStructuredFlow.lightcone {K N : ℕ} (F : FieldStructuredFlow K N) [NeZero N] {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 : ℕ} (hcone : Disjoint (graphBall F.edges R d) Y) {t : ℝ} (ht : 0 ≤ t) (p : FieldArena K N) : |arenaObs A (F.arenaFlow t (arenaKick W p)) - arenaObs A (F.arenaFlow t p)| ≤ 2 * ((2 * ‖∑ e ∈ F.edges, F.piece e‖ * t) ^ d / ↑d.factorial) * ‖A‖

★★ P1's characterisation: every field-structured flow's arena action has the Lieb-Robinson cone. A kick supported outside the graph d-ball of region R (in the flow's own interaction graph) changes any region-R arena observable after time t by at most the factorial tail. Field structure — a locally-decomposed generator — is exactly what buys a light cone at the record arena, and it buys it for every such flow, not for a chosen drive.

Non-vacuity: the corpus's own drives are field-structured

noncomputable def CSD.CV.oscHamAt {K N : ℕ} (k : Fin K) : Matrix (FieldConfig K N) (FieldConfig K N) ℂ

The single-mode energy Hamiltonian, placed at mode k.

Equations

• CSD.CV.oscHamAt k = Matrix.diagonal fun (c : CSD.CV.FieldConfig K N) => ↑(CSD.CV.oscEnergy ↑(c k))

theorem CSD.CV.oscHamAt_hermitian {K N : ℕ} (k : Fin K) : (oscHamAt k).conjTranspose = oscHamAt k

theorem CSD.CV.sum_oscHamAt {K N : ℕ} : ∑ k : Fin K, oscHamAt k = fieldHamiltonian K N

The on-site Hamiltonians assemble to the free-field Hamiltonian.

noncomputable def CSD.CV.freeFieldStructured (K N : ℕ) (τ : ℝ) : FieldStructuredFlow K N

★ The free field is field-structured: on-site pieces only (self-edges), one per mode.

Equations

• One or more equations did not get rendered due to their size.

theorem CSD.CV.freeFieldStructured_flow_eq {K N : ℕ} (τ t : ℝ) : ↑((freeFieldStructured K N τ).flow t) = ↑(freeFieldU K N (τ * t))

The structured free flow IS the CV chain's free drive: flow t equals freeFieldU at the accumulated phase τ·t. The definitional layer captures the existing drive rather than a parallel object.

noncomputable def CSD.CV.edgeHamAt {K N : ℕ} (g : Fin K × Fin K → Fin N → Fin N → ℝ) (e : Fin K × Fin K) : Matrix (FieldConfig K N) (FieldConfig K N) ℂ

The edge Hamiltonian of a graph coupling.

Equations

• CSD.CV.edgeHamAt g e = Matrix.diagonal fun (c : CSD.CV.FieldConfig K N) => ↑(g e (c e.1) (c e.2))

theorem CSD.CV.edgeHamAt_hermitian {K N : ℕ} (g : Fin K × Fin K → Fin N → Fin N → ℝ) (e : Fin K × Fin K) : (edgeHamAt g e).conjTranspose = edgeHamAt g e

theorem CSD.CV.sum_edgeHamAt {K N : ℕ} (E : Finset (Fin K × Fin K)) (g : Fin K × Fin K → Fin N → Fin N → ℝ) : ∑ e ∈ E, edgeHamAt g e = interactionHamiltonian (graphPotential E g)

The edge Hamiltonians assemble to the graph interaction Hamiltonian.

noncomputable def CSD.CV.graphStructured (K N : ℕ) (τ lam : ℝ) (E : Finset (Fin K × Fin K)) (g : Fin K × Fin K → Fin N → Fin N → ℝ) : FieldStructuredFlow K N

★ The graph-interacting drive is field-structured: on-site pieces plus one piece per coupling edge. (The no-self-loops hypothesis appears only on the identification with interactingU, where the two edge families must not collide; the structure itself needs no such condition.)

Equations

• One or more equations did not get rendered due to their size.

theorem CSD.CV.graphStructured_flow_eq {K N : ℕ} (τ lam t : ℝ) (E : Finset (Fin K × Fin K)) (g : Fin K × Fin K → Fin N → Fin N → ℝ) (hE : ∀ e ∈ E, e.1 ≠ e.2) : ↑((graphStructured K N τ lam E g).flow t) = ↑(interactingU K N (τ * t) lam (graphPotential E g))

The structured graph flow IS the CV chain's interacting drive at the graph potential: flow t equals interactingU at the accumulated phase τ·t, with the same coupling λ. The arena light cone therefore applies to the corpus's interacting dynamics with no further hypotheses.