import KTV.Johnson.MainTheorems

namespace KTV.Johnson

universe uMain

/--
Closed spectral-gap statement corresponding to the final lazy swap-chain result
of *Spectral Gap for the Binary Fixed-Margin Swap Chain*: on every finite
binary fixed-margin model, the lazy ordered
rectangle-swap operator has gap at least
`1 / choose |Col| 2 * 1 / choose |Row| 2`.
-/
theorem binaryFixedMarginLazySwapChain_spectralGap_card
    {Row Col : Type uMain} [Fintype Row] [DecidableEq Row]
    [Fintype Col] [DecidableEq Col]
    [Nonempty (OrderedDistinctPair Row)]
    [Nonempty (OrderedDistinctPair Col)]
    (M : FixedMarginModel Row Col) [Nonempty (FixedMarginState M)] :
    OperatorSpectralGapAtLeast
      (Ω := FixedMarginState M)
      (fixedMarginOrderedDistinctRectangleLazySwapOperator M)
      (((1 : Rat) / ((Fintype.card Col).choose 2 : Rat)) *
        ((1 : Rat) / ((Fintype.card Row).choose 2 : Rat))) :=
  fixedMarginOrderedDistinctRectangleLazySwapOperator_gap_card M

end KTV.Johnson