4.4. Cubic diagonal operator🔗

Theorem4.4.1

uses 0used by 0✓L∃∀N

The linear diagonal input route simultaneously exposes rational orthogonality, the exact clean block, normalizer 1, and the named resource equality. This is the proved input expected by later polynomial or direct cubic routes.

Lean code for Theorem4.4.1●1 theorem

theoremdefined in QuantumBlockEncoding/CubicStatePreparation.lean

complete

theorem QuantumBlockEncoding.CubicDiagonalOracle.linearDiagonalHouseholderInputBEContract_complete
  (n : ℕ) :
  QuantumBlockEncoding.BlockEncodingClassics.IsRationalOrthogonal
      (QuantumBlockEncoding.CubicDiagonalOracle.linearDiagonalHouseholderInputBEContract
          n).U ∧
    (QuantumBlockEncoding.BlockEncodingClassics.cleanBlockBy
            (QuantumBlockEncoding.CubicDiagonalOracle.linearDiagonalHouseholderInputBEContract
                n).embed
            (QuantumBlockEncoding.CubicDiagonalOracle.linearDiagonalHouseholderInputBEContract
                n).U).PointwiseEq
        (QuantumBlockEncoding.CubicDiagonalOracle.linearDiagonalTarget
            n).operator ∧
      (QuantumBlockEncoding.CubicDiagonalOracle.linearDiagonalTarget
              n).normalizer =
          1 ∧
        (QuantumBlockEncoding.CubicDiagonalOracle.linearDiagonalHouseholderInputBEContract
              n).resource =
          QuantumBlockEncoding.Resource.ofCountsWithDepth 0 0 1 0 1

theorem QuantumBlockEncoding.CubicDiagonalOracle.linearDiagonalHouseholderInputBEContract_complete
  (n : ℕ) :
  QuantumBlockEncoding.BlockEncodingClassics.IsRationalOrthogonal
      (QuantumBlockEncoding.CubicDiagonalOracle.linearDiagonalHouseholderInputBEContract
          n).U ∧
    (QuantumBlockEncoding.BlockEncodingClassics.cleanBlockBy
            (QuantumBlockEncoding.CubicDiagonalOracle.linearDiagonalHouseholderInputBEContract
                n).embed
            (QuantumBlockEncoding.CubicDiagonalOracle.linearDiagonalHouseholderInputBEContract
                n).U).PointwiseEq
        (QuantumBlockEncoding.CubicDiagonalOracle.linearDiagonalTarget
            n).operator ∧
      (QuantumBlockEncoding.CubicDiagonalOracle.linearDiagonalTarget
              n).normalizer =
          1 ∧
        (QuantumBlockEncoding.CubicDiagonalOracle.linearDiagonalHouseholderInputBEContract
              n).resource =
          QuantumBlockEncoding.Resource.ofCountsWithDepth
            0 0 1 0 1

Root certificate for the hinted input operator `O_0`.  This theorem exposes
all matrix-level facts needed by a downstream polynomial consumer in one
place, so the harness does not reopen the four-square, Householder, cleanup,
normalizer, or resource leaves after they have compiled.

Theorem4.4.2

uses 0used by 1✓L∃∀N

For every grid index, four-square witnesses complete the cubic clean amplitude to a rational unit vector. The direct sum of the resulting Householder blocks is rational orthogonal and its selected block is the cubic diagonal operator.

Lean code for Theorem4.4.2●1 theorem

theoremdefined in QuantumBlockEncoding/CubicStatePreparation.lean

complete

theorem QuantumBlockEncoding.CubicDiagonalOracle.cubicDiagonalRationalCompletion_backendSupport
  (n : ℕ) :
  ∃ v,
    (QuantumBlockEncoding.BlockEncodingClassics.cleanBlockBy
            (QuantumBlockEncoding.CubicDiagonalOracle.controlledHouseholder8Embed
              n)
            (QuantumBlockEncoding.CubicDiagonalOracle.controlledHouseholder8DirectSum
              n v)).PointwiseEq
        (QuantumBlockEncoding.CubicDiagonalOracle.cubicDiagonalOperator
          n) ∧
      QuantumBlockEncoding.BlockEncodingClassics.IsRationalOrthogonal
        (QuantumBlockEncoding.CubicDiagonalOracle.controlledHouseholder8DirectSum
          n v)

