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

Category: 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);
• 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); SigmaLayer/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.