SurvivingSeeds.lean`

46 declarations, 0 contain sorry, 0 declared as axioms

abbrev OAI.PlanarL1.Columns.Model.BandTrees.RadialIndex line 15
Source documentation
The very same finite connected radial cells, at an arbitrary prescribed width; the secondary construction uses width g, not the main width D.
```
abbrev RadialIndex (width phase : ℝ) :=
…
```
instance OAI.PlanarL1.Columns.Model.BandTrees.(instance at line 19) line 19
lemma OAI.PlanarL1.Columns.Model.BandTrees.radial_cover line 23
lemma OAI.PlanarL1.Columns.Model.BandTrees.radial_unique line 46
lemma OAI.PlanarL1.Columns.Model.BandTrees.radial_diameter line 58
lemma OAI.PlanarL1.Columns.Model.BandTrees.radial_separated line 65
structure OAI.PlanarL1.Columns.Model.SurvivingGroups.Position line 98
Source documentation
Geometric part of a retained endpoint, before witness selection. Both old identifiers refer to the actual closed unrestricted radius-five ball.
```
structure Position where
…
```
lemma OAI.PlanarL1.Columns.Model.SurvivingGroups.Position.band_near line 116
lemma OAI.PlanarL1.Columns.Model.SurvivingGroups.Position.subA line 122
lemma OAI.PlanarL1.Columns.Model.SurvivingGroups.Position.subB line 124
lemma OAI.PlanarL1.Columns.Model.SurvivingGroups.Position.contains line 126
structure OAI.PlanarL1.Columns.Model.SurvivingGroups.Seed line 133
Source documentation
Literal geometric data retained after both descent tests and the low-tip exclusion. These records are finite witnesses of those tests, not estimates or success/persistence assumptions.
```
structure Seed extends Position A SA SB lo C lo₂ phase where
…
```
Mentions: OAI.PlanarL1.Columns.Model.SurvivingGroups.Position
lemma OAI.PlanarL1.Columns.Model.SurvivingGroups.Seed.source line 148
abbrev OAI.PlanarL1.Columns.Model.SurvivingGroups.Key line 155
def OAI.PlanarL1.Columns.Model.SurvivingGroups.key line 156
def OAI.PlanarL1.Columns.Model.SurvivingGroups.keys line 158
abbrev OAI.PlanarL1.Columns.Model.SurvivingGroups.GroupIndex line 159
instance OAI.PlanarL1.Columns.Model.SurvivingGroups.(instance at line 160) line 160
def OAI.PlanarL1.Columns.Model.SurvivingGroups.members line 161
lemma OAI.PlanarL1.Columns.Model.SurvivingGroups.members_nonempty line 162
def OAI.PlanarL1.Columns.Model.SurvivingGroups.seeds line 165
lemma OAI.PlanarL1.Columns.Model.SurvivingGroups.seed_mem line 166
lemma OAI.PlanarL1.Columns.Model.SurvivingGroups.seeds_nonempty line 169
def OAI.PlanarL1.Columns.Model.SurvivingGroups.group line 174
Source documentation
Group formation: exactly one finite proposal family per g-cell and pair of old identifiers. The update groups themselves add no chart boundary.
```
noncomputable def group (q : GroupIndex s) : SecondaryGeometry.Group A SB where
…
```
Mentions: OAI.PlanarL1.Columns.Model.SurvivingGroups.GroupIndex, OAI.PlanarL1.Columns.Model.SecondaryGeometry.Group
def OAI.PlanarL1.Columns.Model.SurvivingGroups.Seed.partnerAt line 223
def OAI.PlanarL1.Columns.Model.SurvivingGroups.Seed.descentAt line 225
def OAI.PlanarL1.Columns.Model.SurvivingGroups.Seed.partnerDescentAt line 229
lemma OAI.PlanarL1.Columns.Model.SurvivingGroups.Seed.apartAt line 232
lemma OAI.PlanarL1.Columns.Model.SurvivingGroups.Seed.closeAt line 235
lemma OAI.PlanarL1.Columns.Model.SurvivingGroups.Seed.retainedAt line 239

lemma OAI.PlanarL1.Columns.Model.SurvivingGroups.center_names line 253

Source documentation

Coincidence of BOTH old names at the center is derived from literal eligibility. No bound on the pre-existing number of chart identifiers is used.

lemma center_names (c : M.Point (BandTrees.band broad lo) (BandTrees.root M broad lo C))
    (cp : ∀ w, M.Path (BandTrees.band narrow lo₂) c.column (s w).point.column)
    (hp : ∀ w, (cp w).length c.height (s w).point.height≤4*R) (w : W) :
    SA.name c.column c.height=(s w).indexA ∧ SB.name c.column c.height=(s w).indexB := by
…

Mentions: OAI.PlanarL1.Columns.Model.BandTrees.band, OAI.PlanarL1.Columns.Model.BandTrees.root

theorem OAI.PlanarL1.Columns.Model.SurvivingGroups.packing line 271
Source documentation
The concrete restricted packing estimate for retained endpoints: choose one seed per actual group meeting the narrow ball, rather than assume a bounded overlap of proposal domains.
```
theorem packing (c : M.Point (BandTrees.band broad lo) (BandTrees.root M broad lo C))
    (hc : c.height ∈ BandTrees.band narrow lo₂)
    (cp : ∀ w, M.Path (BandTrees.band narrow lo₂) c.column (s w).point.column)
    (hp : ∀ w, (cp w).length c.height (s w).point.height≤4*R)
    (hkey : Function.Injective (key s)) : (Fintype.card W : ℝ)≤2+1600*R/g := by
