`cellCount`

definition

show as: view math explainer →

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

open explainer

Read the cached plain-language explainer.

open lean source

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

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

 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
 326  norm_num
 327
 328theorem localCoeff_face : localCoeff .face = 3 / 2 := by
 329  unfold localCoeff cellCount anchorsPerCell
 330  norm_num
 331
 332theorem localCoeff_cube : localCoeff .cube = 1 / 8 := by
 333  unfold localCoeff cellCount anchorsPerCell

papers checked against this theorem

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