`cube_faces`

definition

show as: view math explainer →

module: IndisputableMonolith.Physics.PMNSCorrections
domain: Physics
line: 69 · github
papers citing: none yet

open explainer

Generate a durable explainer page for this declaration.

open lean source

IndisputableMonolith.Physics.PMNSCorrections on GitHub at line 69.

browse module

All declarations in this module, on Recognition.

explainer page

Tracked in the explainer inventory; generation is lazy so crawlers do not trigger LLM jobs.

open explainer

depends on

used by

formal source

  66def cube_edges_count (D : ℕ) : ℕ := D * 2^(D-1)
  67
  68/-- Number of faces in a D-cube: F = D(D-1) · 2^(D-2) for D ≥ 2 -/
  69def cube_faces (D : ℕ) : ℕ :=
  70  match D with
  71  | 0 => 0
  72  | 1 => 0
  73  | 2 => 4  -- square has 4 edges (faces in 2D)
  74  | 3 => 6  -- cube has 6 faces
  75  | n+4 => (n+4) * (n+3) * 2^(n+2)
  76
  77theorem cube3_vertices : cube_vertices 3 = 8 := by native_decide
  78theorem cube3_edges : cube_edges_count 3 = 12 := by native_decide
  79theorem cube3_faces : cube_faces 3 = 6 := rfl
  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. -/
  89def atmospheric_coefficient : ℕ := cube_faces 3
  90
  91theorem atmospheric_coefficient_eq_6 : atmospheric_coefficient = 6 := rfl
  92
  93/-- The atmospheric radiative correction is 6α. -/
  94noncomputable def atmospheric_correction : ℝ := (atmospheric_coefficient : ℝ) * alpha
  95
  96theorem atmospheric_correction_eq : atmospheric_correction = 6 * alpha := by
  97  unfold atmospheric_correction atmospheric_coefficient
  98  rfl
  99

papers checked against this theorem

No papers in the current corpus map onto this theorem yet.