theorem
proved
localCoeff_cube
show as:
view math explainer →
open explainer
Read the cached plain-language explainer.
open lean source
IndisputableMonolith.Physics.LeptonGenerations.TauStepDeltaDerivation on GitHub at line 332.
browse module
All declarations in this module, on Recognition.
explainer page
depends on
used by
formal source
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
348 · intro h
349 cases h
350 | edge =>
351 constructor
352 · intro h
353 have : (6 : ℝ) = 3 / 2 := by
354 simpa [localCoeff, cellCount, anchorsPerCell] using h
355 norm_num at this
356 · intro h
357 cases h
358 | face =>
359 constructor
360 · intro _h
361 rfl
362 · intro _h