OrderedState.lean`

45 declarations, 0 contain sorry, 0 declared as axioms

def OAI.PlanarL1.Columns.Model.Field.negate line 11
lemma OAI.PlanarL1.Columns.Model.Field.ordered_negate line 16
def OAI.PlanarL1.Columns.Model.Field.affine line 35
lemma OAI.PlanarL1.Columns.Model.Field.ordered_affine line 47
def OAI.PlanarL1.Columns.Model.Field.weaken line 67
def OAI.PlanarL1.Columns.Model.Field.add line 72
structure OAI.PlanarL1.Columns.Model.OrderedData line 82
Source documentation
The ordered-chart data. The base ordered field never changes during this identifier's lifetime. The auxiliary field is replaced by its actual signed increment history; its bound is 100, not an unbounded sum of the individual increments.
```
structure OrderedData {k : ℕ} (M : Model (k+1)) where
…
```
Mentions: OAI.PlanarL1.Columns.Model
def OAI.PlanarL1.Columns.Model.OrderedData.value line 95
def OAI.PlanarL1.Columns.Model.OrderedData.field line 98
lemma OAI.PlanarL1.Columns.Model.OrderedData.field_value line 102
def OAI.PlanarL1.Columns.Model.OrderedData.install line 109
Source documentation
Install the spatial ordered branch O_F, with zero auxiliary history. The boolean is the conversion back to the old chart orientation. Negation exchanges, rather than discards, the two circular boundary columns.
```
noncomputable def install {I : Set ℝ} (hI : IsClosed I) (hc : I.OrdConnected)
    (L : M.Field I 1) (a b : Fin (k+1)) (ho : L.OrderedFrom a b)
    (c : ℝ) (positive : Bool) : OrderedData M where
…
```
Mentions: OAI.PlanarL1.Columns.Model.OrderedData
lemma OAI.PlanarL1.Columns.Model.OrderedData.install_value line 126
inductive OAI.PlanarL1.Columns.Model.BData line 135
Source documentation
System B has precisely the ordinary and ordered chart alternatives.
```
inductive BData {k : ℕ} (M : Model (k+1))
  | ordinary : OrdinaryData M → BData M
  | ordered : OrderedData M → BData M