theorem QuantumBlockEncoding.CubicDiagonalOracle.cubicDiagonalRationalCompletion_backendSupport
  (n : ℕ) :
  ∃ v,
    (QuantumBlockEncoding.BlockEncodingClassics.cleanBlockBy
            (QuantumBlockEncoding.CubicDiagonalOracle.controlledHouseholder8Embed
              n)
            (QuantumBlockEncoding.CubicDiagonalOracle.controlledHouseholder8DirectSum
              n v)).PointwiseEq
        (QuantumBlockEncoding.CubicDiagonalOracle.cubicDiagonalOperator
          n) ∧
      QuantumBlockEncoding.BlockEncodingClassics.IsRationalOrthogonal
        (QuantumBlockEncoding.CubicDiagonalOracle.controlledHouseholder8DirectSum
          n v)

Theorem4.4.3

uses 1used by 0✓L∃∀N

The root theorem combines the unitary predicate, exact clean-block target, normalizer, and resource identity. It closes the direct exact construction without treating a clean-block-only wrapper as a full operator certificate.

Lean code for Theorem4.4.3●1 theorem

theoremdefined in QuantumBlockEncoding/CubicStatePreparation.lean

complete

theorem QuantumBlockEncoding.CubicDiagonalOracle.cubicDiagonalHouseholderExactBEContract_complete
  (n : ℕ) :
  QuantumBlockEncoding.BlockEncodingClassics.IsRationalOrthogonal
      (QuantumBlockEncoding.CubicDiagonalOracle.cubicDiagonalHouseholderExactBEContract
            n).exactPayload.U ∧
    (QuantumBlockEncoding.CubicDiagonalOracle.cubicDiagonalHouseholderExactBEContract
                n).exactPayload.clean.PointwiseEq
        (QuantumBlockEncoding.CubicDiagonalOracle.cubicDiagonalTarget
            n).operator ∧
      (QuantumBlockEncoding.CubicDiagonalOracle.cubicDiagonalTarget
              n).normalizer =
          1 ∧
        (QuantumBlockEncoding.CubicDiagonalOracle.cubicDiagonalHouseholderExactBEContract
              n).resource =
          QuantumBlockEncoding.Resource.ofCountsWithDepth 0 0 1 0 1

theorem QuantumBlockEncoding.CubicDiagonalOracle.cubicDiagonalHouseholderExactBEContract_complete
  (n : ℕ) :
  QuantumBlockEncoding.BlockEncodingClassics.IsRationalOrthogonal
      (QuantumBlockEncoding.CubicDiagonalOracle.cubicDiagonalHouseholderExactBEContract
            n).exactPayload.U ∧
    (QuantumBlockEncoding.CubicDiagonalOracle.cubicDiagonalHouseholderExactBEContract
                n).exactPayload.clean.PointwiseEq
        (QuantumBlockEncoding.CubicDiagonalOracle.cubicDiagonalTarget
            n).operator ∧
      (QuantumBlockEncoding.CubicDiagonalOracle.cubicDiagonalTarget
              n).normalizer =
          1 ∧
        (QuantumBlockEncoding.CubicDiagonalOracle.cubicDiagonalHouseholderExactBEContract
              n).resource =
          QuantumBlockEncoding.Resource.ofCountsWithDepth
            0 0 1 0 1

Unconditional exact root certificate for the cubic diagonal operator.  The
conjunction deliberately includes the unitary predicate, clean-block target,
normalizer, and resource equality; a clean-block-only arithmetic wrapper is
not sufficient to close an operator block-encoding task.