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) ⋯

Parallel validity checking

Table.rowsValidParB splits the index range into chunks and checks them concurrently via Task.spawn. Since Task.spawn fn is definitionally ⟨fn ()⟩, the parallelism is invisible to the logic, and correctness is proved exactly as for the sequential checker. This matters for Noperthedron.exists_solution_table, where native_decide runs this check over a table with ~18.7 million rows.

def Noperthedron.Solution.Table.rowsValidChunkedB (tab : Table) (nTasks chunkSize : ℕ) : Bool

Check all rows of the table for validity, splitting the work into nTasks chunks of size chunkSize that run concurrently via Task.spawn. The leading decide guard ensures that the chunks cover the whole table, so that Table.rowsValid_of_rowsValidChunkedB holds for arbitrary (even nonsensical) values of nTasks and chunkSize.

Equations

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

theorem Noperthedron.Solution.Table.rowsValid_of_rowsValidChunkedB {tab : Table} {nTasks chunkSize : ℕ} (h : tab.rowsValidChunkedB nTasks chunkSize = true) : tab.RowsValid

def Noperthedron.Solution.Table.rowsValidParB (tab : Table) (nTasks : ℕ) : Bool

Parallel analogue of Table.rowsValidB, splitting the table into nTasks chunks of (near-)equal size.

Equations

• tab.rowsValidParB nTasks = tab.rowsValidChunkedB nTasks (Array.size tab / nTasks + 1)

theorem Noperthedron.Solution.Table.rowsValid_of_rowsValidParB {tab : Table} {nTasks : ℕ} (h : tab.rowsValidParB nTasks = true) : tab.RowsValid

theorem Noperthedron.Solution.Table.rowsValidParB_eq_true_iff {tab : Table} {nTasks : ℕ} (hn : 0 < nTasks) : tab.rowsValidParB nTasks = true ↔ tab.RowsValid

The parallel checker is complete: for a positive number of tasks it agrees with Table.RowsValid. (Soundness, which is the direction the final proof needs, holds for any nTasks; see Table.rowsValid_of_rowsValidParB.)

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