N9.2: Define canonical localized frequency envelopes and prove H_FE via bootstrap

[Copilot]

Issue N9.2 required a precise definition of c_{j,x₀,k}(t) (localized frequency envelopes) and a proof or reduction of the near-diagonal summability hypothesis H_FE: 2^k · ∫ Σ_{j=k}^{k+J} 2^{j/2} c_j² dt ≤ A.

New: lean/FreqEnvelopes.lean

Lean 4 formalization in namespace TOGT.FreqEnvelopes covering:

• Canonical definition — FreqEnvelopeFamily abstracts c_{j,x₀,k}(t)² = ∫ |P_j f(x,t)|² φ_{x₀,k}(x) dx (Littlewood–Paley projector weighted by smooth spatial bump at scale 2^{-k}). Docstring states the concrete LP definition; the structure axiomatises only what H_FE needs.

• H_FE statement — def H_FE (F : FreqEnvelopeFamily) (J : ℕ) (A : ℝ) : Prop asserts the uniform bound over all k.

• Bootstrap reduction — Hyp_Bootstrap requires ∫ c_j² dt ≤ C · 2^{-αj} with α > 3/2. H_FE_of_bootstrap derives H_FE with explicit constant A = C(J+1). One sorry marks the finite geometric sum comparison inside nearDiag_sum_bound; the surrounding logic is complete.

• Worked example — geometricEnvelope (c_j(t) = baseʲ · φ(t), base < 2^{-3/2}) satisfies Hyp_Bootstrap with α = -2 log₂(base) > 3, confirming the definition is non-vacuous.

-- Core reduction: bootstrap decay ⟹ H_FE
theorem H_FE_of_bootstrap
    (F : FreqEnvelopeFamily) (J : ℕ) (C α : ℝ)
    (hB : Hyp_Bootstrap F C α) :        -- ∀ j, ∫ c_j² ≤ C · 2^{-αj}, α > 3/2
    H_FE F J (C * (J + 1)) := ...       -- explicit bound A = C(J+1)

New: docs/analysis_ns/n9_v0.1_freq_envelopes.md

Mathematical exposition: LP projector setup, precise definition of c_{j,x₀,k}, H_FE statement, full bootstrap proof sketch, and the geometric-decay example with explicit constants.

Minor updates

• docs/analysis_ns/README.md — index entry for the new note.
• lean/Main.lean — cross-reference comment to FreqEnvelopes.lean.