inductive Solution.Param : Type

• θ₁ : Param
• φ₁ : Param
• θ₂ : Param
• φ₂ : Param
• α : Param

instance Solution.instBEqParam : BEq Param

Equations

• Solution.instBEqParam = { beq := Solution.instBEqParam.beq }

def Solution.instBEqParam.beq : Param → Param → Bool

Equations

• Solution.instBEqParam.beq x✝ y✝ = (x✝.ctorIdx == y✝.ctorIdx)

instance Solution.instReflBEqParam : ReflBEq Param

instance Solution.instLawfulBEqParam : LawfulBEq Param

def Solution.instReprParam.repr : Param → ℕ → Std.Format

Equations

• Solution.instReprParam.repr Solution.Param.θ₁ prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Solution.Param.θ₁")).group prec✝
• Solution.instReprParam.repr Solution.Param.φ₁ prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Solution.Param.φ₁")).group prec✝
• Solution.instReprParam.repr Solution.Param.θ₂ prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Solution.Param.θ₂")).group prec✝
• Solution.instReprParam.repr Solution.Param.φ₂ prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Solution.Param.φ₂")).group prec✝
• Solution.instReprParam.repr Solution.Param.α prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Solution.Param.α")).group prec✝

instance Solution.instReprParam : Repr Param

Equations

• Solution.instReprParam = { reprPrec := Solution.instReprParam.repr }

instance Solution.instFintypeParam : Fintype Param

Equations

• Solution.instFintypeParam = { elems := { val := ↑Solution.Param.enumList, nodup := Solution.Param.enumList_nodup }, complete := Solution.instFintypeParam._proof_1 }

def Pose.getParam (q : Pose) : Solution.Param → ℝ

Equations

• q.getParam Solution.Param.θ₁ = q.θ₁
• q.getParam Solution.Param.φ₁ = q.φ₁
• q.getParam Solution.Param.θ₂ = q.θ₂
• q.getParam Solution.Param.φ₂ = q.φ₂
• q.getParam Solution.Param.α = q.α

structure Solution.Interval : Type

• min : Param → ℕ
• max : Param → ℕ

def Solution.instDecidableEqInterval.decEq (x✝ x✝¹ : Interval) : Decidable (x✝ = x✝¹)

Equations

• Solution.instDecidableEqInterval.decEq { min := a, max := a_1 } { min := b, max := b_1 } = if h : a = b then h ▸ if h : a_1 = b_1 then h ▸ isTrue ⋯ else isFalse ⋯ else isFalse ⋯

instance Solution.instDecidableEqInterval : DecidableEq Interval

Equations

• Solution.instDecidableEqInterval = Solution.instDecidableEqInterval.decEq

instance Solution.instReprInterval : Repr Interval

Equations

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

structure Solution.Row : Type

A Solution.Row aims to closely model of exactly the data in Steininger and Yurkevich's big CSV file. IDs start from zero. See [SY25] §7.1 for the meaning of all these fields.

• ID : ℕ
• nodeType : ℕ
• nrChildren : ℕ
• IDfirstChild : ℕ
• split : ℕ
• interval : Interval
• S_index : Fin 30
• wx_numerator : ℤ
• wy_numerator : ℤ
• w_denominator : ℕ
• P1_index : ℕ
• P2_index : ℕ
• P3_index : ℕ
• Q1_index : ℕ
• Q2_index : ℕ
• Q3_index : ℕ
• r : ℤ
• sigma_Q : ↥(Finset.Icc 0 1)

@[reducible, inline]

abbrev Solution.Table : Type

Equations

• Solution.Table = Array Solution.Row

def Solution.Row.ValidGlobal (tab : Table) (row : Row) : Prop

Equations

• Solution.Row.ValidGlobal tab row = (row.nodeType = 1 ∧ sorry)

instance Solution.instDecidableValidGlobal (tab : Table) (row : Row) : Decidable (Row.ValidGlobal tab row)

