CV/OscillatorBorn: the truncated mode as a record-layer measurement (EFT Stage 0)

Category: CV (continuous variables — the single bosonic mode).

Turns the truncated single mode of CV/OscillatorSpectrum.lean from an operator algebra into a genuine CSD reconstruction, by wiring its number/energy measurement into the record layer (SigmaLayer/Measurement.lean) and establishing cutoff-independence of the Born content — Stage 0 of the EFT direction (specs/record-layer-plan.md; the ladder QM → CV → relativistic EFT).

The oscillator Hamiltonian is diagonal (hamiltonian_eq_diagonal), so the number/energy eigenbasis is the standard basis of EuclideanSpace ℂ (Fin N); a number/energy measurement is therefore exactly the standard-basis record-layer measurement. Hence:

• numberBornProb / numberBornProb_eq — the Born probability of finding n quanta (energy oscEnergy n = n + ½) is ‖⟨n|ψ⟩‖², the record-layer bornRate;
• numberMeasurement / numberMeasurement_prob — the mode's measurement is a record-layer Measurement (context + unknown microstate → record), with outcome probability ‖⟨n|ψ⟩‖²;
• numberMeasurement_frequency — the oscillator's Born rule is the law of large numbers over the unknown microstate (inherited from the record layer);
• numberState_energy_eigenstate — the Fock state n is the energy eigenstate E = oscEnergy n, so number = energy measurement;
• numberBornProb_embed — cutoff-independence: raising the truncation N → M ≥ N (zero-padding the new high levels) leaves each finite level's Born probability unchanged; the mode's finite-level Born predictions do not depend on the cutoff (the Born analogue of oscEnergy_cutoff_independent).

Honest scope: this is the single mode at a finite cutoff. The strict continuum limit (rigged Hilbert space / Bargmann–Fock) is deliberately not taken — the EFT posture is cutoff-independence, not the continuum (ApproxCCR.no_exact_finite_ccr + ccr_exact_on_bulk). Multi-mode fields, relativistic dispersion, locality, and interactions are the later EFT stages. Foundational-triple, no sorry.

References

CV/OscillatorSpectrum.lean (hamiltonian, oscEnergy, hamiltonian_mulVec_single, oscEnergy_cutoff_independent); CV/ApproxCCR.lean (the finite-CCR obstruction / bulk-exactness); SigmaLayer/Measurement.lean (the record layer, bornMeasurement, bornMeasurement_frequency); SigmaLayer/BasisMeasurement.lean (arbitrary observable, if a non-number basis is measured).

noncomputable def CSD.CV.numberBornProb {N : ℕ} (ψ : EuclideanSpace ℂ (Fin N)) (n : Fin N) : ℝ

The Born probability of finding n quanta (energy oscEnergy n = n + ½) in mode state ψ: the squared amplitude ‖⟨n|ψ⟩‖², i.e. the record-layer bornRate. The number eigenbasis is the standard basis (hamiltonian is diagonal), so this is the standard-basis Born weight.

Equations

• CSD.CV.numberBornProb ψ n = CSD.RecordLayer.bornRate ψ n

theorem CSD.CV.numberBornProb_eq {N : ℕ} (ψ : EuclideanSpace ℂ (Fin N)) (n : Fin N) : numberBornProb ψ n = ‖ψ.ofLp n‖ ^ 2

theorem CSD.CV.sum_numberBornProb_unit {N : ℕ} (ψ : EuclideanSpace ℂ (Fin N)) (hψ : ‖ψ‖ = 1) : ∑ n : Fin N, numberBornProb ψ n = 1

The number-level Born probabilities sum to 1 on a unit state.

theorem CSD.CV.numberState_energy_eigenstate {N : ℕ} (n : Fin N) : (hamiltonian N).mulVec (Pi.single n 1) = ↑(oscEnergy ↑n) • Pi.single n 1

The Fock state n is the energy eigenstate with eigenvalue oscEnergy n = n + ½. So measuring the number is measuring the energy; the Born probability of energy oscEnergy n is numberBornProb ψ n.

