`localCoeff`

definition

show as: view math explainer →

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

open explainer

Read the cached plain-language explainer.

open lean source

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

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

 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
 341  cases k with
 342  | vertex =>
 343      constructor
 344      · intro h
 345        have : (8 : ℝ) = 3 / 2 := by
 346          simpa [localCoeff, cellCount, anchorsPerCell] using h
 347        norm_num at this

papers checked against this theorem

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