OAI/MathematicalPhysics/NavierStokes/ForcedComputation/Detector/ExpandingGateCount.lean

GitHub source file

3 declarations, 0 contain sorry, 0 declared as axioms

The complete instruction array has at most one gate per source address. This exponential bound will pay for summing all gate derivatives.

  1. theorem OAI.ForcedComputation.ExpandingDetector.stageWire_card_le line 12
  2. theorem OAI.ForcedComputation.ExpandingDetector.stageWire_card_growth line 26
  3. theorem OAI.ForcedComputation.ExpandingDetector.stageWire_card_growth_real line 37