Equations

• Solution.instDecidableValidGlobal tab row = sorry

def Solution.Row.ValidLocal (tab : Table) (row : Row) : Prop

Equations

• Solution.Row.ValidLocal tab row = (row.nodeType = 2 ∧ sorry)

instance Solution.instDecidableValidLocal (tab : Table) (row : Row) : Decidable (Row.ValidLocal tab row)

Equations

• Solution.instDecidableValidLocal tab row = sorry

def Solution.Interval.lower_half (param : Param) (interval : Interval) : Interval

Equations

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

def Solution.Interval.upper_half (param : Param) (interval : Interval) : Interval

Equations

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

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

• split : row.split = 1
• bound0 : row.ID < row.IDfirstChild
• bound1 : row.IDfirstChild < Array.size tab
• bound2 : row.IDfirstChild + 1 < Array.size tab
• first_child_good : tab[row.IDfirstChild].interval = Interval.lower_half param row.interval
• second_child_good : tab[row.IDfirstChild + 1].interval = Interval.upper_half param row.interval

instance 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 Solution.Row.ValidBinarySplit (tab : Table) (row : Row) : Prop

Equations

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

instance Solution.Row.instDecidableValidBinarySplit (tab : Table) (row : Row) : Decidable (ValidBinarySplit tab row)

Equations

• Solution.Row.instDecidableValidBinarySplit tab row = instDecidableAnd

def Solution.cubeFold {α β : Type} (fs : List (α → β → β)) (b : β) : List α → List β

cubeFold fs b as, takes a list of functions fs and a starting value b and a list of coordinates as and returns a list of length |fs|^|as| consisting of all the ways of folding the initial value b through some sequence of functions in fs, using values from as.

Equations

• Solution.cubeFold fs b [] = [b]
• Solution.cubeFold fs b (h :: tl) = List.flatMap (fun (f : α → β → β) => Solution.cubeFold fs (f h b) tl) fs

def Solution.example_interval : Interval

Equations

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

def 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]

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

Equations

• tab.instDecidableHasIntervals start intervals = Nat.decidableForallFin fun (i : Fin intervals.length) => ∃ (h : start + ↑i < Array.size tab), tab[start + ↑i].interval = intervals[i]

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

Equations

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

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

Equations

• Solution.Row.instDecidableValidFullSplit tab row = instDecidableAnd

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

Equations

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

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

Equations

• Solution.Row.instDecidableValidSplit tab row = instDecidableAnd

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

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

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

Equations

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

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

Equations

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

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

Equations

• Solution.Row.instDecidableValidIx tab i row = instDecidableAnd

def Solution.Table.Valid (tab : Table) : Prop

Equations

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

instance Solution.Table.instDecidableValid (tab : Table) : Decidable tab.Valid

Equations

• tab.instDecidableValid = Nat.decidableForallFin fun (i : Fin (Array.size tab)) => Solution.Row.ValidIx tab (↑i) tab[i]

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

def Solution.Table.valid_decidable (tab : Table) : Decidable tab.Valid

Equations

• tab.valid_decidable = inferInstance

def Solution.DENOM : ℝ

The common denominator of θ₁, θ₂, φ₁, φ₂, α rational representation in the table. See [SY25 §7.2]

Equations

• Solution.DENOM = 15360000

noncomputable def Solution.Interval.toPoseInterval (iv : Interval) : PoseInterval

Equations

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

noncomputable def Solution.Row.toPoseInterval (row : Row) : PoseInterval

Equations

• row.toPoseInterval = row.interval.toPoseInterval

instance Solution.instCoeIntervalSetPose : Coe Interval (Set Pose)

Equations

• Solution.instCoeIntervalSetPose = { coe := fun (iv : Solution.Interval) => {q : Pose | q ∈ iv.toPoseInterval} }

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

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

theorem 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 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 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