module module

`IndisputableMonolith.Foundation.CausalPropagationOrdering`

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

depends on (2)

Lean names referenced from this declaration's body.

IndisputableMonolith.Constants module_import
IndisputableMonolith.Foundation.RHatFixedPoint module_import

declarations in this module (15)

def blend_step L48
def chain_activation L54
theorem hop_ordering_preserved L61
theorem distance_2_zero_at_tick_1 L72
theorem activation_at_tick_2 L78
theorem general_hop_ordering L88
structure ShortcutGraph L100
theorem shortcut_simultaneous_activation L109
theorem bidirectional_destroys_ordering L118
def peak_activation L128
theorem peak_decreases L131
theorem practical_reach_bound L139
theorem phi_blend_5_hop_weak L149
theorem octave_sufficient_for_4_hop L163
theorem diagnostic_q1_q2 L189