ASPBE Lean Blueprint

6. Declaration catalog: Semantics🔗

This chapter is generated from the Lean source. Every node denotes one explicit public declaration, and every Lean link is checked during the Blueprint build. Definitions appear in source order before later results whenever the source module does so.

Reader orientation: Definitions and lemmas that connect circuit syntax to evaluated matrix semantics, finite state action, and explicit product-register projection. Each card separates an accessible reading cue from formal status, the source docstring, and the authoritative Lean panel. The standalone Library Explorer adds full-text search and filters across every chapter.

  1. 6.1. QuantumBlockEncoding/CircuitSemantics.lean
  2. 6.2. QuantumBlockEncoding/ConcreteSemantics.lean
  3. 6.3. QuantumBlockEncoding/ModularAdder3.lean
  4. 6.4. QuantumBlockEncoding/PrimitiveBasisLE.lean
  5. 6.5. QuantumBlockEncoding/PrimitiveCircuit.lean
  6. 6.6. QuantumBlockEncoding/PrimitiveMacros.lean
  7. 6.7. QuantumBlockEncoding/PrimitiveRefinement.lean
  8. 6.8. QuantumBlockEncoding/PrimitiveSemantics.lean
  9. 6.9. QuantumBlockEncoding/PromiseGateOptimization.lean
  10. 6.10. QuantumBlockEncoding/ReversibleClassical.lean
  11. 6.11. QuantumBlockEncoding/TeachingRouteClosures.lean
  12. 6.12. QuantumBlockEncoding/TextbookStatePreparation.lean
  13. 6.13. QuantumBlockEncoding/UniformlyControlledRy.lean