Physics Cube Spectrum

The cube's spectrum

The three-dimensional cube, the unit cell of the integer lattice, has 8 vertices, 12 edges, and 6 faces. Its graph Laplacian, a matrix that records how each vertex connects to its neighbors, has eigenvalues {0, 2, 2, 2, 4, 4, 4, 6} with multiplicities {1, 3, 3, 1}. These multiplicities are the binomial coefficients C(3,k), the same numbers that appear in Pascal's triangle. The cube's automorphism group, the set of symmetries that map the cube to itself, has order 48, equal to 3! · 2³.

These facts are classical combinatorics, known since the nineteenth century. The spectral gap, the difference between the smallest nonzero eigenvalue and zero, is 2. The largest eigenvalue is 6, which is twice the degree of each vertex. The sum of all eigenvalues equals the degree times the number of vertices, a general identity for any graph. The cube also satisfies Euler's formula: vertices plus faces equals edges plus two.

In Recognition Science, the cube's spectrum enters through the framework's critical exponent corrections. The framework models physical systems as discrete recognition events recorded in a ledger, a discrete record of events. The cube provides the structural numbers that appear in the correction-to-scaling structure: the face-pair count 18 appears in the η₂ correction, and the simplex vertex count 4 appears in the η₁ correction. The ratio of consecutive eigenvalues, 4/2 = 2, governs the subleading renormalization group eigenvalue.

The module formalizes these properties in a machine-checked library of formal theorems. It proves the cube's Euler relation, the eigenvalue count matching the vertex count, the trace identity, the binomial multiplicities, the automorphism group order, and the face-pair and simplex counts. A certificate structure bundles all these facts into a single object that can be passed to other proofs.

The practical consequence is that the numbers 18 and 4, which appear in the framework's corrections to critical exponents, are not arbitrary. They are forced by the cube's combinatorial structure. The module makes this dependence explicit and machine-checkable, so the corrections rest on proved combinatorial facts rather than on numerical coincidence.

def Q3_vertices : ℕ := 8

def Q3_edges : ℕ := 12

def Q3_faces : ℕ := 6

def Q3_laplacian_eigenvalues : List ℕ := [0, 2, 2, 2, 4, 4, 4, 6]

/-- The multiplicities are {1, 3, 3, 1} = binomial coefficients C(3,k). -/
def Q3_multiplicities : List ℕ := [1, 3, 3, 1]

theorem Q3_aut_order_eq : Q3_aut_order = Nat.factorial Q3_degree * 2 ^ Q3_degree := by
  unfold Q3_aut_order Q3_degree; native_decide

theorem Q3_face_pair_count_eq : Q3_face_pair_count = 18 := by
  unfold Q3_face_pair_count Q3_degree; omega

theorem Q3_simplex_vertices_eq : Q3_simplex_vertices = 4 := by
  unfold Q3_simplex_vertices Q3_degree; omega

What this page does not claim

The module does not derive the critical exponents themselves, only the structural numbers that appear in them. The connection between the cube's spectrum and physical measurements is not established in this module.

Verify this page

Every tagged claim above names its theorem. To check one yourself rather than trust this page, elaborate the source module with Lean 4 and audit its axiom basis:

$ lake env lean IndisputableMonolith/Physics/CubeSpectrum.lean
expected axiom basis: [propext, Classical.choice, Quot.sound] (the Lean kernel's standard three; no RS-specific axioms)

A page whose claims cannot be reproduced this way does not ship. In production, every anchor links to the exact declaration in the public source release, and this block carries the build receipt for the page itself.

Derived articles

This page is generated by a question-recursion engine: the questions its answers raise become the next pages. The current agenda, with open targets marked red: