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

cube3_faces

show as:
view Lean formalization →

The face count of the three-dimensional hypercube equals six by the standard formula for hypercube faces. Researchers deriving radiative corrections to the PMNS mixing angles cite this to obtain the atmospheric coefficient 6α. The proof reduces immediately to reflexivity once the hypercube face definition is unfolded.

claimThe number of faces of the three-dimensional hypercube equals six: $F_3 = 6$.

background

In the PMNS radiative correction module, integer coefficients for mixing angle predictions are extracted from the topology of the three-dimensional cube. The atmospheric correction uses the face count directly. Upstream, the face count function is defined as twice the dimension: cube_faces d = 2d. This matches the general hypercube geometry where a D-cube has 2D faces. The module sets the local setting by linking cube faces to vacuum polarization contributions in the μ-τ sector.

proof idea

The proof is a one-line reflexivity that applies the definition cube_faces d := 2 * d at d=3.

why it matters in Recognition Science

This declaration supplies the integer 6 that appears in the atmospheric mixing prediction sin²θ₂₃ = ½ + 6α. It closes the geometric derivation step for the atmospheric sector within the cube topology framework. The result aligns with the Recognition Science assignment of D=3 spatial dimensions and supports the eight-tick octave closure for the reactor angle.

scope and limits

formal statement (Lean)

  79theorem cube3_faces : cube_faces 3 = 6 := rfl

proof body

Term-mode proof.

  80
  81/-! ## Derivation of the Coefficient 6 (Atmospheric) -/
  82
  83/-- The atmospheric correction coefficient is the face count of a 3-cube.
  84
  85    **Physical interpretation**: Each of the 6 faces of the cubic ledger
  86    contributes one unit of vacuum polarization to the atmospheric mixing.
  87    The μ-τ sector, being maximally mixed (sin²θ₂₃ ≈ 1/2), receives a
  88    symmetric correction from all faces. -/

depends on (24)

Lean names referenced from this declaration's body.