Validity over a row source

The proof-producing kernel checker cannot use a flat Array: child lookup in a two-million-row literal would be linear in the child index. Runtime checking, on the other hand, naturally gets rows from an array. Both routes use the same validity predicates below, parameterized only by a total row getter and its logical size. The bounds in the predicates ensure that out-of-range values of the total getter are irrelevant.

structure Noperthedron.Solution.Row.ValidSplitParamAt (get : ℕ → Row) (size : ℕ) (row : Row) (param : Param) : Prop

• id_in_table : row.ID < row.IDfirstChild
• children_in_table : row.IDfirstChild + row.nrChildren ≤ size
• nonzero_children : row.nrChildren ≠ 0
• children_intervals_good (n : Fin row.nrChildren) : (get (row.IDfirstChild + ↑n)).interval = Interval.nth_part param row.interval row.nrChildren n

theorem Noperthedron.Solution.Row.validSplitParamAt_iff (get : ℕ → Row) (size : ℕ) (row : Row) (param : Param) : ValidSplitParamAt get size row param ↔ row.ID < row.IDfirstChild ∧ row.IDfirstChild + row.nrChildren ≤ size ∧ ∃ (nonzero_children : row.nrChildren ≠ 0), ∀ (n : Fin row.nrChildren), (get (row.IDfirstChild + ↑n)).interval = Interval.nth_part param row.interval row.nrChildren n

@[implicit_reducible]

instance Noperthedron.Solution.instDecidableValidSplitParamAt (get : ℕ → Row) (size : ℕ) (row : Row) (param : Param) : Decidable (Row.ValidSplitParamAt get size row param)

Equations

• One or more equations did not get rendered due to their size.

def Noperthedron.Solution.Row.ValidSingleParamSplitAt (get : ℕ → Row) (size : ℕ) (row : Row) : Prop

The row's split code selects a single parameter (via Param.ofSplitCode?), and the row is a valid split of its interval along that parameter.

Equations

• One or more equations did not get rendered due to their size.

@[implicit_reducible]

instance Noperthedron.Solution.instDecidableValidSingleParamSplitAt (get : ℕ → Row) (size : ℕ) (row : Row) : Decidable (Row.ValidSingleParamSplitAt get size row)

Equations

• One or more equations did not get rendered due to their size.

def Noperthedron.Solution.HasIntervalsAt (get : ℕ → Row) (size start : ℕ) (intervals : List Interval) : Prop

Equations

• Noperthedron.Solution.HasIntervalsAt get size start intervals = ∀ (i : Fin intervals.length), start + ↑i < size ∧ (get (start + ↑i)).interval = intervals[i]

@[implicit_reducible]

instance Noperthedron.Solution.instDecidableHasIntervalsAt (get : ℕ → Row) (size start : ℕ) (intervals : List Interval) : Decidable (HasIntervalsAt get size start intervals)

Equations

• Noperthedron.Solution.instDecidableHasIntervalsAt get size start intervals = Noperthedron.Solution.instDecidableHasIntervalsAt._aux_1 get size start intervals

def Noperthedron.Solution.Row.ValidFullSplitAt (get : ℕ → Row) (size : ℕ) (row : Row) : Prop

Equations

• One or more equations did not get rendered due to their size.

@[implicit_reducible]

instance Noperthedron.Solution.Row.instDecidableValidFullSplitAt (get : ℕ → Row) (size : ℕ) (row : Row) : Decidable (ValidFullSplitAt get size row)

Equations

• Noperthedron.Solution.Row.instDecidableValidFullSplitAt get size row = Noperthedron.Solution.Row.instDecidableValidFullSplitAt._aux_1 get size row

def Noperthedron.Solution.Row.ValidSplitAt (get : ℕ → Row) (size : ℕ) (row : Row) : Prop

Equations

• One or more equations did not get rendered due to their size.

@[implicit_reducible]

instance Noperthedron.Solution.Row.instDecidableValidSplitAt (get : ℕ → Row) (size : ℕ) (row : Row) : Decidable (ValidSplitAt get size row)

Equations

• Noperthedron.Solution.Row.instDecidableValidSplitAt get size row = Noperthedron.Solution.Row.instDecidableValidSplitAt._aux_1 get size row

inductive Noperthedron.Solution.Row.ValidAt (get : ℕ → Row) (size : ℕ) (row : Row) : Prop

• asSplit {get : ℕ → Row} {size : ℕ} {row : Row} : ValidSplitAt get size row → ValidAt get size row
• asGlobal {get : ℕ → Row} {size : ℕ} {row : Row} : row.ValidGlobal → ValidAt get size row
• asLocal {get : ℕ → Row} {size : ℕ} {row : Row} : row.ValidLocal → ValidAt get size row

theorem Noperthedron.Solution.Row.validAt_iff (get : ℕ → Row) (size : ℕ) (row : Row) : ValidAt get size row ↔ ValidSplitAt get size row ∨ row.ValidGlobal ∨ row.ValidLocal

@[implicit_reducible]

instance Noperthedron.Solution.instDecidableValidAt (get : ℕ → Row) (size : ℕ) (row : Row) : Decidable (Row.ValidAt get size row)

Equations

• Noperthedron.Solution.instDecidableValidAt get size row = decidable_of_iff (Noperthedron.Solution.Row.ValidSplitAt get size row ∨ row.ValidGlobal ∨ row.ValidLocal) ⋯