namespace BData
variable {k : ℕ} {M : Model (k+1)}
```
Mentions: OAI.PlanarL1.Columns.Model, OAI.PlanarL1.Columns.Model.OrdinaryData, OAI.PlanarL1.Columns.Model.OrderedData
def OAI.PlanarL1.Columns.Model.BData.band line 142
lemma OAI.PlanarL1.Columns.Model.BData.closed line 146
lemma OAI.PlanarL1.Columns.Model.BData.convex line 151
def OAI.PlanarL1.Columns.Model.BData.value line 156
def OAI.PlanarL1.Columns.Model.BData.field line 160
lemma OAI.PlanarL1.Columns.Model.BData.field_value line 165
def OAI.PlanarL1.Columns.Model.BData.Uses line 173
Source documentation
Component restriction is attached only to a genuine point-source chart; the ordered formula is defined on every component of its recorded band.
```
def Uses (D : BData M) (i : Fin (k+1)) : Prop :=
…
```
Mentions: OAI.PlanarL1.Columns.Model.BData
structure OAI.PlanarL1.Columns.Model.BState line 179
def OAI.PlanarL1.Columns.Model.BState.ofOrdinary line 197
def OAI.PlanarL1.Columns.Model.BState.initial line 208
def OAI.PlanarL1.Columns.Model.BState.lift line 212

def OAI.PlanarL1.Columns.Model.BState.append line 226

Source documentation

Finite chart-table extension. Old identifiers are literally retained in the right summand; installing a fresh chart never refines the old regions.

noncomputable def append (S : BState M κ lam Ω μ) (B : SetSystem M Ω μ)
    (m : ℕ) (D : Fin m → BData M) (Z : Fin m → Threshold.Variables Ω μ)
    (choose : Fin (k+1) → ℝ → Option (Fin m))
    (hin : ∀ i H a, choose i H = some a → H ∈ (D a).band)
    (hcomp : ∀ i H a, choose i H = some a → (D a).Uses i)
    (hswitch : ∀ i j H, H ∈ M.heights i j → choose i H = choose j H)
    (hold : ∀ ω i H, choose i H = none →
      ((B.activity ω).active i H ↔ (S.sets.activity ω).active i H))
    (hnew : ∀ ω i H a (hc : choose i H = some a),
      ((B.activity ω).active i H ↔ Threshold.active (Z a) H
        (κ*(D a).value lam i ⟨H,hin i H a hc⟩) ω)) : BState M κ lam Ω μ where
…

Mentions: OAI.PlanarL1.Columns.Model.BState, OAI.PlanarL1.Columns.Model.SetSystem, OAI.PlanarL1.Columns.Model.BData, OAI.PlanarL1.Threshold.Variables, OAI.PlanarL1.Threshold.active

lemma OAI.PlanarL1.Columns.Model.BState.chart_distance line 293

Source documentation

Deterministic chart distance on a common identifier, with no independence assumed between different identifiers.

lemma chart_distance (S : BState M κ lam Ω μ) (i j : Fin (k+1)) (H T : ℝ)
    (he : S.name i H=S.name j T) :
    (∫ ω, |(S.sets.activity ω).indicator i H-(S.sets.activity ω).indicator j T| ∂μ) =
      max |H-T| |κ*(S.chart (S.name i H)).value lam i ⟨H,S.height_in i H⟩-
        κ*(S.chart (S.name j T)).value lam j ⟨T,S.height_in j T⟩| := by
…

Mentions: OAI.PlanarL1.Columns.Model.BState

def OAI.PlanarL1.Columns.Model.BState.oldValue line 326
lemma OAI.PlanarL1.Columns.Model.BState.oldValue_eq line 329
def OAI.PlanarL1.Columns.Model.BState.newValue line 335
lemma OAI.PlanarL1.Columns.Model.BState.newValue_eq line 339
lemma OAI.PlanarL1.Columns.Model.BState.newValue_lipschitz line 345
lemma OAI.PlanarL1.Columns.Model.BState.oldValue_lipschitz line 355
def OAI.PlanarL1.Columns.Model.BState.fieldActivity line 366
Source documentation
A simultaneous same-identifier update, defined by the actual new fields. The boundary estimate is exactly what the ambient complement taper provides. The name map is retained literally; it is not refined to a partition with better-behaved boundaries.
```
noncomputable def fieldActivity (F : ∀ a, M.Field (S.chart a).band 5)
    (hk : 0 ≤ κ) (hsmall : κ*5 ≤ 1/2) (hlam : lam ≤ (1:ℝ≥0)/100)
    (hd : ∀ i H T, S.name i H≠S.name i T →
      |S.newValue F i H-S.oldValue i H| ≤ |H-T|/8)
    (ω : Ω) : Activity M where
…
```
Mentions: OAI.PlanarL1.Columns.Model.Activity
lemma OAI.PlanarL1.Columns.Model.BState.field_indicator line 390
lemma OAI.PlanarL1.Columns.Model.BState.old_indicator line 398
def OAI.PlanarL1.Columns.Model.BState.fieldUpdate line 405
def OAI.PlanarL1.Columns.Model.OrderedData.withAuxiliary line 433
Source documentation
Replace only the auxiliary history; all data determining t_s stay fixed.
```
def withAuxiliary (D : OrderedData M) (u : M.Field D.band 100) : OrderedData M :=
…
```
Mentions: OAI.PlanarL1.Columns.Model.OrderedData
lemma OAI.PlanarL1.Columns.Model.OrderedData.withAuxiliary_value line 436
def OAI.PlanarL1.Columns.Model.BData.Auxiliary line 461
def OAI.PlanarL1.Columns.Model.BData.withAuxiliary line 465
lemma OAI.PlanarL1.Columns.Model.BData.withAuxiliary_band line 470
lemma OAI.PlanarL1.Columns.Model.BData.withAuxiliary_uses line 473
def OAI.PlanarL1.Columns.Model.BData.auxiliaryField line 476
lemma OAI.PlanarL1.Columns.Model.BData.auxiliaryField_value line 482

def OAI.PlanarL1.Columns.Model.BState.withAuxiliary line 498

Source documentation

Simultaneously replace every ordered history, while retaining literally all old chart names and all label variables. Ordinary charts are unaltered.

noncomputable def withAuxiliary (U : ∀ a, (S.chart a).Auxiliary)
    (hk : 0 ≤ κ) (hsmall : κ*5 ≤ 1/2) (hlam : lam ≤ (1:ℝ≥0)/100)
    (hd : ∀ i H T, S.name i H≠S.name i T →
      |S.newValue (fun a => (S.chart a).auxiliaryField (U a) lam hlam) i H-S.oldValue i H| ≤
        |H-T|/8) : BState M κ lam Ω μ where
…

Mentions: OAI.PlanarL1.Columns.Model.BState