pith. machine review for the scientific record. sign in
theorem other other high

cube3_edges

show as:
view Lean formalization →

A three-dimensional cube contains twelve edges by the combinatorial formula E(D) = D · 2^(D-1). Researchers deriving PMNS radiative corrections from cube topology cite this count to fix the solar coefficient at ten times alpha. The verification reduces to direct arithmetic evaluation of the defining expression at D = 3.

claimThe edge count in a three-dimensional cube is $E(3) = 12$, where $E(D) := D · 2^{D-1}$ gives the number of edges in a $D$-cube.

background

The PMNS module derives the integer coefficients 6, 10, and 3/2 in mixing-angle predictions from the topology of a three-dimensional cube. The upstream definition states: Number of edges in a D-cube: E = D · 2^(D-1). This supplies the twelve edges that become the solar correction after subtracting the active pair via 2-step torsion. The local setting is the geometric origin of radiative corrections: atmospheric mixing from six faces, solar mixing from edge-face counting, and Cabibbo from vertex-edge duality, all within the 3D voxel ledger of Recognition Science.

proof idea

The proof is a one-line wrapper that applies native_decide to evaluate the arithmetic expression in the definition of cube_edges_count at D = 3.

why it matters in Recognition Science

This result anchors the solar mixing correction by confirming the edge count of the 3-cube, which yields the coefficient 10 in sin²θ₁₂ = φ^{-2} - 10α. It supports the module's derivation of all three integers from cube topology and aligns with the eight-tick octave and D = 3 spatial dimensions. No downstream theorems are recorded, so the declaration closes a local counting step rather than feeding a larger parent result.

scope and limits

formal statement (Lean)

  78theorem cube3_edges : cube_edges_count 3 = 12 := by native_decide

depends on (1)

Lean names referenced from this declaration's body.