def Noperthedron.Solution.Row.ValidIxAt (get : ℕ → Row) (size i : ℕ) : Prop

Equations

• Noperthedron.Solution.Row.ValidIxAt get size i = ((get i).ID = i ∧ Noperthedron.Solution.Row.ValidAt get size (get i) ∧ i < size)

@[implicit_reducible]

instance Noperthedron.Solution.Row.instDecidableValidIxAt (get : ℕ → Row) (size i : ℕ) : Decidable (ValidIxAt get size i)

Equations

• Noperthedron.Solution.Row.instDecidableValidIxAt get size i = Noperthedron.Solution.Row.instDecidableValidIxAt._aux_1 get size i

def Noperthedron.Solution.RowsValidAt (get : ℕ → Row) (size : ℕ) : Prop

Equations

• Noperthedron.Solution.RowsValidAt get size = ∀ (i : Fin size), Noperthedron.Solution.Row.ValidIxAt get size ↑i

def Noperthedron.Solution.Interval.minPose (iv : Interval) : Pose ℝ

The minimum endpoint of an Interval, viewed as a Pose ℝ via Rat.cast.

Equations

• iv.minPose = (PoseInterval.min iv).toReal

def Noperthedron.Solution.Interval.maxPose (iv : Interval) : Pose ℝ

The maximum endpoint of an Interval, viewed as a Pose ℝ via Rat.cast.

Equations

• iv.maxPose = (PoseInterval.max iv).toReal

theorem Noperthedron.Solution.Interval.minPose_le_maxPose (iv : Interval) : iv.minPose ≤ iv.maxPose

def Noperthedron.Solution.Interval.toReal (iv : Interval) : PoseInterval ℝ

Equations

• iv.toReal = PoseInterval.mk iv.minPose iv.maxPose ⋯

def Noperthedron.Solution.Row.toRealInterval (row : Row) : PoseInterval ℝ

Equations

• row.toRealInterval = row.interval.toReal

theorem Noperthedron.Solution.Interval.toReal_center_getParam (iv : Interval) (p : Param) : iv.toReal.center.getParam p = ↑(iv.center p)

Each component of iv.toReal.center (real) is the Rat.cast of the corresponding iv.center (rational).

@[simp]

theorem Noperthedron.Solution.Interval.toReal_center_θ₁ (iv : Interval) : iv.toReal.center.θ₁ = ↑(iv.center Param.θ₁)

@[simp]

theorem Noperthedron.Solution.Interval.toReal_center_θ₂ (iv : Interval) : iv.toReal.center.θ₂ = ↑(iv.center Param.θ₂)

@[simp]

theorem Noperthedron.Solution.Interval.toReal_center_φ₁ (iv : Interval) : iv.toReal.center.φ₁ = ↑(iv.center Param.φ₁)

@[simp]

theorem Noperthedron.Solution.Interval.toReal_center_φ₂ (iv : Interval) : iv.toReal.center.φ₂ = ↑(iv.center Param.φ₂)

@[simp]

theorem Noperthedron.Solution.Interval.toReal_center_α (iv : Interval) : iv.toReal.center.α = ↑(iv.center Param.α)

@[implicit_reducible]

noncomputable instance Noperthedron.Solution.instCoeIntervalSetPoseReal : Coe Interval (Set (Pose ℝ))

The set of poses lying in the rational interval, defined as Set.Icc of the min/max endpoints; agrees definitionally with iv.toReal.

Equations

• Noperthedron.Solution.instCoeIntervalSetPoseReal = { coe := fun (iv : Noperthedron.Solution.Interval) => Set.Icc iv.minPose iv.maxPose }

structure Noperthedron.Solution.ValidTable : Type

• get : ℕ → Row
• size : ℕ
• rows_valid : RowsValidAt self.get self.size
• nonempty : 0 < self.size
• contains_tightInterval : ↑tightInterval ⊆ Set.Icc (self.get 0).interval.minPose (self.get 0).interval.maxPose

theorem Noperthedron.Solution.cube_fold_nonempty_aux {α β : Type} {fs : List (α → β → β)} (hfs : fs ≠ []) (b : β) (as : List α) : 0 < (cubeFold fs b as).length

theorem Noperthedron.Solution.cube_fold_nonempty {α β : Type} {fs : List (α → β → β)} (hfs : fs ≠ []) (b : β) (as : List α) : 1 ≤ (cubeFold fs b as).length

theorem Noperthedron.Solution.cube_fold_halves (h : Param) (tl : List Param) (iv : Interval) (lower upper : Param → Interval → Interval) : cubeFold [lower, upper] iv (h :: tl) = cubeFold [lower, upper] (lower h iv) tl ++ cubeFold [lower, upper] (upper h iv) tl

theorem Noperthedron.Solution.has_intervals_start_in_table (get : ℕ → Row) (size n : ℕ) (ivs : List Interval) (hivs : 1 ≤ ivs.length) (hi : HasIntervalsAt get size n ivs) : n < size

theorem Noperthedron.Solution.has_intervals_concat (get : ℕ → Row) (size start : ℕ) (ivs1 ivs2 : List Interval) : HasIntervalsAt get size start (ivs1 ++ ivs2) ↔ HasIntervalsAt get size start ivs1 ∧ HasIntervalsAt get size (start + ivs1.length) ivs2