…
```
Mentions: OAI.PlanarL1.Columns.Model.BandTrees.band, OAI.PlanarL1.Columns.Model.BandTrees.root, OAI.PlanarL1.Columns.Model.SurvivingGroups.key
def OAI.PlanarL1.Columns.Model.SurvivingGroups.Touch line 343
Source documentation
A real group meets the narrow-band radius-four-R ball through one of its actual retained endpoints. This test involves no fresh random choices.
```
def Touch (c : M.Point (BandTrees.band broad lo) (BandTrees.root M broad lo C))
    (q : GroupIndex s) : Prop := ∃ w, key s w=q.val ∧
…
```
Mentions: OAI.PlanarL1.Columns.Model.BandTrees.band, OAI.PlanarL1.Columns.Model.BandTrees.root, OAI.PlanarL1.Columns.Model.SurvivingGroups.GroupIndex, OAI.PlanarL1.Columns.Model.SurvivingGroups.key
abbrev OAI.PlanarL1.Columns.Model.SurvivingGroups.Hits line 347
instance OAI.PlanarL1.Columns.Model.SurvivingGroups.(instance at line 349) line 349
def OAI.PlanarL1.Columns.Model.SurvivingGroups.packBound line 354
Source documentation
One fixed universal integer, never depending on the finite list, the old identifiers, or the old chart count.
```
noncomputable def packBound : ℕ := 2+Nat.ceil (1600*R/g)
```
lemma OAI.PlanarL1.Columns.Model.SurvivingGroups.packBound_real line 356
lemma OAI.PlanarL1.Columns.Model.SurvivingGroups.touching_card line 361
lemma OAI.PlanarL1.Columns.Model.SurvivingGroups.touching_finset_card line 379
lemma OAI.PlanarL1.Columns.Model.SecondaryGeometry.Group.not_admitted_witness line 401
lemma OAI.PlanarL1.Columns.Model.SecondaryGeometry.Group.nonadmission_drop line 412
lemma OAI.PlanarL1.Columns.Model.SecondaryGeometry.Group.narrow_sub_ordered line 421
lemma OAI.PlanarL1.Columns.Model.SecondaryGeometry.Group.old_ordered line 426
def OAI.PlanarL1.Columns.Model.SecondaryGeometry.Group.excursions_of_rejected line 446
Source documentation
Literal rejection of both sphere tests provides actual narrow-band paths with opposite excursions of the fixed ordered part. No excursion hypothesis is substituted for the geometric admission test.
```
noncomputable def excursions_of_rejected {D : OrderedData M} (he : G.data=.ordered D)
    (C : G.Component) (w : M.Point (BandTrees.band narrow G.lower) (G.root C))
    (hw : w ∈ G.allSeeds C) (hpos : ¬G.Admitted true C w) (hneg : ¬G.Admitted false C w)
    {root : Fin (k+1)} (x : M.Point D.band root)
    (hc : x.column=w.column) (hH : x.height=w.height) :
    D.base.Excursions (G.narrow_sub_ordered he) x (2*R) (2*R/5) := by
…
```
Mentions: OAI.PlanarL1.Columns.Model.OrderedData, OAI.PlanarL1.Columns.Model.BandTrees.band, OAI.PlanarL1.Columns.Model.SecondaryGeometry.Group.root

lemma OAI.PlanarL1.Columns.Model.OrderedData.base_close_of_value line 511

Source documentation

The literal old-field cutoff controls the fixed ordered part; the auxiliary field is already 100-Lipschitz by its recorded history.

lemma base_close_of_value (D : OrderedData M) {root : Fin (k+1)}
    (x y : M.Point D.band root) (hnear : dist x y≤2)
    (hcut : |D.value SecondaryGeometry.Group.lam x.column ⟨x.height,x.inBand⟩-
      D.value SecondaryGeometry.Group.lam y.column ⟨y.height,y.inBand⟩|≤R/10000) :
    |D.base.eval x-D.base.eval y|≤R/1000 := by
…

Mentions: OAI.PlanarL1.Columns.Model.OrderedData, OAI.PlanarL1.Columns.Model.SecondaryGeometry.Group.lam

theorem OAI.PlanarL1.Columns.Model.SecondaryGeometry.Group.two_side_of_rejected line 541

Source documentation

No admitted endpoint gives the genuine transverse separation. All sphere witnesses and paths are obtained from the admission failures, not assumed.

theorem two_side_of_rejected {D : OrderedData M}
    (he : G.data=.ordered D) (hf : H.data=.ordered D) (hl : H.lower=G.lower)
    (C : G.Component) (E : H.Component)
    (w : M.Point (BandTrees.band narrow G.lower) (G.root C))
    (v : M.Point (BandTrees.band narrow H.lower) (H.root E))
    (hw : w ∈ G.allSeeds C) (hv : v ∈ H.allSeeds E)
    (hwp : ¬G.Admitted true C w) (hwn : ¬G.Admitted false C w)
    (hvp : ¬H.Admitted true E v) (hvn : ¬H.Admitted false E v)
    {root : Fin (k+1)} (x y : M.Point D.band root)
    (hxc : x.column=w.column) (hxh : x.height=w.height)
    (hyc : y.column=v.column) (hyh : y.height=v.height)
    (hlo : 1≤dist x y) (hhi : dist x y≤2)
…

Mentions: OAI.PlanarL1.Columns.Model.OrderedData, OAI.PlanarL1.Columns.Model.BandTrees.band, OAI.PlanarL1.Columns.Model.SecondaryGeometry.Group.root