OAI/Combinatorics/PlanarL1/MainStep.lean

GitHub source file

45 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.PlanarL1.Columns.Model.OrdinaryState.represents_named line 16
2. lemma OAI.PlanarL1.Columns.Model.OrdinaryState.contains_named line 23
3. structure OAI.PlanarL1.Columns.Model.OrdinaryState.MainStep line 30

   Source documentation

   Literal deterministic data of a kept eligible main cell. Fresh signs are label coordinates, not assumptions of independence between existing labels.

   structure MainStep (S : OrdinaryState M κ Ω μ) (J : Set ℝ) (root : Fin n) where
   …

   Mentions: OAI.PlanarL1.Columns.Model.OrdinaryState

4. def OAI.PlanarL1.Columns.Model.OrdinaryState.MainStep.data line 57
5. def OAI.PlanarL1.Columns.Model.OrdinaryState.MainStep.comparison line 58
6. lemma OAI.PlanarL1.Columns.Model.OrdinaryState.MainStep.compact_band line 61
7. lemma OAI.PlanarL1.Columns.Model.OrdinaryState.MainStep.old_agreement line 63
8. def OAI.PlanarL1.Columns.Model.OrdinaryState.MainStep.patch line 72
9. def OAI.PlanarL1.Columns.Model.OrdinaryState.MainStep.input line 79
10. def OAI.PlanarL1.Columns.Model.OrdinaryState.MainStep.shield line 82
11. def OAI.PlanarL1.Columns.Model.OrdinaryState.MainStep.shieldConstant line 86
12. lemma OAI.PlanarL1.Columns.Model.OrdinaryState.MainStep.shield_lipschitz line 89
13. def OAI.PlanarL1.Columns.Model.OrdinaryState.MainStep.newData line 108
14. def OAI.PlanarL1.Columns.Model.OrdinaryState.MainStep.newLabels line 111
15. def OAI.PlanarL1.Columns.Model.OrdinaryState.MainStep.choose line 116
16. lemma OAI.PlanarL1.Columns.Model.OrdinaryState.MainStep.patch_inside line 120
17. lemma OAI.PlanarL1.Columns.Model.OrdinaryState.MainStep.chosen_description line 133
18. lemma OAI.PlanarL1.Columns.Model.OrdinaryState.MainStep.unchosen line 194
19. lemma OAI.PlanarL1.Columns.Model.OrdinaryState.MainStep.choose_switch line 210
20. def OAI.PlanarL1.Columns.Model.OrdinaryState.MainStep.apply line 217

    Source documentation

    The exact single kept main-cell update, including the fresh shield label rebase and retention of every old identifier wherever the scalar clip is old.

    noncomputable def apply [SFinite μ] : OrdinaryState M κ (Ω × Bool) (μ.prod Threshold.fair) :=
    …

    Mentions: OAI.PlanarL1.Columns.Model.OrdinaryState, OAI.PlanarL1.Threshold.fair

21. lemma OAI.PlanarL1.Columns.Model.OrdinaryState.MainStep.apply_sets line 224
22. lemma OAI.PlanarL1.Columns.Model.OrdinaryState.MainStep.indicator_inside line 240
23. lemma OAI.PlanarL1.Columns.Model.OrdinaryState.MainStep.old_indicator line 250
24. lemma OAI.PlanarL1.Columns.Model.OrdinaryState.MainStep.movement_exact line 261

    Source documentation

    Actual label mass moved by one kept main cell equals the oriented scalar raise times κ. This compares the new sets with the lifted old sets.

    lemma movement_exact (i : Fin n) (H : ℝ)
        (hi : H ∈ MainCell.domain U.tree U.phase U.cell i) :
        (∫ ω, |(U.patch.apply.activity ω).indicator i H-
          (S.lift.sets.activity ω).indicator i H| ∂(μ.prod Threshold.fair)) =
          κ*(MainCell.replacement U.comparison U.sub_old U.tree U.phase U.cell U.anchor
              U.noise U.error U.shield_offset U.lo (MainCell.cellPoint U.tree U.phase U.cell i H hi)-
            MainCell.old U.comparison U.sub_old (MainCell.cellPoint U.tree U.phase U.cell i H hi)) := by
    …

    Mentions: OAI.PlanarL1.Columns.Model.MainCell.domain, OAI.PlanarL1.Threshold.fair, OAI.PlanarL1.Columns.Model.MainCell.replacement, OAI.PlanarL1.Columns.Model.MainCell.cellPoint, OAI.PlanarL1.Columns.Model.MainCell.old

25. lemma OAI.PlanarL1.Columns.Model.OrdinaryState.MainStep.movement_integrable line 289
26. lemma OAI.PlanarL1.Columns.Model.OrdinaryState.MainStep.movement_bound line 302
27. lemma OAI.PlanarL1.Columns.Model.OrdinaryState.MainStep.movement_or_descent line 321

    Source documentation

    Under the literal padded-cell main test, either there is an actual shortest band descent or the kept-cell movement has the claimed strict positive mass.

    lemma movement_or_descent (w : M.Point J root)
        (hw : w.column ∈ ColumnOrder.componentColumns U.cell)
        {ε : ℝ} (hε : 0<ε) (hεsmall : ε ≤ (1:ℝ)/100)
        (hζ : U.tree.ζ=ε/100) (hE : U.error=ε/1000)
        (hκ : 0<κ)
        (hshield : MainCell.old U.comparison U.sub_old U.anchor+2 ≤
          Clipping.heightShield U.lo U.tree.a (MainCell.old U.comparison U.sub_old U.anchor)
            U.shield_offset w.height)
        (hlow : U.phase+(1:ℝ)/100000+2*U.tree.a <
          dist U.tree.base (w.withHeight U.tree.base.height U.tree.base.inBand))
        (hupp : dist U.tree.base (w.withHeight U.tree.base.height U.tree.base.inBand) <
          U.phase+(1:ℝ)/1000-(1:ℝ)/100000-2*U.tree.a) :
    …

    Mentions: OAI.PlanarL1.ColumnOrder.componentColumns, OAI.PlanarL1.Columns.Model.MainCell.old, OAI.PlanarL1.Clipping.heightShield

