structure Noperthedron.Solution.Row.ValidSplitParam (tab : Table) (row : Row) (param : Param) : Prop

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

theorem Noperthedron.Solution.Row.validSplitParam_iff (tab : Table) (row : Row) (param : Param) : ValidSplitParam tab row param ↔ row.ID < row.IDfirstChild ∧ ∃ (children_in_table : row.IDfirstChild + row.nrChildren ≤ Array.size tab) (nonzero_children : row.nrChildren ≠ 0), ∀ (n : Fin row.nrChildren), tab[row.IDfirstChild + ↑n].interval = Interval.nth_part param row.interval row.nrChildren n

@[implicit_reducible]

instance Noperthedron.Solution.instDecidableValidSplitParam (tab : Table) (row : Row) (param : Param) : Decidable (Row.ValidSplitParam tab row param)

Equations

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

def Noperthedron.Solution.Row.ValidSingleParamSplit (tab : Table) (row : Row) : Prop

Equations

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

@[implicit_reducible]

instance Noperthedron.Solution.Row.instDecidableValidSingleParamSplit (tab : Table) (row : Row) : Decidable (ValidSingleParamSplit tab row)

Equations

• Noperthedron.Solution.Row.instDecidableValidSingleParamSplit tab row = Noperthedron.Solution.Row.instDecidableValidSingleParamSplit._aux_1 tab row

def Noperthedron.Solution.Table.HasIntervals (tab : Table) (start : ℕ) (intervals : List Interval) : Prop

Equations

• tab.HasIntervals start intervals = ∀ (i : Fin intervals.length), ∃ (h : start + ↑i < Array.size tab), tab[start + ↑i].interval = intervals[i]

@[implicit_reducible]

instance Noperthedron.Solution.Table.instDecidableHasIntervals (tab : Table) (start : ℕ) (intervals : List Interval) : Decidable (tab.HasIntervals start intervals)

Equations

• tab.instDecidableHasIntervals start intervals = Noperthedron.Solution.Table.instDecidableHasIntervals._aux_1 tab start intervals

def Noperthedron.Solution.Row.ValidFullSplit (tab : Table) (row : Row) : Prop

Equations

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

@[implicit_reducible]

instance Noperthedron.Solution.Row.instDecidableValidFullSplit (tab : Table) (row : Row) : Decidable (ValidFullSplit tab row)

Equations

• Noperthedron.Solution.Row.instDecidableValidFullSplit tab row = Noperthedron.Solution.Row.instDecidableValidFullSplit._aux_1 tab row

def Noperthedron.Solution.Row.ValidSplit (tab : Table) (row : Row) : Prop

Equations

• Noperthedron.Solution.Row.ValidSplit tab row = (row.nodeType = 3 ∧ (Noperthedron.Solution.Row.ValidSingleParamSplit tab row ∨ Noperthedron.Solution.Row.ValidFullSplit tab row))

@[implicit_reducible]

instance Noperthedron.Solution.Row.instDecidableValidSplit (tab : Table) (row : Row) : Decidable (ValidSplit tab row)

Equations

• Noperthedron.Solution.Row.instDecidableValidSplit tab row = Noperthedron.Solution.Row.instDecidableValidSplit._aux_1 tab row

inductive Noperthedron.Solution.Row.Valid (tab : Table) (row : Row) : Prop

• asSplit {tab : Table} {row : Row} : ValidSplit tab row → Valid tab row
• asGlobal {tab : Table} {row : Row} : row.ValidGlobal → Valid tab row
• asLocal {tab : Table} {row : Row} : row.ValidLocal → Valid tab row

theorem Noperthedron.Solution.Row.valid_iff (tab : Table) (row : Row) : Valid tab row ↔ ValidSplit tab row ∨ row.ValidGlobal ∨ row.ValidLocal

@[implicit_reducible]

instance Noperthedron.Solution.instDecidableValid (tab : Table) (row : Row) : Decidable (Row.Valid tab row)

Equations

• Noperthedron.Solution.instDecidableValid tab row = decidable_of_iff (Noperthedron.Solution.Row.ValidSplit tab row ∨ row.ValidGlobal ∨ row.ValidLocal) ⋯

def Noperthedron.Solution.Row.ValidIx (tab : Table) (i : ℕ) (row : Row) : Prop

Equations

• Noperthedron.Solution.Row.ValidIx tab i row = (row.ID = i ∧ Noperthedron.Solution.Row.Valid tab row ∧ row.ID < Array.size tab)

@[implicit_reducible]

instance Noperthedron.Solution.Row.instDecidableValidIx (tab : Table) (i : ℕ) (row : Row) : Decidable (ValidIx tab i row)

Equations

• Noperthedron.Solution.Row.instDecidableValidIx tab i row = Noperthedron.Solution.Row.instDecidableValidIx._aux_1 tab i row

def Noperthedron.Solution.Table.RowsValid (tab : Table) : Prop

Equations

• tab.RowsValid = ∀ (i : Fin (Array.size tab)), Noperthedron.Solution.Row.ValidIx tab (↑i) tab[i]

theorem Noperthedron.Solution.Table.RowsValid.valid_at {tab : Table} (htab : tab.RowsValid) {i : ℕ} (hi : i < Array.size tab) : Row.ValidIx tab i tab[i]

@[implicit_reducible]

instance Noperthedron.Solution.Table.RowsValid.decidable (tab : Table) : Decidable tab.RowsValid

Equations

• Noperthedron.Solution.Table.RowsValid.decidable tab = decidable_of_iff (Noperthedron.Solution.Table.rowsValidB✝ tab = true) ⋯

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

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

• table : Table
• rows_valid : self.table.RowsValid
• nonempty : 0 < Array.size self.table
• contains_tightInterval : ↑tightInterval ⊆ Set.Icc self.table[0].interval.minPose self.table[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 (tab : Table) (n : ℕ) (ivs : List Interval) (hivs : 1 ≤ ivs.length) (hi : tab.HasIntervals n ivs) : n < Array.size tab

theorem Noperthedron.Solution.has_intervals_concat (tab : Table) (start : ℕ) (ivs1 ivs2 : List Interval) : tab.HasIntervals start (ivs1 ++ ivs2) ↔ tab.HasIntervals start ivs1 ∧ tab.HasIntervals (start + ivs1.length) ivs2