PairSelection.lean`

82 declarations, 0 contain sorry, 0 declared as axioms

def OAI.PlanarL1.Columns.Model.BandTrees.radialValue line 13
def OAI.PlanarL1.Columns.Model.BandTrees.RadialInterior line 18
Source documentation
All column representatives, not only the chosen one, pass the radial interior test. The quantification is over zero-distance geometric points.
```
def RadialInterior (width phase : ℝ) (x : M.Point (band broad lo) (root M broad lo C)) : Prop :=
…
```
Mentions: OAI.PlanarL1.Columns.Model.BandTrees.band, OAI.PlanarL1.Columns.Model.BandTrees.root
lemma OAI.PlanarL1.Columns.Model.BandTrees.radial_difference line 22
lemma OAI.PlanarL1.Columns.Model.BandTrees.radialInterior_of_avoid line 27
lemma OAI.PlanarL1.Columns.Model.BandTrees.RadialInterior.ambient line 38
Source documentation
Intrinsic zero-distance representatives are exactly enough: any other unrestricted representative localizes into the same broad component.
```
lemma RadialInterior.ambient (A : Ambient M) {width phase : ℝ}
    {x : M.Point (band broad lo) (root M broad lo C)} (h : RadialInterior width phase x)
    (y : M.Point Set.univ A.root) (hy : dist (A.point x.column x.height) y=0) :
    ∃ y' : M.Point (band broad lo) (root M broad lo C),
      y'.column=y.column ∧ y'.height=y.height ∧
      ¬Tiling.NearBoundary width phase (radialValue y') (width/50) := by
…
```
Mentions: OAI.PlanarL1.Columns.Model.Ambient, OAI.PlanarL1.Columns.Model.BandTrees.band, OAI.PlanarL1.Columns.Model.BandTrees.root, OAI.PlanarL1.Columns.Model.BandTrees.RadialInterior, OAI.PlanarL1.Tiling.NearBoundary, OAI.PlanarL1.Columns.Model.BandTrees.radialValue
lemma OAI.PlanarL1.Columns.Model.BandTrees.radialInterior_padding line 51

lemma OAI.PlanarL1.FiniteRandom.radial_pair_probability line 74

Source documentation

Two canonical representatives, possibly in the same component, suffice for the source 0.081 radial allowance. No count of columns is involved.

lemma radial_pair_probability {I : Type*} [Fintype I] [DecidableEq I]
    (m : ℕ) (hm : 10000 ≤ m) (i j : I) (x y : ℝ) {width : ℝ}
    (hw : 0<width) (hsmall : a₁≤width/100000) :
    prob (fun ω : I → Fin (m+1) =>
      NearBoundary width (width/m*(ω i).val) x (width/50+a₁) ∨
      NearBoundary width (width/m*(ω j).val) y (width/50+a₁)) ≤81/1000 := by
…

Mentions: OAI.PlanarL1.FiniteRandom.prob

def OAI.PlanarL1.Columns.Model.VertexBands.bandIndex line 110
def OAI.PlanarL1.Columns.Model.VertexBands.lower line 113
def OAI.PlanarL1.Columns.Model.VertexBands.component line 114
def OAI.PlanarL1.Columns.Model.VertexBands.bandComponent line 117
lemma OAI.PlanarL1.Columns.Model.VertexBands.height_mem line 119
def OAI.PlanarL1.Columns.Model.VertexBands.point line 124
def OAI.PlanarL1.Columns.Model.VertexBands.radial line 134
def OAI.PlanarL1.Columns.Model.VertexBands.Interior line 141
Source documentation
Exactly the literal vertex interior predicate. Narrow containment follows from broad height padding and is included below as a checked consequence.
```
def Interior (q p : ℝ) (phaseD phaseG : MainFamily.BandComponent (M := M) q L U → ℝ)
…
```
Mentions: OAI.PlanarL1.Columns.Model.MainFamily.BandComponent
lemma OAI.PlanarL1.Columns.Model.VertexBands.Interior.narrow_sub line 147
lemma OAI.PlanarL1.Tiling.same_index_of_padded line 163
lemma OAI.PlanarL1.Execution.prob_bind_pure line 176
abbrev OAI.PlanarL1.Columns.Model.VertexBands.HeightChoices line 189
def OAI.PlanarL1.Columns.Model.VertexBands.shift line 190
abbrev OAI.PlanarL1.Columns.Model.VertexBands.RadialChoices line 191
abbrev OAI.PlanarL1.Columns.Model.VertexBands.Choices line 194
def OAI.PlanarL1.Columns.Model.VertexBands.phase line 196
def OAI.PlanarL1.Columns.Model.VertexBands.geometricExecution line 200
def OAI.PlanarL1.Columns.Model.VertexBands.InteriorAt line 206
lemma OAI.PlanarL1.Columns.Model.VertexBands.radial_pair_failure line 210
lemma OAI.PlanarL1.Columns.Model.VertexBands.radial_both_failure line 229
lemma OAI.PlanarL1.Columns.Model.VertexBands.interior_pair_probability line 253
Source documentation
A literal finite sequence of shifts followed by component-indexed radial origins. Component types may depend on the height shifts; using bind avoids a spurious uniform law on a dependent sum.
```
lemma interior_pair_probability (m : ℕ) (hm : 10000 ≤ m) (x y : V)
    (hd : |(v y).height-(v x).height|≤a₂/10000) :
    1/4≤(geometricExecution m L U M).prob
      (fun c => InteriorAt A v hv c x ∧ InteriorAt A v hv c y) := by
…
```
Mentions: OAI.PlanarL1.Columns.Model.VertexBands.geometricExecution, OAI.PlanarL1.Columns.Model.VertexBands.InteriorAt
def OAI.PlanarL1.Columns.Model.PairGeometry.narrowLower line 318
lemma OAI.PlanarL1.Columns.Model.PairGeometry.narrow_height line 319
lemma OAI.PlanarL1.Columns.Model.PairGeometry.gcell_exists line 329
def OAI.PlanarL1.Columns.Model.PairGeometry.position line 334
lemma OAI.PlanarL1.Columns.Model.PairGeometry.partner_exists line 354
def OAI.PlanarL1.Columns.Model.PairGeometry.partner line 369
lemma OAI.PlanarL1.Columns.Model.PairGeometry.partner_column line 372
lemma OAI.PlanarL1.Columns.Model.PairGeometry.partner_height line 374
lemma OAI.PlanarL1.Columns.Model.PairGeometry.partner_dist line 376
lemma OAI.PlanarL1.Columns.Model.PairGeometry.comparison_transport line 380
lemma OAI.PlanarL1.Columns.Model.PairGeometry.partner_value line 384
lemma OAI.PlanarL1.Columns.Model.PairGeometry.position_value line 397
def OAI.PlanarL1.Columns.Model.PairGeometry.Retained line 402
Source documentation
The actual surviving test is just the two descending-path tests and the absence of a low separating tip, after the literal earlier tests.
```
def Retained : Prop :=
…
```
def OAI.PlanarL1.Columns.Model.PairGeometry.seed line 412

lemma OAI.PlanarL1.Columns.Model.OrdinaryState.low_tip_certificate line 445

Source documentation

Failure of the actual circular low-tip test produces the literal source certificate, including its tip and measurable positive label mass.

lemma low_tip_certificate (a : Fin (S.count+1)) {root : Fin n}
    (x y : M.Point (S.chart a).band root) (lo : ℝ)
    (hx : S.name x.column x.height=a) (hy : S.name y.column y.height=a)
    (hxH : x.height ∈ Set.Icc lo (lo+a₂)) (hyH : y.height ∈ Set.Icc lo (lo+a₂))
    (hclose : |(S.chart a).comparison.eval x-(S.chart a).comparison.eval y| ≤ EA)
    (hnear : ∀ e : M.Point (S.chart a).band root,
      (dist x e ≤ 1 ∨ dist y e ≤ 1) → S.name e.column e.height=a)
    (hf : ¬(S.chart a).comparison.NoLowCircular x y (Set.Icc lo (lo+a₂)) j) :
    ∃ (e : M.Point (S.chart a).band root) (b : Fin n) (E : Set Ω),
      e.height ∈ M.heights e.column b ∧ ¬Consecutive e.column b ∧
      Field.CircularTipSeparates e.column b x.column y.column ∧
      (dist x e ≤ 1 ∨ dist y e ≤ 1) ∧
…

Mentions: OAI.PlanarL1.Columns.Consecutive, OAI.PlanarL1.Columns.Model.Field.CircularTipSeparates

lemma OAI.PlanarL1.Columns.Model.OrdinaryState.barrier_refined_separation line 472
lemma OAI.PlanarL1.Columns.Model.Point.eq_coordinates line 499
lemma OAI.PlanarL1.Columns.Model.Field.BandDescent.coordinates line 508
lemma OAI.PlanarL1.Columns.Model.Field.NoLowCircular.symm line 515
lemma OAI.PlanarL1.Columns.Model.Field.NoLowCircular.coordinates line 522
lemma OAI.PlanarL1.Columns.Model.OrdinaryData.descent_coordinates line 532
lemma OAI.PlanarL1.Columns.Model.OrdinaryData.noLow_coordinates line 540
structure OAI.PlanarL1.Columns.Model.RetainedSelection.Witness line 571
Source documentation
A literal surviving partner. This is tested before any group coin or orientation is drawn, and never asserts success of an update.
```
structure Witness (x : V) where
…
```
def OAI.PlanarL1.Columns.Model.RetainedSelection.remaining line 579
abbrev OAI.PlanarL1.Columns.Model.RetainedSelection.Endpoint line 581
instance OAI.PlanarL1.Columns.Model.RetainedSelection.(instance at line 582) line 582
lemma OAI.PlanarL1.Columns.Model.RetainedSelection.mem_remaining line 585
def OAI.PlanarL1.Columns.Model.RetainedSelection.witness line 588
def OAI.PlanarL1.Columns.Model.RetainedSelection.Block line 594
Source documentation
Finite processed broad-component/narrow-band blocks. In particular no infinite family of unused tail bands is randomized.
```
def Block (q p L U : ℝ) := Σ b : MainFamily.BandComponent (M := M) q L U,
…
```
Mentions: OAI.PlanarL1.Columns.Model.MainFamily.BandComponent
instance OAI.PlanarL1.Columns.Model.RetainedSelection.(instance at line 597) line 597
def OAI.PlanarL1.Columns.Model.RetainedSelection.Block.lower line 603
def OAI.PlanarL1.Columns.Model.RetainedSelection.Block.lower₂ line 604
lemma OAI.PlanarL1.Columns.Model.RetainedSelection.Block.sub line 605
def OAI.PlanarL1.Columns.Model.RetainedSelection.block line 614
abbrev OAI.PlanarL1.Columns.Model.RetainedSelection.LocalSeed line 621
def OAI.PlanarL1.Columns.Model.RetainedSelection.rawSeed line 624
abbrev OAI.PlanarL1.Columns.Model.RetainedSelection.Slice line 631
def OAI.PlanarL1.Columns.Model.RetainedSelection.localSeeds line 633
abbrev OAI.PlanarL1.Columns.Model.RetainedSelection.GroupIndex line 636
instance OAI.PlanarL1.Columns.Model.RetainedSelection.(instance at line 638) line 638
def OAI.PlanarL1.Columns.Model.RetainedSelection.group line 641
def OAI.PlanarL1.Columns.Model.RetainedSelection.groupOf line 644
lemma OAI.PlanarL1.Columns.Model.RetainedSelection.localSeeds_self line 649
lemma OAI.PlanarL1.Columns.Model.RetainedSelection.groupOf_seed line 652
lemma OAI.PlanarL1.Columns.Model.RetainedSelection.rawSeed_column line 656
lemma OAI.PlanarL1.Columns.Model.RetainedSelection.rawSeed_height line 658
lemma OAI.PlanarL1.Columns.Model.PairGeometry.broad_lower_eq line 684
lemma OAI.PlanarL1.Columns.Model.PairGeometry.narrow_lower_eq line 693
lemma OAI.PlanarL1.Columns.Model.PairGeometry.Retained.symm line 702
lemma OAI.PlanarL1.Columns.Model.Ambient.coordinate_dist_le line 738
def OAI.PlanarL1.Columns.Model.PairGeometry.Certificate line 762
Source documentation
The source component certificate on literal active labels and an actual terminal link. Its labels, tip and positive mass are not extra input.
```
def Certificate (b : ℝ) : Prop :=
…
```
lemma OAI.PlanarL1.Columns.Model.PairGeometry.certificate_of_excluded line 772
lemma OAI.PlanarL1.Columns.Model.MainFamily.available_of_ball5 line 831
Source documentation
The literal radius-five eligibility test suffices for the full closed one-neighborhood availability of every cell containing this endpoint.
```
lemma available_of_ball5 (c : CellIndex q L U phase) (x : M.Point Set.univ A.root)
    (hx : x.height ∈ domain phase c x.column) {a : Fin (S.count+1)}
    (hname : A.Common S.name x 5 a) : Available A S phase c := by
…
```
Mentions: OAI.PlanarL1.Columns.Model.MainFamily.CellIndex, OAI.PlanarL1.Columns.Model.MainFamily.domain, OAI.PlanarL1.Columns.Model.MainFamily.Available
lemma OAI.PlanarL1.Columns.Model.MainFamily.distinct_cells line 843