28. lemma OAI.PlanarL1.Columns.Model.OrdinaryState.MainStep.old_indicator_named line 375
29. lemma OAI.PlanarL1.Columns.Model.OrdinaryState.MainStep.pair_distance line 386

    Source documentation

    Actual common-label pair distance when one cell is kept and the other endpoint is outside it. The comparison uses old labels, not new chart names.

    lemma pair_distance (x y : M.Point J root)
        (hx : x.column ∈ ColumnOrder.componentColumns U.cell)
        (hy : y.column ∉ ColumnOrder.componentColumns U.cell)
        (hyn : S.name y.column y.height=U.index) :
        (∫ ω, |(U.patch.apply.activity ω).indicator x.column x.height-
            (U.patch.apply.activity ω).indicator y.column y.height| ∂(μ.prod Threshold.fair)) =
          max |x.height-y.height|
            (κ*|MainCell.replacement U.comparison U.sub_old U.tree U.phase U.cell U.anchor
              U.noise U.error U.shield_offset U.lo x-MainCell.old U.comparison U.sub_old y|) := by
    …

    Mentions: OAI.PlanarL1.ColumnOrder.componentColumns, OAI.PlanarL1.Threshold.fair, OAI.PlanarL1.Columns.Model.MainCell.replacement, OAI.PlanarL1.Columns.Model.MainCell.old

30. lemma OAI.PlanarL1.Columns.Model.OrdinaryState.MainStep.separation_of_raise line 416
31. lemma OAI.PlanarL1.Columns.Model.OrdinaryState.MainStep.pair_separation_of_no_descent line 435

    Source documentation

    Literal deterministic favorable branch in the main pair-separation test.

    lemma pair_separation_of_no_descent (x y : M.Point J root)
        (hx : x.column ∈ ColumnOrder.componentColumns U.cell)
        (hy : y.column ∉ ColumnOrder.componentColumns U.cell)
        (hyn : S.name y.column y.height=U.index) (hκ : 0<κ)
        {ε : ℝ} (hε : 0<ε) (hεsmall : ε ≤ (1:ℝ)/100)
        (hζ : U.tree.ζ=ε/100) (hE : U.error=ε/1000)
        (hclose : |MainCell.old U.comparison U.sub_old x-MainCell.old U.comparison U.sub_old y| ≤ U.error)
        (hshield : MainCell.old U.comparison U.sub_old U.anchor+2 ≤
          Clipping.heightShield U.lo U.tree.a (MainCell.old U.comparison U.sub_old U.anchor)
            U.shield_offset x.height)
        (hlow : U.phase+(1:ℝ)/100000+2*U.tree.a <
          dist U.tree.base (x.withHeight U.tree.base.height U.tree.base.inBand))
    …

    Mentions: OAI.PlanarL1.ColumnOrder.componentColumns, OAI.PlanarL1.Columns.Model.MainCell.old, OAI.PlanarL1.Clipping.heightShield

32. structure OAI.PlanarL1.Columns.Model.OrdinaryState.MainBatch line 481

    Source documentation

    A finite family of the actual main-cell proposals. Distinct cells may meet at unchanged boundary points; no disjointness of their closed domains is assumed.

    structure MainBatch (S : OrdinaryState M κ Ω μ) where
    …

    Mentions: OAI.PlanarL1.Columns.Model.OrdinaryState

33. def OAI.PlanarL1.Columns.Model.OrdinaryState.MainBatch.NewIndex line 491
34. instance OAI.PlanarL1.Columns.Model.OrdinaryState.MainBatch.(instance at line 492) line 492
35. def OAI.PlanarL1.Columns.Model.OrdinaryState.MainBatch.newData line 494
36. def OAI.PlanarL1.Columns.Model.OrdinaryState.MainBatch.newLabels line 496
37. def OAI.PlanarL1.Columns.Model.OrdinaryState.MainBatch.chosen line 500
38. def OAI.PlanarL1.Columns.Model.OrdinaryState.MainBatch.choose line 503
39. lemma OAI.PlanarL1.Columns.Model.OrdinaryState.MainBatch.choose_some line 506
40. lemma OAI.PlanarL1.Columns.Model.OrdinaryState.MainBatch.choose_none line 513
41. lemma OAI.PlanarL1.Columns.Model.OrdinaryState.MainBatch.choose_switch line 521
42. def OAI.PlanarL1.Columns.Model.OrdinaryState.MainBatch.sets line 529
43. lemma OAI.PlanarL1.Columns.Model.OrdinaryState.MainBatch.chosen_description line 532
44. lemma OAI.PlanarL1.Columns.Model.OrdinaryState.MainBatch.unchosen line 546
45. def OAI.PlanarL1.Columns.Model.OrdinaryState.MainBatch.apply line 555

    Source documentation

    Actual finite main update, with the chart table containing every ancestor formula and each shield's rebased label variables.

    noncomputable def apply [SFinite μ] : OrdinaryState M κ (Ω × Bool) (μ.prod Threshold.fair) := by
    …

    Mentions: OAI.PlanarL1.Columns.Model.OrdinaryState, OAI.PlanarL1.Threshold.fair