BarrierCollapse.lean`

3 declarations, 0 contain sorry, 0 declared as axioms

Collapse forced by barriers of vanishing energy

The line-payment inequality prevents barriers of vanishing energy from crossing every horizontal line over a fixed interval of positive length. Applied to both coordinate projections, this forces a compact connected planar set to be a singleton. The hypotheses specify barrier existence, crossings, and absolute continuity of the restrictions.

def OAI.CircleDomainRigidity.HasVanishingRectangleBarriers line 25
Source documentation
A sequence of actual rectangle barriers, each crossing almost every horizontal line over (a,b], whose squared horizontal derivative energies tend to zero. The supporting horizontal interval is fixed for the sequence.
```
def HasVanishingRectangleBarriers (a b : ℝ) : Prop :=
…
```
theorem OAI.CircleDomainRigidity.eq_of_vanishing_rectangle_barriers line 38
Source documentation
A nondegenerate interval cannot support crossings by barriers whose energies tend to zero. This is the contradiction step after line payment.
```
theorem eq_of_vanishing_rectangle_barriers {a b : ℝ} (hab : a ≤ b)
    (hbar : HasVanishingRectangleBarriers a b) : a = b := by
…
```
Mentions: OAI.CircleDomainRigidity.HasVanishingRectangleBarriers
theorem OAI.CircleDomainRigidity.subsingleton_of_vanishing_projection_barriers line 52
Source documentation
If both coordinate projection intervals of a compact connected planar set admit the barriers above, then every two points of the set coincide. Compactness and connectedness identify the projections with the full closed intervals between their extrema.
```
theorem subsingleton_of_vanishing_projection_barriers {K : Set ℂ}
    (hcompact : IsCompact K) (hconnected : IsConnected K)
    (hre : HasVanishingRectangleBarriers
      (sInf (Complex.re '' K)) (sSup (Complex.re '' K)))
    (him : HasVanishingRectangleBarriers
      (sInf (Complex.im '' K)) (sSup (Complex.im '' K))) :
    K.Subsingleton := by
…
```
Mentions: OAI.CircleDomainRigidity.HasVanishingRectangleBarriers