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)
140def eightTickCoherence : Structure → ℝ
141| .BCC => 1.0 -- Perfect 8-tick match
142| .FCC => 2/3 -- 8/12 = 2/3 match
143| .HCP => 2/3 -- Same as FCC
144
145/-- BCC has maximum 8-tick coherence. -/
used by (3)
From the project-wide theorem graph. These declarations reference this one in their body.
depends on (5)
Lean names referenced from this declaration's body.
-
Structure
in IndisputableMonolith.Chemistry.CrystalStructure
decl_use
-
tick
in IndisputableMonolith.Constants
decl_use
-
tick
in IndisputableMonolith.Constants.RSNativeUnits
decl_use
-
has
in IndisputableMonolith.Engineering.AsteroidOreSpectroscopy
decl_use
-
as
in IndisputableMonolith.Foundation.SimplicialLedger.ContinuumBridge
decl_use