CV/FieldModes: a free scalar field at a cutoff as a product of modes (EFT Stage 1)

Category: 3-Local (CV; continuous variables — the multi-mode field).

Stage 1 of the EFT direction: a free field at a cutoff = finitely many modes, each a truncated oscillator. The field Hilbert space is the (truncated) tensor product of the single-mode spaces, indexed by occupation configurations c : Fin K → Fin N (mode k has c k quanta): FieldSpace K N = EuclideanSpace ℂ (FieldConfig K N).

• fieldEnergy / fieldHamiltonian / fieldHamiltonian_mulVec_single — the free-field Hamiltonian is the sum of the single-mode Hamiltonians: diagonal in the configuration basis with eigenvalue fieldEnergy c = ∑ₖ oscEnergy (c k) (free field = sum of oscillators);
• fieldEnergy_cutoff_independent — the field energy of a configuration is cutoff-independent (the multi-mode analogue of oscEnergy_cutoff_independent);

Honest residue for the CV track

⚠️ CV has no root module, so EMPIRICAL.md's honest-residue paragraph is carried here, at the field-side entry point (CR-8, 2026-09-05).

The concrete SectorData instances behind the CV volume readings still carry Φ = id — LF5 exercises a genuine Φ_vN ≠ id only on the dilated Σ', not in these instances — so these readings remain realisation, not derivation. The Born value is derived from the posited sector geometry on Σ, which is the standing assumption these results rest on. The Born content additionally rests on the record layer's cell law: a posit with a characterisation (specs/POSITS.md Posit 1; torus generation pins the rate field, torus invariance does not). And the locality proved on this track is mode-disjoint commutation, not the Haag–Kastler axiom — mode sets, no net, no covariance (CV/ModeLocality.lean).

• fieldBornProb / sum_fieldBornProb_unit — the full-configuration measurement is a standard-basis (record-layer) measurement: ‖⟨c|Ψ⟩‖², a probability distribution over configurations;
• tprodState / norm_sq_tprodState — a product state Ψ = ⊗ₖ ψₖ has ‖Ψ‖² = ∏ₖ ‖ψₖ‖²; a product of unit modes is a unit state (norm_tprodState_unit) — the composite (tensor) structure.

This is the free field at a finite cutoff: a finite product Σ, with the record layer applying mode-by-mode. Relativistic dispersion, microcausality, and interactions are the later EFT stages. Foundational-triple, no sorry.

References

CV/OscillatorBorn.lean (the single mode as a record-layer measurement); CV/OscillatorSpectrum.lean (oscEnergy, oscEnergy_cutoff_independent); CV/Position.lean (the spatial-lattice seed); RecordLayer/Measurement.lean (the record layer).

@[reducible, inline]

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

A field-mode configuration: mode k carries c k quanta (K modes, each truncated to N levels).

Equations

• CSD.CV.FieldConfig K N = (Fin K → Fin N)

@[reducible, inline]

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

The truncated multi-mode field Hilbert space: the (truncated) tensor product of K single-mode spaces, indexed by occupation configurations.

Equations

• CSD.CV.FieldSpace K N = EuclideanSpace ℂ (CSD.CV.FieldConfig K N)

noncomputable def CSD.CV.fieldEnergy {K N : ℕ} (c : FieldConfig K N) : ℝ

The field energy of a configuration: the sum of the mode energies E_{c_k} = c_k + ½.

Equations

• CSD.CV.fieldEnergy c = ∑ k : Fin K, CSD.CV.oscEnergy ↑(c k)

noncomputable def CSD.CV.fieldHamiltonian (K N : ℕ) : Matrix (FieldConfig K N) (FieldConfig K N) ℂ

The free-field Hamiltonian: diagonal in the configuration basis with eigenvalue the field energy — the sum of the single-mode oscillator Hamiltonians.

Equations

• CSD.CV.fieldHamiltonian K N = Matrix.diagonal fun (c : CSD.CV.FieldConfig K N) => ↑(CSD.CV.fieldEnergy c)

theorem CSD.CV.fieldHamiltonian_mulVec_single {K N : ℕ} (c : FieldConfig K N) : (fieldHamiltonian K N).mulVec (Pi.single c 1) = ↑(fieldEnergy c) • Pi.single c 1

The configuration c is a field-energy eigenstate with eigenvalue ∑ₖ oscEnergy (c k).

theorem CSD.CV.fieldEnergy_cutoff_independent {K N M : ℕ} (c : FieldConfig K N) (d : FieldConfig K M) (h : ∀ (k : Fin K), ↑(c k) = ↑(d k)) : fieldEnergy c = fieldEnergy d

