pith. machine review for the scientific record. sign in
theorem proved term proof high

color_offset_eq

show as:
view Lean formalization →

Color offset is shown to equal 4 by direct reduction to the edges-per-face count in three dimensions. Researchers deriving particle baselines in Recognition Science cite this when fixing the quark rung from cube geometry. The proof applies the D=3 edges theorem in one step.

claimThe color offset, defined as the number of edges per face of the 3-cube, equals $4$.

background

This result sits in the module deriving baseline rung integers from the combinatorics of the 3-cube Q₃ once D=3 is fixed. The color offset is defined as edges_per_face D. Upstream, edges_per_face_at_D3 states: At D = 3: edges per face = 4. The module upgrades several boundary assumptions to derived status, including color offset as B-25 with value 2^(D-1).

proof idea

The proof is a one-line wrapper that applies the edges_per_face_at_D3 theorem directly.

why it matters in Recognition Science

This theorem supplies the value 4 for color offset (B-25), matching the quark baseline and feeding the neutrino rung derivation. It closes one entry in the baseline derivations table, confirming all such integers trace to D=3. In the framework it supports the mass formula on the phi-ladder and the eight-tick octave.

scope and limits

formal statement (Lean)

 190theorem color_offset_eq : color_offset = 4 := by

proof body

Term-mode proof.

 191  exact edges_per_face_at_D3
 192
 193/-- Color offset equals quark baseline (same geometric origin). -/

used by (1)

From the project-wide theorem graph. These declarations reference this one in their body.

depends on (2)

Lean names referenced from this declaration's body.