`CellDim`

definition

show as: view math explainer →

module: IndisputableMonolith.Physics.LeptonGenerations.TauStepDeltaDerivation
domain: Physics
line: 295 · github
papers citing: none yet

open explainer

Read the cached plain-language explainer.

open lean source

IndisputableMonolith.Physics.LeptonGenerations.TauStepDeltaDerivation on GitHub at line 295.

browse module

All declarations in this module, on Recognition.

explainer page

A cached Ask Recognition explainer exists for this declaration.

open explainer

depends on

used by

formal source

 292/-! ### A tiny 3-cube cell model (enough to refute the E/8 counterexample) -/
 293
 294/-- The four cell dimensions in a 3-cube (0,1,2,3). -/
 295inductive CellDim where
 296  | vertex : CellDim
 297  | edge : CellDim
 298  | face : CellDim
 299  | cube : CellDim
 300deriving DecidableEq
 301
 302/-- Number of k-cells in the 3-cube. -/
 303def cellCount : CellDim → ℕ
 304  | .vertex => 8
 305  | .edge   => 12
 306  | .face   => 6
 307  | .cube   => 1
 308
 309/-- Number of vertices (0-cells) per k-cell (anchors per mediator). -/
 310def anchorsPerCell : CellDim → ℕ
 311  | .vertex => 1
 312  | .edge   => 2
 313  | .face   => 4
 314  | .cube   => 8
 315
 316/-- Local (cellwise) normalized coefficient: (number of mediators)/(anchors per mediator). -/
 317noncomputable def localCoeff (k : CellDim) : ℝ :=
 318  (cellCount k : ℝ) / (anchorsPerCell k : ℝ)
 319
 320theorem localCoeff_vertex : localCoeff .vertex = 8 := by
 321  unfold localCoeff cellCount anchorsPerCell
 322  norm_num
 323
 324theorem localCoeff_edge : localCoeff .edge = 6 := by
 325  unfold localCoeff cellCount anchorsPerCell

papers checked against this theorem

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