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

RCLDerivation

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)

  58structure RCLDerivation where
  59  step1_universal_cost : Prop
  60  step2_dalembert : Prop
  61  step3_unique_J : Prop
  62  step4_forces_RS : Prop
  63  chain_complete : step1_universal_cost → step2_dalembert →
  64    step3_unique_J → step4_forces_RS → True
  65

used by (2)

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