noncomputable def CSD.CV.numberMeasurement {N : ℕ} (ψ : EuclideanSpace ℂ (Fin N)) (t : SigmaLayer.OnticTime) : RecordLayer.Measurement N

The mode's number/energy measurement, as a record-layer measurement. The number basis is the standard basis, so the measurement is Measurement.bornMeasurement: the unknown microstate selects the recorded quantum number, the combined result is the record-layer P5 record.

Equations

• CSD.CV.numberMeasurement ψ t = CSD.RecordLayer.Measurement.bornMeasurement ψ t

theorem CSD.CV.numberMeasurement_prob {N : ℕ} (ψ : EuclideanSpace ℂ (Fin N)) (hψ : ‖ψ‖ = 1) (n : Fin N) (t : SigmaLayer.OnticTime) : (numberMeasurement ψ t).prob n = ENNReal.ofReal (numberBornProb ψ n)

The record-layer probability of recording n quanta is the oscillator Born probability.

theorem CSD.CV.numberMeasurement_frequency {N : ℕ} (ψ : EuclideanSpace ℂ (Fin N)) (hψ : ‖ψ‖ = 1) (n : Fin N) (t : SigmaLayer.OnticTime) {Ω : Type u_1} [MeasurableSpace Ω] {P : MeasureTheory.Measure Ω} [MeasureTheory.IsProbabilityMeasure P] (X : ℕ → Ω → ℝ) (hX : ∀ (k : ℕ), Measurable (X k)) (hlaw : ∀ (k : ℕ), MeasureTheory.Measure.map (X k) P = RecordLayer.fibreTypicality) (hindep : Pairwise (Function.onFun (fun (f g : Ω → ℝ) => ProbabilityTheory.IndepFun f g P) fun (k : ℕ) => (X k ⁻¹' (numberMeasurement ψ t).basin n).indicator fun (x : Ω) => 1)) : ∀ᵐ (ω : Ω) ∂P, Filter.Tendsto (fun (m : ℕ) => (∑ k ∈ Finset.range m, (X k ⁻¹' (numberMeasurement ψ t).basin n).indicator (fun (x : Ω) => 1) ω) / ↑m) Filter.atTop (nhds (numberBornProb ψ n))

The oscillator's Born rule is the law of large numbers over the unknown microstate. For i.i.d. typical microstates, the frequency of trials recording n quanta converges a.s. to the Born probability numberBornProb ψ n = ‖⟨n|ψ⟩‖². Inherited verbatim from the record layer.

noncomputable def CSD.CV.embedMode {N M : ℕ} (_h : N ≤ M) (ψ : EuclideanSpace ℂ (Fin N)) : EuclideanSpace ℂ (Fin M)

Zero-padding embedding of a cutoff-N mode state into a larger cutoff M ≥ N: keep the low levels, set the new high levels to 0.

Equations

• CSD.CV.embedMode _h ψ = WithLp.toLp 2 fun (j : Fin M) => if hj : ↑j < N then ψ.ofLp ⟨↑j, hj⟩ else 0

theorem CSD.CV.embedMode_castLE {N M : ℕ} (h : N ≤ M) (ψ : EuclideanSpace ℂ (Fin N)) (i : Fin N) : (embedMode h ψ).ofLp (Fin.castLE h i) = ψ.ofLp i

The embedded state agrees with ψ on the low levels.

theorem CSD.CV.numberBornProb_embed {N M : ℕ} (h : N ≤ M) (ψ : EuclideanSpace ℂ (Fin N)) (i : Fin N) : numberBornProb (embedMode h ψ) (Fin.castLE h i) = numberBornProb ψ i

Cutoff-independence of the Born content. Raising the truncation from N to any M ≥ N (zero-padding the new high levels) leaves each finite level's Born probability unchanged: the mode's finite-level Born predictions do not depend on the cutoff. The Born analogue of oscEnergy_cutoff_independent.