def definition def or abbrev

`syncPeriod`

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

formal statement (Lean)

  55def syncPeriod (D : ℕ) : ℕ := Nat.lcm (2 ^ D) 45

proof body

Definition body.

used by (24)

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

syncPeriod in IndisputableMonolith.Constants.RSNativeUnits decl_use
syncPeriod_eq_lcm in IndisputableMonolith.Constants.RSNativeUnits decl_use
ConstraintS_Cert in IndisputableMonolith.Gap45.SyncMinimization decl_use
constraint_S_minimization in IndisputableMonolith.Gap45.SyncMinimization decl_use
D3_unique_minimizer in IndisputableMonolith.Gap45.SyncMinimization decl_use
sync_3_lt_11 in IndisputableMonolith.Gap45.SyncMinimization decl_use
sync_3_lt_5 in IndisputableMonolith.Gap45.SyncMinimization decl_use
sync_3_lt_7 in IndisputableMonolith.Gap45.SyncMinimization decl_use
sync_3_lt_9 in IndisputableMonolith.Gap45.SyncMinimization decl_use
syncPeriod in IndisputableMonolith.Gap45.SyncMinimization decl_use
syncPeriod_11 in IndisputableMonolith.Gap45.SyncMinimization decl_use
syncPeriod_3 in IndisputableMonolith.Gap45.SyncMinimization decl_use
syncPeriod_5 in IndisputableMonolith.Gap45.SyncMinimization decl_use
syncPeriod_7 in IndisputableMonolith.Gap45.SyncMinimization decl_use
syncPeriod_9 in IndisputableMonolith.Gap45.SyncMinimization decl_use
sync_strictly_increasing_odd in IndisputableMonolith.Gap45.SyncMinimization decl_use
ConstraintS in IndisputableMonolith.Papers.DraftV1 decl_use
constraintS_forces_D3 in IndisputableMonolith.Papers.DraftV1 decl_use
kepler_selection_principle in IndisputableMonolith.Papers.DraftV1 decl_use
synchronization_selection_principle in IndisputableMonolith.Papers.DraftV1 decl_use
syncPeriod_3_eq_360 in IndisputableMonolith.Papers.DraftV1 decl_use
syncPeriod_def in IndisputableMonolith.Papers.DraftV1 decl_use
syncPeriod_eq_mul in IndisputableMonolith.Papers.DraftV1 decl_use
sync_resource_functional_minimized in IndisputableMonolith.Papers.DraftV1 decl_use

depends on (2)

Lean names referenced from this declaration's body.

syncPeriod in IndisputableMonolith.Constants.RSNativeUnits decl_use
syncPeriod in IndisputableMonolith.Gap45.SyncMinimization decl_use