P1, closed: the fibre-active extension — records in the fibre inherit the cone

Category: CV (continuous variables — the fibred completion of the arena bridge; P1's last item).

Glossary: https://glossary.constraintsurfacedynamics.com/record-light-cone/ Plain-language, CSD-role and formal statements of the record light cone, with this module as the Lean anchor. Kept symmetric by scripts/check-glossary.sh.

ArenaBridge.lean carried operator locality onto the projective base; FieldStructuredFlow.lean made field structure a definition whose every instance has the cone there. What remained of P1 was the fibre: the record layer's arenas are fibred (Σ = ℂℙ^{N-1} × T², LF4.KSigma), and the record-forming content lives in the fibre — for N ≥ 3 it must (specs/sigma-fibre-contextuality.md). The corpus's record mechanism (RecordLayer/ShearWitness.lean) is a skew stroke: base held fixed, fibre translated by a base-dependent Haar shift. This module covers exactly that shape.

• RecordFibre — the flat torus (ℝ/ℤ)², definitionally LF4.KTorus, so the record layer consumes these statements with no glue.
• FibredFieldArena K N — base × fibre; fibredKick (mode-localised interventions act on the field factor — the fibre is the record medium); FieldStructuredFlow.fibredFlow (base evolves, fibre rotates rigidly).
• recordStroke A g — the record write: fibre translated by g (arenaObs A ·), a base-dependent shift factoring through a region-S arena observable. This is the ShearWitness skew-product shape with the base-reading realised through the bridge.
• fibredObs A h — fibre-carrying observables arenaObs A p · h θ, with ★ fibredObs_kick_of_disjointSupport the exact statics.
• ★ recordStroke_comm_kick — interventions outside the read region commute with record writing, exactly. The record cannot tell whether a disjointly supported kick happened before or after it was written.
• ★★ record_lightcone — the fibre-active record cone, closing P1: kick outside the graph d-ball of the record's read region, evolve under any field-structured flow, write the record, read any Lipschitz fibre observable — and the readout differs from the unkicked run by at most L_h · L_g · 2(2‖S‖t)^d/d! · ‖A‖. The record cell a trajectory lands in — a fibre fact — cannot be steered from outside the cone, with the write and read Lipschitz constants as the only new prices.

⚠️ Honest scope: fibre activity here is the stroke shape — base-dependent fibre shifts (the corpus's own record mechanism), with base-readings factoring through region-supported arena observables and Lipschitz write/read maps. Continuous-time skew flows whose fibre velocity is base-coupled are a stronger class and are not claimed here; nothing in the record layer currently needs them, and covering them would be a new scoping decision, not the discharge of this boundary.

References

specs/eft-pillars-plan.md (P1); specs/arena-bridge-plan.md; CV/ArenaBridge.lean; CV/FieldStructuredFlow.lean; RecordLayer/ShearWitness.lean (the skew stroke this covers); LF4/KahlerInstance.lean (KTorus, KSigma — RecordFibre is the same type); specs/sigma-fibre-contextuality.md (why the fibre is load-bearing).

The fibred arena

@[reducible, inline]

abbrev CSD.CV.RecordFibre : Type

The record fibre: the flat torus (ℝ/ℤ)². Definitionally the same type as LF4.KTorus, so record-layer consumers need no glue.

Equations

• CSD.CV.RecordFibre = (AddCircle 1 × AddCircle 1)

@[reducible, inline]

abbrev CSD.CV.FibredFieldArena (K N : ℕ) : Type

The fibred field arena: projective base × record fibre — the field-side analogue of LF4.KSigma.

Equations

• CSD.CV.FibredFieldArena K N = (CSD.CV.FieldArena K N × CSD.CV.RecordFibre)

noncomputable def CSD.CV.fibredKick {K N : ℕ} (W : ↥(Matrix.unitaryGroup (FieldConfig K N) ℂ)) (x : FibredFieldArena K N) : FibredFieldArena K N

A mode-localised intervention acts on the field factor; the fibre is the record medium and is not written by interventions.

Equations

• CSD.CV.fibredKick W x = (CSD.CV.arenaKick W x.1, x.2)

noncomputable def CSD.CV.FieldStructuredFlow.fibredFlow {K N : ℕ} (F : FieldStructuredFlow K N) (ω : ℝ × ℝ) (t : ℝ) (x : FibredFieldArena K N) : FibredFieldArena K N

The fibred flow of a field-structured generator: the base evolves, the fibre rotates rigidly at velocity ω.

Equations

• F.fibredFlow ω t x = (F.arenaFlow t x.1, x.2.1 + ↑(t * ω.1), x.2.2 + ↑(t * ω.2))

noncomputable def CSD.CV.recordStroke {K N : ℕ} (A : Matrix (FieldConfig K N) (FieldConfig K N) ℂ) (g : ℝ → RecordFibre) (x : FibredFieldArena K N) : FibredFieldArena K N

The record stroke: the fibre is translated by a base-dependent shift factoring through the arena observable of A — the ShearWitness skew-product shape, with the base-reading realised through the bridge.

Equations

• CSD.CV.recordStroke A g x = (x.1, x.2 + g (CSD.CV.arenaObs A x.1))

Fibre-carrying observables and exact statics

noncomputable def CSD.CV.fibredObs {K N : ℕ} (A : Matrix (FieldConfig K N) (FieldConfig K N) ℂ) (h : RecordFibre → ℝ) (x : FibredFieldArena K N) : ℝ

A fibre-carrying observable: a matrix observable on the base times an arbitrary reading of the fibre. Born-cell indicators are the case A = 1.

Equations

• CSD.CV.fibredObs A h x = CSD.CV.arenaObs A x.1 * h x.2

theorem CSD.CV.fibredObs_kick_of_disjointSupport {K N : ℕ} [NeZero N] {S T : Finset (Fin K)} (hST : Disjoint S T) {A : Matrix (FieldConfig K N) (FieldConfig K N) ℂ} (hA : SupportedOn S A) {W : ↥(Matrix.unitaryGroup (FieldConfig K N) ℂ)} (hW : SupportedOn T ↑W) (h : RecordFibre → ℝ) (x : FibredFieldArena K N) : fibredObs A h (fibredKick W x) = fibredObs A h x

★ Exact statics on the fibred arena: a fibre-carrying observable whose base part is supported on S is exactly invariant under kicks supported on disjoint T — the kick touches neither the region nor the fibre.

theorem CSD.CV.recordStroke_comm_kick {K N : ℕ} [NeZero N] {S T : Finset (Fin K)} (hST : Disjoint S T) {A : Matrix (FieldConfig K N) (FieldConfig K N) ℂ} (hA : SupportedOn S A) {W : ↥(Matrix.unitaryGroup (FieldConfig K N) ℂ)} (hW : SupportedOn T ↑W) (g : ℝ → RecordFibre) (x : FibredFieldArena K N) : recordStroke A g (fibredKick W x) = fibredKick W (recordStroke A g x)

★ Interventions outside the read region commute with record writing — exactly. Kick then write, or write then kick: the record cannot tell, because the stroke's base-reading is invariant under the disjoint kick and the kick does not touch the fibre.

The fibre-active record cone

theorem CSD.CV.record_lightcone {K N : ℕ} [NeZero N] (F : FieldStructuredFlow K 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) {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 * ((2 * ‖∑ e ∈ F.edges, F.piece e‖ * t) ^ d / ↑d.factorial) * ‖A‖)

★★ The record cone — P1's closing theorem. Kick outside the graph d-ball of the record's read region R, evolve for time t under any field-structured flow, write the record (a fibre shift reading region R through A), then read any Lipschitz observable of the fibre. The readout differs from the unkicked run by at most

L_h · L_g · 2·(2‖S‖t)^d/d! · ‖A‖.

The record cell the trajectory lands in — a fibre fact, and the fibre is where the corpus places the record-forming content for N ≥ 3 (one natural class of base candidate is refuted, not every candidate: specs/sigma-fibre-contextuality.md) — cannot be steered from outside the cone. The write map's and read map's Lipschitz constants are the only prices added to the base cone, and the rigid fibre rotation drops out because it is common to both histories.