def definition def or abbrev

`EightTickFromDimension`

No prose has been written for this declaration yet. The Lean source and graph data below render without it.

formal statement (Lean)

 125def EightTickFromDimension (D : Dimension) : ℕ := 2^D

Definition body.

 126
 127/-- Derived ledger lower bound: every simplicial recognition loop has at least 8 ticks. -/

From the project-wide theorem graph. These declarations reference this one in their body.

eight_tick_forces_D3 in IndisputableMonolith.Foundation.DimensionForcing decl_use
physical_eight_tick in IndisputableMonolith.Foundation.DimensionForcing decl_use
RSCompatibleDimension in IndisputableMonolith.Foundation.DimensionForcing decl_use
spinor_eight_tick_forces_D3 in IndisputableMonolith.Foundation.DimensionForcing decl_use
why_D_equals_3 in IndisputableMonolith.Foundation.DimensionForcing decl_use

Lean names referenced from this declaration's body.