SigmaLayer/ApproxProjectability: A5's approximate (ε,T)-projectability

Category: 7-SigmaLayer (Paper C A5 — the axiom that selects the sector).

What A5 says, and what was missing

A5's physical content is the approximate case: a Hamiltonian is quantum-effective when it is almost fibre-invariant — H = h∘π + δH with sup‖d(δH)|_V‖ ≤ ε over a time window T — and it is this condition, not the exact one, that selects which Hamiltonians the sector supports. Until now only the exact case H = h∘π was formalised (kSectorDataFlow_projectable, SigmaLayer/DynamicsBridge.lean): the axiom that does the selecting had its actual content unformalised. This module supplies it, in two halves:

• the ontic predicate — EpsProjectable, in oscillation form: the ontic Hamiltonian varies by at most ε along each fibre. ⚠️ The derivative form sup‖d(δH)|_V‖ ≤ ε is the scoped manifold statement (reconstruction-status.md §2a — no exterior-calculus API); the oscillation form is its formalisable core, related in the usual way (a derivative bound integrates to an oscillation bound on a compact fibre). Stated so the substitution is visible, not silent.
• the dynamical content — the shadowing theorem: a Hamiltonian ε-close in L2 operator norm to a sector-projectable one generates Schrödinger dynamics that the sector dynamics tracks to within ε·T over the window [−T, T] (quantum_effective_shadowing, from the Duhamel bound). That is the operational meaning of "quantum-effective": for times up to T, the sector cannot tell H from its projectable part.

What is proved

• EpsProjectable — the predicate on ontic Hamiltonians Σ → ℝ; epsProjectable_mono.
• epsProjectable_zero_iff — the exact case is the ε = 0 instance: zero fibre-oscillation is precisely factoring through π. This is the BACKLOG row's required tie-in, and it is an iff.
• diagOnticEnergy_epsProjectable — non-vacuity: the moment-map energy of a diagonal observable (∑ₖ λₖ · momentMap) is an EpsProjectable _ 0 witness — the corpus's own Born-weight energies are exactly projectable.
• quantum_effective_shadowing — ‖H − H₀‖ ≤ ε and |t| ≤ T give ‖e^{t(−iH)} − e^{t(−iH₀)}‖ ≤ ε·T.
• quantum_effective_shadowing_state — the same at the level of states: evolved vectors stay within ε·T·‖ψ‖.

⚠️ Scope

• The derivative-form predicate is not formalised (manifold API; §2a) — the oscillation form stands in, and the docstrings say so wherever it appears.
• The shadowing theorems live on the Hilbert side (matrix generators), where the corpus's dynamics genuinely runs; the ontic predicate lives on Σ. The bridge between them — an ontic Hamiltonian generating a flow whose projection is e^{−itH} — is A2's open row, not A5's, and is not claimed here.
• H₀'s witness flow being projectable is the existing exact-case result (productDynamicsBridge); this module adds the approximate layer on top of it, not a new dynamics.

References

Mathlib/Analysis/Matrix/DuhamelBound.lean (the quantitative engine); SigmaLayer/DynamicsBridge.lean (the exact case this extends); LF4/MomentMap.lean (momentMap — the non-vacuity witness); specs/BACKLOG.md (the ★ A5 row); specs/reconstruction-status.md §2a.

The ontic predicate, in oscillation form

def CSD.RecordLayer.EpsProjectable {N : ℕ} (Hs : LF4.KSigma N → ℝ) (ε : ℝ) : Prop

(ε)-projectability of an ontic Hamiltonian (oscillation form): Hs varies by at most ε along each fibre of π = Prod.fst. The fibre directions are Paper C's vertical subspace V; the scoped derivative form sup‖d(δH)|_V‖ ≤ ε refines this on a smooth structure the corpus does not carry (reconstruction-status.md §2a).

Equations

• CSD.RecordLayer.EpsProjectable Hs ε = ∀ (p : CSD.LF4.CPN N) (θ θ' : CSD.LF4.KTorus), |Hs (p, θ) - Hs (p, θ')| ≤ ε

theorem CSD.RecordLayer.epsProjectable_mono {N : ℕ} {Hs : LF4.KSigma N → ℝ} {ε ε' : ℝ} (h : ε ≤ ε') (hHs : EpsProjectable Hs ε) : EpsProjectable Hs ε'

theorem CSD.RecordLayer.epsProjectable_zero_iff {N : ℕ} (Hs : LF4.KSigma N → ℝ) : EpsProjectable Hs 0 ↔ ∃ (h : LF4.CPN N → ℝ), Hs = fun (x : LF4.KSigma N) => h x.1

The exact case is the ε = 0 instance — as an iff. Zero fibre-oscillation is precisely factoring through the projection: Hs = h ∘ π. This ties the new predicate to the corpus's existing exact-case formalisation (kSectorDataFlow_projectable).

noncomputable def CSD.RecordLayer.diagOnticEnergy {N : ℕ} (lam : Fin N → ℝ) : LF4.KSigma N → ℝ

Non-vacuity: the corpus's own energies are exactly projectable. The moment-map energy of a diagonal observable with eigenvalues λ — the ontic form of ⟨ψ, diag(λ) ψ⟩ (observable_correspondence_diagonal) — depends on the base point alone, so it is EpsProjectable _ 0.

Equations

• CSD.RecordLayer.diagOnticEnergy lam x = ∑ k : Fin N, lam k * CSD.LF4.momentMap x.1 k

theorem CSD.RecordLayer.diagOnticEnergy_epsProjectable {N : ℕ} (lam : Fin N → ℝ) : EpsProjectable (diagOnticEnergy lam) 0

The dynamical content: shadowing over the window

theorem CSD.RecordLayer.quantum_effective_shadowing {N : ℕ} [NeZero N] {H H₀ : Matrix (Fin N) (Fin N) ℂ} (hH : H.IsHermitian) (hH₀ : H₀.IsHermitian) {ε T t : ℝ} (hclose : ‖H - H₀‖ ≤ ε) (ht : |t| ≤ T) : ‖NormedSpace.exp (t • -Complex.I • H) - NormedSpace.exp (t • -Complex.I • H₀)‖ ≤ ε * T

★ The shadowing theorem (A5's dynamical content). If H is ε-close in L2 operator norm to a Hamiltonian H₀ — the projectable part — then over the whole window [−T, T] the two Schrödinger unitaries differ by at most ε·T.

Reading: H₀'s witness flow is projectable (the exact case, productDynamicsBridge), so the sector dynamics tracks the true dynamics of H to within ε·T — for times up to T, the sector cannot tell a quantum-effective Hamiltonian from its projectable part. That is what "selects the sector" means operationally, and it is the content the exact case alone could not express.

theorem CSD.RecordLayer.quantum_effective_shadowing_state {N : ℕ} [NeZero N] {H H₀ : Matrix (Fin N) (Fin N) ℂ} (hH : H.IsHermitian) (hH₀ : H₀.IsHermitian) {ε T t : ℝ} (hclose : ‖H - H₀‖ ≤ ε) (ht : |t| ≤ T) (ψ : EuclideanSpace ℂ (Fin N)) : ‖(Matrix.toEuclideanLin (NormedSpace.exp (t • -Complex.I • H))) ψ - (Matrix.toEuclideanLin (NormedSpace.exp (t • -Complex.I • H₀))) ψ‖ ≤ ε * T * ‖ψ‖

The shadowing theorem at the level of states: for any initial vector ψ, the two evolved states stay within ε·T·‖ψ‖ for the whole window.