pith. machine review for the scientific record. sign in
structure definition def or abbrev

ShortcutGraph

show as:
view Lean formalization →

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)

 100structure ShortcutGraph where
 101  weight_AB : ℝ
 102  weight_AC : ℝ
 103  weight_AB_pos : 0 < weight_AB
 104  weight_AC_pos : 0 < weight_AC
 105
 106/-- With a shortcut A→C, C receives signal at tick 1 (via shortcut) with weight w_AC,
 107    simultaneously with B receiving signal at tick 1 with weight w_AB.
 108    If w_AC ≥ w_AB, C activates at least as strongly as B at tick 1. -/

used by (1)

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

depends on (7)

Lean names referenced from this declaration's body.