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

cube3_faces

show as:
view Lean formalization →

No prose has been written for this declaration yet. The Lean source and graph data below render without it.

generate prose now

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.