PacketDataSignedAngularGeometry.lean`

2 declarations, 0 contain sorry, 0 declared as axioms

Angular margins discharge the direction hypotheses of signed selected-box separation, for both passes of the stopping procedure.

theorem OAI.LipschitzHilbert.PacketLatticeData.SizeStoppingRun.selected_top_direction_bound_signed line 18

theorem OAI.LipschitzHilbert.PacketLatticeData.SizeStoppingRun.selected_boxes_disjoint_of_margin_signed line 36

Source documentation

The geometric separation now needs only the packet-cell margins and the two packet slope bounds; it does not assume the later top's direction.

theorem selected_boxes_disjoint_of_margin_signed
    (h : P.SizeStoppingRun negative w cb tau sigma epsilon A cell grid c initial tops remaining)
    (hw : 0<w) (hwW : w≤P.width) (hcb : 0<cb)
    (t K CZero : ℝ) (hK : 0≤K) (hCZero : 0<CZero)
    (hconstants : (1+cb/4)/CZero≤cb/4)
    (hA : 2*K*(1+(1+cb/4))+1/2≤A)
    (p p' : SlopeBox × Finset P.PacketIndex)
    (hp : p∈P.sizeSelectionRecords negative w cb A cell grid initial tops)
    (hp' : p'∈P.sizeSelectionRecords negative w cb A cell grid initial tops)
    (q q' : P.PacketIndex) (hq : q∈p.2) (hq' : q'∈p'.2)
    (hlen : P.length q.1≤P.length q'.1)
    (hfar : CZero*P.length q.1≤P.length q'.1)
…

Mentions: OAI.LipschitzHilbert.SlopeBox