OAI/MathematicalPhysics/ContinuumCoulomb/Quantum/QuantumSpatialFinalGeometry.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

The complete literal spatial routing output carries the exact physical square-lattice embedding, with a fixed multiple of the original box.

  1. theorem OAI.ContinuumCoulomb.QuantumFinalRoutingProgram.spatial_realization line 14