def CauchyFunctional.isCauchyAdditive (f : (Fin 3 → ℤ) → ℝ) (G : HypergraphZ3.TriadHypergraph) : Prop

An additive Cauchy function $f : \mathbb{Z}^3 \to \mathbb{R}$ on the Triad Hypergraph. It must satisfy $f(k) = f(p) + f(q)$ for all hyperedges $k = p + q$.

Equations

• CauchyFunctional.isCauchyAdditive f G = ∀ (k p q : Fin 3 → ℤ), G.is_hyperedge k p q → f k = f p + f q

Cauchy Functional Equation on ℤ³ — Full Proof

We prove that every additive function on the triad hypergraph is linear. The key ingredient is the connectivity theorem hypergraph_connected_3D: every vector in ℤ³ can be built from the standard basis via addition. The proof proceeds by induction on IsConstructible.

theorem CauchyFunctional.cauchy_additive_is_linear (f : HypergraphZ3.Z3 → ℝ) (G : HypergraphZ3.TriadHypergraph) (hG : ∀ (p q : Fin 3 → ℤ), G.is_hyperedge (p + q) p q) (h_add : isCauchyAdditive f G) : ∃ (omega_vec : Fin 3 → ℝ), ∀ (k : HypergraphZ3.Z3), f k = ∑ i : Fin 3, omega_vec i * ↑(k i)

Theorem (Cauchy Linearity on ℤ³): Every Cauchy-additive function on the full ℤ³ triad hypergraph is linear. If f(k) = f(p) + f(q) whenever the hypergraph says k = p + q, then f(k) = ω · k for some constant vector ω ∈ ℝ³, where ωᵢ = f(eᵢ).

The hypothesis hG asserts the hypergraph contains every triad (p+q, p, q), which is trivially rfl for the default TriadHypergraph.

structure CauchyFunctional.CauchyUnicity : Prop

The CauchyUnicity structure can now be instantiated from the theorem above.

• linear_solution (f : (Fin 3 → ℤ) → ℝ) (G : HypergraphZ3.TriadHypergraph) (h_additive : isCauchyAdditive f G) : ∃ (omega_vec : Fin 3 → ℝ), ∀ (k : Fin 3 → ℤ), f k = ∑ i : Fin 3, omega_vec i * ↑(k i)