Chapter F2

import Definitions.Def_ChapterF1
import Mathlib


/-!
# Chapter F2 — the mass gap in the Bargmann–Fock model (roadmap N7(c), §0 S7)

This file formalizes the mathematically self-contained content of the book's
**"Mass gap"** section (`book.tex` ~line 4060), continuing the polynomial
(Bargmann–Fock) field model of `BookProof.ChapterF1` and following the `../unfer`
design decisions (§0 S7: quadratic ordering, Hermitian field representation,
`nested_fock_algebra` crate).

Following the book's own definition — *"the mass gap is the eigenvalue of the
Hamiltonian which is closer to the null eigenvalue corresponding to the vacuum
state"* — the Hamiltonian is the quadratically-ordered
`H := a† a = N` (`ChapterF1.hamiltonian`, the number operator).  On the monomial
basis `H Xⁿ = n·Xⁿ` (`ChapterF1.numberOp_monomial`), so the spectrum is `ℕ`, the
vacuum `|0⟩ = 1` has energy `0`, and the mass gap is `Δ = 1`.

## Deliverables

* **F2.1 `numberOp_coeff`** — the coefficient formula `(N p)_n = n · p_n`, and
  `numberOp_support` (`N` does not enlarge the support).
* **F2.2 `hamiltonian_expectation_nonneg`** — the Hamiltonian is *bounded from
  below / positive*: `⟨ψ|H|ψ⟩ ≥ 0` for every state (the quadratic ordering makes
  the vacuum energy the infimum; book: *"the Hamiltonian can be bounded from
  below because it is defined a priori with a correct (Quadratic) ordering"*).
* **F2.3 mass-gap deformation** — `deformedHamiltonian c := c • N`
  (`= H + (c−1)·N`), `deformedHamiltonian_monomial` (`H_c Xⁿ = (c·n)·Xⁿ`, so the
  mass gap becomes `c`, an arbitrary positive number, with unchanged
  eigenstates) and `deformedHamiltonian_commutes_numberOp` (`[H_c, N] = 0`) —
  the book's claim that *"the number operator can be added to the Hamiltonian,
  modifying the mass gap without observable consequences"* (`[H, N] = 0`).
* **F2.4 HEADLINE `mass_gap`** — for any state `ψ` orthogonal to the vacuum
  (`ψ₀ = 0`), `⟨ψ|H|ψ⟩ ≥ ⟨ψ|ψ⟩`: the spectrum of `H` above the vacuum is bounded
  below by the mass gap `Δ = 1`.  The gap is *tight*: `mass_gap_attained`
  (`⟨X|H|X⟩ = ⟨X|X⟩`, the first excited state saturates it), and the vacuum
  energy is `0` (`vacuum_energy_zero`).  `massGap_smallest_excited` records the
  eigenvalue-form statement (`1` is the smallest positive eigenvalue).

Everything is `sorry`-free and `axiom`-free (only `propext`, `Classical.choice`,
`Quot.sound`); **no `EXTERNAL` hypothesis**.
-/

open Polynomial Finset
open scoped BigOperators

namespace BookProof.ChapterF2

open BookProof.ChapterF1

noncomputable section

/-! ## F2.1 — Coefficients of the number operator -/





/-! ## F2.2 — Real form of the energy expectation and positivity -/







/-! ## F2.3 — Deforming the mass gap by adding the number operator -/

/-- The **deformed Hamiltonian** `H_c := c • N` (equivalently `H + (c−1)·N`,
adding a multiple of the number operator to `H = N`).  Because `[H, N] = 0`, this
modifies the mass gap without changing the observable algebra (generated by `N`)
or the eigenstates — the book's *"the number operator can be added to the
Hamiltonian, modifying the mass gap without observable consequences"*. -/
noncomputable def deformedHamiltonian (c : ℂ) : ℂ[X] →ₗ[ℂ] ℂ[X] := c • numberOp







/-! ## F2.4 — The mass gap (HEADLINE) -/









end

end BookProof.ChapterF2