`anchorsPerCell`

definition

show as: view math explainer →

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

open explainer

Read the cached plain-language explainer.

open lean source

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

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

 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
 334  norm_num
 335
 336/-! ### Uniqueness inside the admissible local mechanism class -/
 337
 338/-- Within the local (cellwise) mechanism class, **only** face-mediation yields 3/2 in the 3-cube. -/
 339theorem localCoeff_eq_three_halves_iff (k : CellDim) :
 340    localCoeff k = 3 / 2 ↔ k = .face := by

papers checked against this theorem

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