KuhnCells

Ported from scottnarmstrong/Superdiffusion at 7f20476385d4af418f110303085ad0740c9eba46. Module imports, support namespace and local option directives adapted for Lean Pool.

Triadic simplices and the standard simplicial decomposition S_j(□)

This module defines a local implementation of the simplex notation in ABK26's "Triadic cubes and simplices" paragraph, which is the geometric input of e.SW.def:

• the model ordered simplex and the triadic simplex △_n^π(z) of e.simplex.def;
• vertices V(△) and the fact that there are d + 1 of them;
• the standard simplicial decomposition S_j(□) of a triadic cube into simplices of size 3^j, together with its cardinality 3^{d(scale − j)} · d!, its exactness as a partition, and its nesting under further triadic subdivision.

Carriers

A simplex is indexed by a KuhnCell: a triadic support cube together with a permutation of the coordinates. Its open realization openCarrier is the manuscript's △_n^π(z) verbatim. Because the open simplices of a cube omit their common faces, an exact (rather than almost-everywhere) partition needs a boundary convention; carrier is the canonical half-open realization obtained by breaking coordinate ties with Tuple.sort. closedCarrier is the closure. The three are related by openCarrier ⊆ carrier ⊆ closedCarrier.

Reading notes (recorded)

• The manuscript writes S_n(z+□_m) = {z + △_n^π(z') : z' ∈ 3^n ℤ^d, △_n^π(z') ⊆ □_m}. Since the triadic grids are nested, △_n^π(z') ⊆ □_m selects exactly the scale-n triadic descendants of □_m; that is the indexing taken here (descendantsAtScale). The condition n ≤ m of the display is carried as an explicit hypothesis where it is used; outside that range triadicSimplexPartition is empty, matching descendantsAtScale.
• No face-to-face or simplicial-complex claim is made here or anywhere downstream.

References

• ABK26, (e.simplex.def).

The model ordered simplex

def Algsuperdiff.Section3.Provider.Whitney.orderedUnitSimplex {d : ℕ} (pi : Equiv.Perm (Fin d)) : Set (HCPolySupport.Vec d)

The model open simplex of e.simplex.def: {x ∈ ℝ^d: -1/2 < x_{π(1)} < ⋯ < x_{π(d)} < 1/2}, written as the conjunction of the coordinate box and the π-ordering. mem_orderedUnitSimplex_iff_chain shows this is the printed chain.

Equations

• Algsuperdiff.Section3.Provider.Whitney.orderedUnitSimplex pi = {x : HCPolySupport.Vec d | (∀ (i : Fin d), -(1 / 2) < x i ∧ x i < 1 / 2) ∧ ∀ (i j : Fin d), ↑i < ↑j → x (pi i) < x (pi j)}

def Algsuperdiff.Section3.Provider.Whitney.triadicSimplex {d : ℕ} (n : ℤ) (z : HCPolySupport.Vec d) (pi : Equiv.Perm (Fin d)) : Set (HCPolySupport.Vec d)

ABK26 e.simplex.def: the triadic simplex of size 3^n based at z, △_n^π(z) = z + 3^n · {x : -1/2 < x_{π(1)} < ⋯ < x_{π(d)} < 1/2}.

Equations

• Algsuperdiff.Section3.Provider.Whitney.triadicSimplex n z pi = (fun (x : HCPolySupport.Vec d) => z + 3 ^ n • x) '' Algsuperdiff.Section3.Provider.Whitney.orderedUnitSimplex pi

theorem Algsuperdiff.Section3.Provider.Whitney.mem_triadicSimplex_iff {d : ℕ} {n : ℤ} {z : HCPolySupport.Vec d} {pi : Equiv.Perm (Fin d)} {y : HCPolySupport.Vec d} : y ∈ triadicSimplex n z pi ↔ (∀ (i : Fin d), -(1 / 2) * 3 ^ n < y i - z i ∧ y i - z i < 1 / 2 * 3 ^ n) ∧ ∀ (i j : Fin d), ↑i < ↑j → y (pi i) - z (pi i) < y (pi j) - z (pi j)

The translated/rescaled membership test for △_n^π(z).

Kuhn cells

structure Algsuperdiff.Section3.Provider.Whitney.KuhnCell (d : ℕ) : Type

One triadic simplex, indexed by its support cube and the coordinate order of e.simplex.def.

• supportCube : HCPolySupport.TriadicCube d

  The triadic cube containing the simplex; its size is the simplex size.

• order : Equiv.Perm (Fin d)

  The permutation π of e.simplex.def.

def Algsuperdiff.Section3.Provider.Whitney.instDecidableEqKuhnCell.decEq {d✝ : ℕ} (x✝ x✝¹ : KuhnCell d✝) : Decidable (x✝ = x✝¹)

Equations

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

@[instance_reducible]

instance Algsuperdiff.Section3.Provider.Whitney.instDecidableEqKuhnCell {d✝ : ℕ} : DecidableEq (KuhnCell d✝)

Equations

• Algsuperdiff.Section3.Provider.Whitney.instDecidableEqKuhnCell = Algsuperdiff.Section3.Provider.Whitney.instDecidableEqKuhnCell.decEq

noncomputable def Algsuperdiff.Section3.Provider.Whitney.triadicLocalCoordinate {d : ℕ} (Q : HCPolySupport.TriadicCube d) (x : HCPolySupport.Vec d) (i : Fin d) : ℝ

Coordinates centered at the index point of a triadic cube.

Equations

• Algsuperdiff.Section3.Provider.Whitney.triadicLocalCoordinate Q x i = x i - ↑(Q.index i) * HCPolySupport.cubeScaleFactor Q

def Algsuperdiff.Section3.Provider.Whitney.KuhnCell.openCarrier {d : ℕ} (T : KuhnCell d) : Set (HCPolySupport.Vec d)

The manuscript's open simplex △_{scale}^{order}(center) of a Kuhn cell.

Equations

• T.openCarrier = Algsuperdiff.Section3.Provider.Whitney.triadicSimplex T.supportCube.scale (HCPolySupport.cubeCenter T.supportCube) T.order

theorem Algsuperdiff.Section3.Provider.Whitney.KuhnCell.mem_openCarrier_iff {d : ℕ} {T : KuhnCell d} {x : HCPolySupport.Vec d} : x ∈ T.openCarrier ↔ x ∈ HCPolySupport.openCubeSet T.supportCube ∧ ∀ (i j : Fin d), ↑i < ↑j → triadicLocalCoordinate T.supportCube x (T.order i) < triadicLocalCoordinate T.supportCube x (T.order j)

theorem Algsuperdiff.Section3.Provider.Whitney.KuhnCell.openCarrier_subset_openCubeSet {d : ℕ} (T : KuhnCell d) : T.openCarrier ⊆ HCPolySupport.openCubeSet T.supportCube

def Algsuperdiff.Section3.Provider.Whitney.KuhnCell.carrier {d : ℕ} (T : KuhnCell d) : Set (HCPolySupport.Vec d)

The canonical half-open realization. Tuple.sort assigns each coordinate tie to exactly one cell, which turns the family of open simplices of a cube into an exact partition of the half-open cube.

Equations

• T.carrier = {x : HCPolySupport.Vec d | x ∈ HCPolySupport.cubeSet T.supportCube ∧ T.order = Tuple.sort (Algsuperdiff.Section3.Provider.Whitney.triadicLocalCoordinate T.supportCube x)}

theorem Algsuperdiff.Section3.Provider.Whitney.KuhnCell.carrier_subset_cubeSet {d : ℕ} (T : KuhnCell d) : T.carrier ⊆ HCPolySupport.cubeSet T.supportCube

theorem Algsuperdiff.Section3.Provider.Whitney.KuhnCell.openCarrier_subset_carrier {d : ℕ} (T : KuhnCell d) : T.openCarrier ⊆ T.carrier

def Algsuperdiff.Section3.Provider.Whitney.KuhnCell.closedCarrier {d : ℕ} (T : KuhnCell d) : Set (HCPolySupport.Vec d)

The closed simplex: the closed support cube together with the weak order-monotonicity of the local coordinates.

Equations

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

theorem Algsuperdiff.Section3.Provider.Whitney.KuhnCell.carrier_subset_closedCarrier {d : ℕ} (T : KuhnCell d) : T.carrier ⊆ T.closedCarrier

theorem Algsuperdiff.Section3.Provider.Whitney.KuhnCell.openCarrier_subset_closedCarrier {d : ℕ} (T : KuhnCell d) : T.openCarrier ⊆ T.closedCarrier

Vertices

noncomputable def Algsuperdiff.Section3.Provider.Whitney.KuhnCell.vertex {d : ℕ} (T : KuhnCell d) (k : Fin (d + 1)) : HCPolySupport.Vec d

V(△): the k-th vertex of a Kuhn cell. It raises the last k coordinates in the cell's order to the upper face and leaves the rest on the lower face; k = 0 is the lower corner and k = d the upper corner.

Disclosure (definitional stand-in). ABK26 defines a vertex of a simplex to be an extreme point of that simplex, and then observes that there are d+1 of them. This declaration is instead the explicit corner formula, so it is a stand-in for the printed definition, not a transcription of it. What is proved here is that the formula proves in the cell (vertex_mem_closedCarrier), is injective, and yields exactly d+1 points (ncard_vertexSet, the printed count).

Equations

• T.vertex k i = (↑(T.supportCube.index i) + if d ≤ ↑((Equiv.symm T.order) i) + ↑k then 1 / 2 else -(1 / 2)) * HCPolySupport.cubeScaleFactor T.supportCube

def Algsuperdiff.Section3.Provider.Whitney.KuhnCell.vertexSet {d : ℕ} (T : KuhnCell d) : Set (HCPolySupport.Vec d)

V(△): the vertex set of a Kuhn cell.

Equations

• T.vertexSet = Set.range T.vertex

theorem Algsuperdiff.Section3.Provider.Whitney.KuhnCell.vertex_mem_closedCarrier {d : ℕ} (T : KuhnCell d) (k : Fin (d + 1)) : T.vertex k ∈ T.closedCarrier

The standard simplicial decomposition S_j(□)

def Algsuperdiff.Section3.Provider.Whitney.kuhnCellEquiv {d : ℕ} : HCPolySupport.TriadicCube d × Equiv.Perm (Fin d) ≃ KuhnCell d

The enumeration equivalence used to count the cells of a decomposition.

Equations

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

def Algsuperdiff.Section3.Provider.Whitney.triadicSimplexPartition {d : ℕ} (Q : HCPolySupport.TriadicCube d) (j : ℤ) : Finset (KuhnCell d)

ABK26 S_j(□): the decomposition of the triadic cube Q into the triadic simplices of size 3^j supported on its scale-j triadic descendants. Empty when j > Q.scale, matching the display's range j ≤ m.

Equations

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

@[simp]

theorem Algsuperdiff.Section3.Provider.Whitney.mem_triadicSimplexPartition_iff {d : ℕ} {Q : HCPolySupport.TriadicCube d} {j : ℤ} {T : KuhnCell d} : T ∈ triadicSimplexPartition Q j ↔ T.supportCube ∈ HCPolySupport.descendantsAtScale Q j

theorem Algsuperdiff.Section3.Provider.Whitney.triadicSimplexPartition_eq_empty {d : ℕ} {Q : HCPolySupport.TriadicCube d} {j : ℤ} (hj : Q.scale < j) : triadicSimplexPartition Q j = ∅

theorem Algsuperdiff.Section3.Provider.Whitney.supportCube_scale_eq_of_mem_triadicSimplexPartition {d : ℕ} {Q : HCPolySupport.TriadicCube d} {j : ℤ} (hj : j ≤ Q.scale) {T : KuhnCell d} (hT : T ∈ triadicSimplexPartition Q j) : T.supportCube.scale = j

The size clause of S_j(□): every simplex of S_j(□) has size 3^j.

theorem Algsuperdiff.Section3.Provider.Whitney.cubeSet_eq_iUnion_triadicSimplexPartition {d : ℕ} (Q : HCPolySupport.TriadicCube d) {j : ℤ} (hj : j ≤ Q.scale) : HCPolySupport.cubeSet Q = ⋃ T ∈ ↑(triadicSimplexPartition Q j), T.carrier

The canonical half-open cells of S_j(□) cover the half-open cube exactly.

theorem Algsuperdiff.Section3.Provider.Whitney.KuhnCell.disjoint_carrier_of_supportCube_eq {d : ℕ} {T U : KuhnCell d} (hTU : T ≠ U) (hsupport : T.supportCube = U.supportCube) : Disjoint T.carrier U.carrier

theorem Algsuperdiff.Section3.Provider.Whitney.triadicSimplexPartition_pairwiseDisjoint {d : ℕ} (Q : HCPolySupport.TriadicCube d) (j : ℤ) : (↑(triadicSimplexPartition Q j)).PairwiseDisjoint KuhnCell.carrier

The half-open cells of S_j(□) are pairwise disjoint, boundaries included.

theorem Algsuperdiff.Section3.Provider.Whitney.triadicSimplexPartition_openCarrier_pairwiseDisjoint {d : ℕ} (Q : HCPolySupport.TriadicCube d) (j : ℤ) : (↑(triadicSimplexPartition Q j)).PairwiseDisjoint KuhnCell.openCarrier

The manuscript's open simplices of S_j(□) are pairwise disjoint.

Nesting of the standard decompositions

def Algsuperdiff.Section3.Provider.Whitney.childKuhnOrderKey {d : ℕ} (digits : Fin d → Fin 3) (pi : Equiv.Perm (Fin d)) (i : Fin d) : Lex (ℕ × ℕ)

The lexicographic key that coarsens a child order across one triadic subdivision: first the child's digit in that coordinate, then the child's own rank.

Equations

• Algsuperdiff.Section3.Provider.Whitney.childKuhnOrderKey digits pi i = toLex (↑(digits i), ↑((Equiv.symm pi) i))

theorem Algsuperdiff.Section3.Provider.Whitney.childKuhnOrderKey_injective {d : ℕ} (digits : Fin d → Fin 3) (pi : Equiv.Perm (Fin d)) : Function.Injective (childKuhnOrderKey digits pi)

def Algsuperdiff.Section3.Provider.Whitney.coarsenedChildKuhnOrder {d : ℕ} (digits : Fin d → Fin 3) (pi : Equiv.Perm (Fin d)) : Equiv.Perm (Fin d)

The parent order induced by a child cube's digits and the child's order.

Equations

• Algsuperdiff.Section3.Provider.Whitney.coarsenedChildKuhnOrder digits pi = Tuple.sort (Algsuperdiff.Section3.Provider.Whitney.childKuhnOrderKey digits pi)

theorem Algsuperdiff.Section3.Provider.Whitney.exists_selfSimplex_openCarrier_superset {d : ℕ} (Q : HCPolySupport.TriadicCube d) (depth : ℕ) {T : KuhnCell d} : T.supportCube ∈ HCPolySupport.descendantsAtDepth Q depth → ∃ U ∈ triadicSimplexPartition Q Q.scale, T.openCarrier ⊆ U.openCarrier

Every simplex of a deeper decomposition of Q lies in one of the d! simplices of Q itself.

theorem Algsuperdiff.Section3.Provider.Whitney.triadicSimplexPartition_refines_openCarrier {d : ℕ} (Q : HCPolySupport.TriadicCube d) {j j' : ℤ} (hj : j ≤ Q.scale) (hj' : j' ≤ j) {T : KuhnCell d} (hT : T ∈ triadicSimplexPartition Q j') : ∃ U ∈ triadicSimplexPartition Q j, T.openCarrier ⊆ U.openCarrier

Nested standard decompositions. Every simplex of the finer decomposition S_{j'}(□) lies inside a simplex of any coarser decomposition S_j(□), j' ≤ j ≤ Q.scale. This is the only cross-scale compatibility that e.SW.def supports.