ASPBE Lean Blueprint

10. Declaration catalog: PaperAndExamples🔗

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: Paper-facing backend models, source-specific Hermite constructions, and concrete State Preparation / Robin example artifacts. 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. 10.1. QuantumBlockEncoding/ConstructiveHermitePreparation.lean
  2. 10.2. QuantumBlockEncoding/Examples/RobinHeat.lean
  3. 10.3. QuantumBlockEncoding/GHL2025.lean
  4. 10.4. QuantumBlockEncoding/GHLHamiltonian.lean
  5. 10.5. QuantumBlockEncoding/HermiteBernstein.lean
  6. 10.6. QuantumBlockEncoding/HermiteBinaryCutoff.lean
  7. 10.7. QuantumBlockEncoding/HermiteBoundaryInjection.lean
  8. 10.8. QuantumBlockEncoding/HermiteCutRank.lean
  9. 10.9. QuantumBlockEncoding/HermiteExplicitBond.lean
  10. 10.10. QuantumBlockEncoding/HermiteFiniteChain.lean
  11. 10.11. QuantumBlockEncoding/HermiteFiniteNorm.lean
  12. 10.12. QuantumBlockEncoding/HermiteIntervalMass.lean
  13. 10.13. QuantumBlockEncoding/HermitePolynomial.lean
  14. 10.14. QuantumBlockEncoding/HermitePolynomialPreparation.lean
  15. 10.15. QuantumBlockEncoding/HermitePolynomialResources.lean
  16. 10.16. QuantumBlockEncoding/HermiteSampleStructure.lean
  17. 10.17. QuantumBlockEncoding/HermiteSmoothness.lean
  18. 10.18. QuantumBlockEncoding/HermiteStatePreparation.lean
  19. 10.19. QuantumBlockEncoding/HermiteTransferCores.lean
  20. 10.20. QuantumBlockEncoding/RealAmplitudePreparation.lean
  21. 10.21. QuantumBlockEncoding/Robin/ComplexLCU.lean
  22. 10.22. QuantumBlockEncoding/Robin/ComplexLCUProjection.lean
  23. 10.23. QuantumBlockEncoding/Robin/EvolvedCandidates.lean
  24. 10.24. QuantumBlockEncoding/Robin/Figure4Loaders.lean
  25. 10.25. QuantumBlockEncoding/Robin/Figure4MiddlePrimitive.lean
  26. 10.26. QuantumBlockEncoding/Robin/Figure4PreparePrimitive.lean
  27. 10.27. QuantumBlockEncoding/Robin/Figure4Primitive.lean
  28. 10.28. QuantumBlockEncoding/Robin/Figure4SourceData.lean
  29. 10.29. QuantumBlockEncoding/Robin/Figure4T3.lean
  30. 10.30. QuantumBlockEncoding/Robin/FixedN3Data.lean
  31. 10.31. QuantumBlockEncoding/Robin/Hadamard8BlockEncoding.lean
  32. 10.32. QuantumBlockEncoding/Robin/Hadamard8Verified.lean
  33. 10.33. QuantumBlockEncoding/Robin/PaperSevenAmplitudePrimitive.lean
  34. 10.34. QuantumBlockEncoding/Robin/PaperSevenLogicalUnitary.lean
  35. 10.35. QuantumBlockEncoding/Robin/PaperSevenPrepare.lean
  36. 10.36. QuantumBlockEncoding/Robin/PaperSevenPreparePrimitive.lean
  37. 10.37. QuantumBlockEncoding/Robin/PaperSevenPrimitive.lean
  38. 10.38. QuantumBlockEncoding/Robin/PaperSevenT3.lean
  39. 10.39. QuantumBlockEncoding/Robin/ResourceComparison.lean
  40. 10.40. QuantumBlockEncoding/Robin/SixSlotOptimal.lean
  41. 10.41. QuantumBlockEncoding/Robin/SourceBaseline.lean
  42. 10.42. QuantumBlockEncoding/Robin/SourceSevenSparseData.lean
  43. 10.43. QuantumBlockEncoding/Robin/SymmetryFourSlot.lean
  44. 10.44. QuantumBlockEncoding/Robin/SymmetryFourSlotBlockEncoding.lean
  45. 10.45. QuantumBlockEncoding/Robin/SymmetryFourSlotLogicalUnitary.lean
  46. 10.46. QuantumBlockEncoding/Robin/SymmetryFourSlotPrimitive.lean
  47. 10.47. QuantumBlockEncoding/Robin/SymmetryXorFourSlotLogicalUnitary.lean
  48. 10.48. QuantumBlockEncoding/Robin/SymmetryXorFourSlotPrimitive.lean
  49. 10.49. QuantumBlockEncoding/Robin/SystemConjugation.lean
  50. 10.50. QuantumBlockEncoding/Robin/T3ResourceComparison.lean
  51. 10.51. QuantumBlockEncoding/Robin/WeightedPermutation.lean
  52. 10.52. QuantumBlockEncoding/RobinEvolution.lean
  53. 10.53. QuantumBlockEncoding/StatePreparationBellRoute.lean
  54. 10.54. QuantumBlockEncoding/StatePreparationBenchmarksCoreFixed.lean
  55. 10.55. QuantumBlockEncoding/StatePreparationPaperEntryCertificates.lean
  56. 10.56. QuantumBlockEncoding/StatePreparationPaperRoutesCompact.lean
  57. 10.57. QuantumBlockEncoding/StatePreparationPrimitiveRoutes.lean
  58. 10.58. QuantumBlockEncoding/StoredBernstein.lean
  59. 10.59. QuantumBlockEncoding/StoredHermiteBoundaries.lean
  60. 10.60. QuantumBlockEncoding/StoredHermiteChildGeometry.lean
  61. 10.61. QuantumBlockEncoding/StoredHermiteCoefficients.lean
  62. 10.62. QuantumBlockEncoding/StoredHermiteGeometry.lean
  63. 10.63. QuantumBlockEncoding/StoredHermiteKernelTable.lean
  64. 10.64. QuantumBlockEncoding/StoredHermiteRawCost.lean
  65. 10.65. QuantumBlockEncoding/StoredHermiteRawSource.lean
  66. 10.66. QuantumBlockEncoding/StoredHermiteSharedTables.lean
  67. 10.67. QuantumBlockEncoding/StoredHermiteSourceCache.lean
  68. 10.68. QuantumBlockEncoding/StoredHermiteStageFields.lean
  69. 10.69. QuantumBlockEncoding/StoredHermiteStageInput.lean