Documentation

Lean 4 Proof

theorem simon_near_decomposable_gap
    (ε _withinBlock : ℝ) (hε : 0 < ε) (hε1 : ε < 1)
    (_hw : 0 < _withinBlock) :
    -- The spectral gap is bounded below by the decomposability quality
    1 / ε - 1 > 0 ∧
    -- Schematic: actual spectral gap ≥ (1/ε - 1) for ε-near-decomposable matrix
    True := by
  constructor
  · rw [gt_iff_lt, sub_pos, lt_div_iff₀ hε]
    linarith
  · trivial

Dependency Graph

Location

thesis/CESProofs/Hierarchy/SpectralHierarchy.lean:203

Module Section

Endogenous Hierarchy: Why N Levels?

In the same file