OAI/MathematicalPhysics/ContinuumCoulomb/Quantum/QuantumEvenTapeOutputBounds.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

A uniform source promise for the literal even tape followed by the fixed final routing rounds, with a common numerical envelope for the spatial compiler.

  1. theorem OAI.ContinuumCoulomb.QuantumEvenTapeGeometry.output_polynomialPromise line 19