Cutoff-independence of the field energy. Configurations with the same per-mode occupation have the same field energy, regardless of the truncation. The multi-mode analogue of oscEnergy_cutoff_independent.

noncomputable def CSD.CV.fieldBornProb {K N : ℕ} (Ψ : FieldSpace K N) (c : FieldConfig K N) : ℝ

The Born probability of the full occupation configuration c in field state Ψ: ‖⟨c|Ψ⟩‖². The configuration basis is the standard basis, so this is the record-layer Born weight.

Equations

• CSD.CV.fieldBornProb Ψ c = ‖Ψ.ofLp c‖ ^ 2

theorem CSD.CV.fieldBornProb_eq {K N : ℕ} (Ψ : FieldSpace K N) (c : FieldConfig K N) : fieldBornProb Ψ c = ‖Ψ.ofLp c‖ ^ 2

theorem CSD.CV.sum_fieldBornProb_unit {K N : ℕ} (Ψ : FieldSpace K N) (hΨ : ‖Ψ‖ = 1) : ∑ c : FieldConfig K N, fieldBornProb Ψ c = 1

The configuration Born probabilities sum to 1 on a unit field state — a probability distribution over occupation configurations.

noncomputable def CSD.CV.tprodState {K N : ℕ} (ψ : Fin K → EuclideanSpace ℂ (Fin N)) : FieldSpace K N

A product (tensor) field state Ψ = ⊗ₖ ψₖ: the amplitude of configuration c is the product of the per-mode amplitudes ∏ₖ ψₖ (c k).

Equations

• CSD.CV.tprodState ψ = WithLp.toLp 2 fun (c : CSD.CV.FieldConfig K N) => ∏ k : Fin K, (ψ k).ofLp (c k)

theorem CSD.CV.tprodState_apply {K N : ℕ} (ψ : Fin K → EuclideanSpace ℂ (Fin N)) (c : FieldConfig K N) : (tprodState ψ).ofLp c = ∏ k : Fin K, (ψ k).ofLp (c k)

theorem CSD.CV.norm_sq_tprodState {K N : ℕ} (ψ : Fin K → EuclideanSpace ℂ (Fin N)) : ‖tprodState ψ‖ ^ 2 = ∏ k : Fin K, ‖ψ k‖ ^ 2

The composite (tensor) structure: norms multiply. A product state's squared norm is the product of the mode squared norms, ‖⊗ₖ ψₖ‖² = ∏ₖ ‖ψₖ‖².

theorem CSD.CV.norm_tprodState_unit {K N : ℕ} (ψ : Fin K → EuclideanSpace ℂ (Fin N)) (hψ : ∀ (k : Fin K), ‖ψ k‖ = 1) : ‖tprodState ψ‖ = 1

A product of unit modes is a unit field state.

noncomputable def CSD.CV.modeMarginal {K N : ℕ} (Ψ : FieldSpace K N) (k₀ : Fin K) (n : Fin N) : ℝ

The single-mode marginal Born probability: the probability that mode k₀ carries n quanta, summed over the occupations of all the other modes.

Equations

• CSD.CV.modeMarginal Ψ k₀ n = ∑ c : CSD.CV.FieldConfig K N with c k₀ = n, CSD.CV.fieldBornProb Ψ c

theorem CSD.CV.modeMarginal_tprod {K N : ℕ} (ψ : Fin K → EuclideanSpace ℂ (Fin N)) (k₀ : Fin K) (n : Fin N) : modeMarginal (tprodState ψ) k₀ n = ‖(ψ k₀).ofLp n‖ ^ 2 * ∏ k ∈ Finset.univ.erase k₀, ‖ψ k‖ ^ 2

Mode-wise Born (the marginal of a product state). For a product field state, the marginal Born probability that mode k₀ carries n quanta factorises as ‖ψ_{k₀} n‖² · ∏_{k≠k₀} ‖ψ k‖² — the single-mode Born weight of k₀, times the norms of the spectator modes. The modes are independent.

theorem CSD.CV.modeMarginal_tprod_unit {K N : ℕ} (ψ : Fin K → EuclideanSpace ℂ (Fin N)) (hψ : ∀ (k : Fin K), ‖ψ k‖ = 1) (k₀ : Fin K) (n : Fin N) : modeMarginal (tprodState ψ) k₀ n = ‖(ψ k₀).ofLp n‖ ^ 2

Mode-wise Born for unit modes. For a product of unit modes, the marginal Born probability that mode k₀ carries n quanta is exactly the single-mode Born weight ‖ψ_{k₀} n‖² — measuring one mode of the field reproduces the single-mode record-layer Born rule.