No prose has been written for this declaration yet. The Lean source and graph data below render
without it.
generate prose now
formal statement (Lean)
204theorem weak_polarizations_near_8 : totalWeakPolarizations = 9 := rfl
proof body
Term-mode proof.
205
206/-- 9 = 8 + 1 (8-tick plus one). -/
depends on (7)
Lean names referenced from this declaration's body.
-
tick
in IndisputableMonolith.Constants
decl_use
-
tick
in IndisputableMonolith.Constants.RSNativeUnits
decl_use
-
one
in IndisputableMonolith.Foundation.IntegersFromLogic
decl_use
-
one
in IndisputableMonolith.Foundation.RationalsFromLogic
decl_use
-
totalWeakPolarizations
in IndisputableMonolith.Physics.WeakForceEmergence
decl_use
-
one
in IndisputableMonolith.QFT.SpinStatistics
decl_use
-
one
in IndisputableMonolith.RecogSpec.Core
decl_use