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

threeSubstrateCert

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)

  68def threeSubstrateCert : ThreeSubstrateCert where
  69  three_substrates := validationSubstrateCount

proof body

Definition body.

  70  fixed_point := shared_fixed_point
  71  descent := shared_descent
  72  symmetry := shared_symmetry
  73  lm_alignment := lm_fraction_eq
  74  photonic_rate := photonic_code_rate_rfl
  75  f2_cube_connection := seven_eighths_from_F2_cube
  76
  77end IndisputableMonolith.Foundation.ThreeSubstrateValidationCert

depends on (8)

Lean names referenced from this declaration's body.