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)
162theorem circuit_capacity_bound {n : ℕ} (c : BooleanCircuit n) :
163 CircuitZCapacity c ≤ 2 * c.gate_count :=
proof body
Term-mode proof.
164 circuit_bond_count_le c
165
166/-- Corollary: a poly-size circuit has poly-bounded Z-capacity. -/
used by (2)
From the project-wide theorem graph. These declarations reference this one in their body.
depends on (6)
Lean names referenced from this declaration's body.
-
BooleanCircuit
in IndisputableMonolith.Complexity.CircuitLedger
decl_use
-
circuit_bond_count_le
in IndisputableMonolith.Complexity.CircuitLedger
decl_use
-
CircuitZCapacity
in IndisputableMonolith.Complexity.CircuitLedger
decl_use
-
has
in IndisputableMonolith.Engineering.AsteroidOreSpectroscopy
decl_use
-
Z
in IndisputableMonolith.Masses.Anchor
decl_use
-
Z
in IndisputableMonolith.Physics.AnchorPolicyCertified
decl_use