def definition def or abbrev

`the_proof_sketch`

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

formal statement (Lean)

 232def the_proof_sketch : AlgebraicRestrictionProofSketch where
 233  non_separability := trivial

Definition body.

 234  layer_propagation := trivial
 235  accumulation := trivial
 236
 237/-! ## Certificate -/
 238

Lean names referenced from this declaration's body.

AlgebraicRestrictionProofSketch in IndisputableMonolith.Complexity.CircuitLowerBound decl_use