@[reducible, inline]

abbrev HypergraphZ3.Z3 : Type

Z3 is the 3D integer lattice

Equations

• HypergraphZ3.Z3 = (Fin 3 → ℤ)

def HypergraphZ3.is_resonant (k p q : Z3) : Prop

The resonance condition for a triad: k = p + q

Equations

• HypergraphZ3.is_resonant k p q = (k = p + q)

structure HypergraphZ3.TriadHypergraph : Type

The Triad Hypergraph $\mathcal{G}(\mathbb{Z}^3)$. A hyperedge exists between nodes $k, p, q \in \mathbb{Z}^3$ if $k = p + q$. This graph describes the exact resonant nonlinear energy transfer channels in the discrete Fourier space.

• is_hyperedge (k p q : Fin 3 → ℤ) : Prop

  A hyperedge is a set of 3 nodes sum-constrained.

def HypergraphZ3.e (i : Fin 3) : Z3

The standard basis vectors for Z3

Equations

• HypergraphZ3.e i j = if i = j then 1 else 0

inductive HypergraphZ3.IsConstructible : Z3 → Prop

A vector is constructible if it can be generated from the standard basis and their opposites via the resonance condition.

• zero : IsConstructible 0
• base_pos (i : Fin 3) : IsConstructible (e i)
• base_neg (i : Fin 3) : IsConstructible (-e i)
• add (p q : Z3) (hp : IsConstructible p) (hq : IsConstructible q) : IsConstructible (p + q)

inductive HypergraphZ3.IsConstructible1D : ℤ → Prop

To establish the methodology cleanly, we demonstrate 1D connectiveness on ℤ first, avoiding any 'sorry'.

• zero : IsConstructible1D 0
• base_pos : IsConstructible1D 1
• base_neg : IsConstructible1D (-1)
• add (p q : ℤ) (hp : IsConstructible1D p) (hq : IsConstructible1D q) : IsConstructible1D (p + q)

theorem HypergraphZ3.hypergraph_connected_1D_pos (k : ℕ) : IsConstructible1D ↑k

theorem HypergraphZ3.hypergraph_connected_1D_neg (k : ℕ) : IsConstructible1D (-↑k)

theorem HypergraphZ3.hypergraph_connected_1D (k : ℤ) : IsConstructible1D k

theorem HypergraphZ3.constructible_axis_pos (k : ℕ) (i : Fin 3) : IsConstructible fun (j : Fin 3) => if i = j then ↑k else 0

theorem HypergraphZ3.constructible_axis_neg (k : ℕ) (i : Fin 3) : IsConstructible fun (j : Fin 3) => if i = j then -↑k else 0

theorem HypergraphZ3.constructible_axis (n : ℤ) (i : Fin 3) : IsConstructible fun (j : Fin 3) => if i = j then n else 0

theorem HypergraphZ3.hypergraph_connected_3D (k : Z3) : IsConstructible k