4.5. Robin-boundary audit🔗

Theorem4.5.1

uses 0used by 0✓L∃∀N

The former raw symbolic target is not a missing associativity proof. It is false for the current H-free backend model. The theorem converts the proposed equality to the equivalent backend expansion and applies a compiled all-one coefficient counterexample. This closes that search branch while leaving the paper-wide external oracle contracts visibly experimental.

Lean code for Theorem4.5.1●1 theorem

theoremdefined in QuantumBlockEncoding/RobinMatrix.lean

complete

theorem QuantumBlockEncoding.Examples.RobinHeat.oneTermRobinGamma3BoundaryUnitaryEntry_ne_backendFold_n3 :
  QuantumBlockEncoding.Examples.RobinHeat.oneTermRobinGamma3BoundaryProjectionSummationTarget_n3.signalUnitaryEntry ≠
    QuantumBlockEncoding.blockExtractionBranchContributionSum
      QuantumBlockEncoding.Examples.RobinHeat.oneTermRobinGamma3BoundaryBackendBranchContribution_n3

theorem QuantumBlockEncoding.Examples.RobinHeat.oneTermRobinGamma3BoundaryUnitaryEntry_ne_backendFold_n3 :
  QuantumBlockEncoding.Examples.RobinHeat.oneTermRobinGamma3BoundaryProjectionSummationTarget_n3.signalUnitaryEntry ≠
    QuantumBlockEncoding.blockExtractionBranchContributionSum
      QuantumBlockEncoding.Examples.RobinHeat.oneTermRobinGamma3BoundaryBackendBranchContribution_n3

The historical H-free raw fold is false for the current symbolic target.

This closes the old diagnostic route by rejection rather than by an axiom.  It
combines the compiled equivalence to the backend-expansion statement with the
explicit all-one counterexample above.  The source-prepared route remains a
separate conditional interface and is never allowed to reuse this rejected
parent.

Theorem4.5.2

uses 0used by 0✓L∃∀N

The seven active matrices are listed in exactly the circuit order used by the finite semantics. Because symbolic coefficients retain expression-tree parentheses, algebraic regrouping belongs after evaluation and is not asserted as raw constructor equality.

Lean code for Theorem4.5.2●1 theorem

theoremdefined in QuantumBlockEncoding/RobinMatrix.lean

complete

theorem QuantumBlockEncoding.Examples.RobinHeat.oneTermRobinGamma3BoundaryGateMatrixList_n3 :
  List.map (fun gateMatrix => gateMatrix.matrix)
      (QuantumBlockEncoding.GHL2025.oneTermRobinGateMatrixPlaceholders
        (QuantumBlockEncoding.Examples.RobinHeat.oneTermParameters 3)) =
    [QuantumBlockEncoding.GHL2025.indicatorOracleMatrix
        (QuantumBlockEncoding.Examples.RobinHeat.oneTermParameters 3),
      QuantumBlockEncoding.GHL2025.sparseAmplitudeOracleDTRotationMatrix
        (QuantumBlockEncoding.Examples.RobinHeat.oneTermParameters 3),
      QuantumBlockEncoding.GHL2025.boundaryRotationMatrix
        (QuantumBlockEncoding.Examples.RobinHeat.oneTermParameters 3),
      QuantumBlockEncoding.GHL2025.bandedSparseAccessPaperMatrix
        (QuantumBlockEncoding.Examples.RobinHeat.oneTermParameters 3),
      QuantumBlockEncoding.GHL2025.functionOraclePaperMatrix
        (QuantumBlockEncoding.Examples.RobinHeat.oneTermParameters 3),
      QuantumBlockEncoding.GHL2025.swapOracleMatrix
        (QuantumBlockEncoding.Examples.RobinHeat.oneTermParameters 3),
      QuantumBlockEncoding.GHL2025.bandedSparseAccessPaperDaggerMatrix
        (QuantumBlockEncoding.Examples.RobinHeat.oneTermParameters 3)]

theorem QuantumBlockEncoding.Examples.RobinHeat.oneTermRobinGamma3BoundaryGateMatrixList_n3 :
  List.map
      (fun gateMatrix =>
        gateMatrix.matrix)
      (QuantumBlockEncoding.GHL2025.oneTermRobinGateMatrixPlaceholders
        (QuantumBlockEncoding.Examples.RobinHeat.oneTermParameters
          3)) =
    [QuantumBlockEncoding.GHL2025.indicatorOracleMatrix
        (QuantumBlockEncoding.Examples.RobinHeat.oneTermParameters
          3),
      QuantumBlockEncoding.GHL2025.sparseAmplitudeOracleDTRotationMatrix
        (QuantumBlockEncoding.Examples.RobinHeat.oneTermParameters
          3),
      QuantumBlockEncoding.GHL2025.boundaryRotationMatrix
        (QuantumBlockEncoding.Examples.RobinHeat.oneTermParameters
          3),
      QuantumBlockEncoding.GHL2025.bandedSparseAccessPaperMatrix
        (QuantumBlockEncoding.Examples.RobinHeat.oneTermParameters
          3),
      QuantumBlockEncoding.GHL2025.functionOraclePaperMatrix
        (QuantumBlockEncoding.Examples.RobinHeat.oneTermParameters
          3),
      QuantumBlockEncoding.GHL2025.swapOracleMatrix
        (QuantumBlockEncoding.Examples.RobinHeat.oneTermParameters
          3),
      QuantumBlockEncoding.GHL2025.bandedSparseAccessPaperDaggerMatrix
        (QuantumBlockEncoding.Examples.RobinHeat.oneTermParameters
          3)]

The seven active gate matrices have the exact paper-facing order recorded by
the circuit semantics layer.

The project-local symbolic `Coeff` matrix multiplication stores syntax trees,
so differently parenthesized products are not definitionally equal.  This
structural theorem is the correct raw certificate; algebraic regrouping must
be stated after `Coeff.evalWith`, where rational associativity is available.