ReservoirSchur

Abstract

ReservoirSchur supplies the width-three bridge max-flow proof.

Formulas retain the Lean parameter types and all hypotheses. HDiv.hDiv and HMod.hMod are displayed infix: on natural and integer carriers they mean the respective Lean integer division and remainder operations; on rational carriers division is field division. Coe.coe denotes the coercion determined by the displayed target type. Finite and dependent-pair constructors omit proof fields, which do not change their values. A dash in a match pattern is an anonymous wildcard. CoeFun.coe and CoeSort.coe retain coercions to functions and types. All dimensions use ℕ, all construction coefficients use ℚ, and max-flow uses ℂ.

Definition 1.1 (kernelEmbedding).

$$\forall (palphabetagammadelta:\mathbb{N})(w:Finalpha\times Findelta\to \mathbb{Q})(u:(({\Sigma }_{t:Sum(Finalpha)(Finbeta)}Fin(ShiftPencilBlocks.blockLengthpalphabetat+1)))\times ({\Sigma }_{t:Sum(Fingamma)(Findelta)}Fin(ShiftPencilBlocks.blockLengthpgammadeltat))),ReservoirSchur.kernelEmbeddingpalphabetagammadeltawu=(matchu.1,u.2with|⟨Sum.inli,s⟩,⟨Sum.inrh,j⟩\mapsto w(i,h)\cdot ShiftPencilBlocks.antiDiagonalp(s,j)|-,-\mapsto 0)$$

Formalization. D5/S3/Quantum/TensorNetworks/BridgeGraph/ReservoirSchur.kernelEmbedding (✓ std3).

Source. Repository-derived.

Commentary.

kernelEmbedding places one alternating anti-diagonal vector in each short-long block and is zero on the other blocks; kernel_coordinates shows that these vectors parametrize the entire same-depth width-two kernel.

Theorem 1.2 (kernelEmbedding_injective).

$$\forall (palphabetagammadelta:\mathbb{N}),Function.Injective(CoeFun.coe\left(ReservoirSchur.kernelEmbeddingpalphabetagammadelta\right))$$

Proof. Machine-checked in Lean as D5/S3/Quantum/TensorNetworks/BridgeGraph/ReservoirSchur.kernelEmbedding_injective (✓ std3). ∎

Source. Repository-derived.

Commentary.

The anti-diagonal kernel coordinates determine their embedded vector uniquely; kernelEmbedding_range combines this injectivity with the kernel dimension to identify the entire kernel.

Theorem 1.3 (kernel_coordinates).

$$\forall (palphabetagammadelta:\mathbb{N})(u:(({\Sigma }_{t:Sum(Finalpha)(Finbeta)}Fin(ShiftPencilBlocks.blockLengthpalphabetat+1)))\times ({\Sigma }_{t:Sum(Fingamma)(Findelta)}Fin(ShiftPencilBlocks.blockLengthpgammadeltat))\to \mathbb{Q}),(ShiftPencilBlocks.widthTwoMatrixppalphabetagammadelta).mulVecu=0\to \exists (w:Finalpha\times Findelta\to \mathbb{Q}),(ReservoirSchur.kernelEmbeddingpalphabetagammadelta)w=u$$

Proof. Machine-checked in Lean as D5/S3/Quantum/TensorNetworks/BridgeGraph/ReservoirSchur.kernel_coordinates (✓ std3). ∎

Source. Repository-derived.

Commentary.

Every vector annihilated by the same-depth widthTwoMatrix is an image of kernelEmbedding; LongReservoir.single_update_injective uses this parametrization to reduce the added-slice equation to the kernel coordinates.

Definition 1.4 (cokernelEmbedding).

$$\forall (palphabetagammadelta:\mathbb{N})(w:Finbeta\times Fingamma\to \mathbb{Q})(u:(({\Sigma }_{t:Sum(Finalpha)(Finbeta)}Fin(ShiftPencilBlocks.blockLengthpalphabetat)))\times ({\Sigma }_{t:Sum(Fingamma)(Findelta)}Fin(ShiftPencilBlocks.blockLengthpgammadeltat+1))),ReservoirSchur.cokernelEmbeddingpalphabetagammadeltawu=(matchu.1,u.2with|⟨Sum.inrk,s⟩,⟨Sum.inlj,t⟩\mapsto w(k,j)\cdot ShiftPencilBlocks.antiDiagonalp((s,t).2,(s,t).1)|-,-\mapsto 0)$$

Formalization. D5/S3/Quantum/TensorNetworks/BridgeGraph/ReservoirSchur.cokernelEmbedding (✓ std3).

Source. Repository-derived.

Commentary.

cokernelEmbedding places transposed alternating anti-diagonal vectors in the long-short output blocks; cokernelMatrix_mul_widthTwo shows that the associated coordinate projection annihilates the width-two matrix.

Theorem 1.5 (kernelMatrix_mulVec).

$$\forall (palphabetagammadelta:\mathbb{N})(w:Finalpha\times Findelta\to \mathbb{Q}),({LinearMap.toMatrix}^{\prime }(ReservoirSchur.kernelEmbeddingpalphabetagammadelta)).mulVecw=(ReservoirSchur.kernelEmbeddingpalphabetagammadelta)w$$

Proof. Machine-checked in Lean as D5/S3/Quantum/TensorNetworks/BridgeGraph/ReservoirSchur.kernelMatrix_mulVec (✓ std3). ∎

Source. Repository-derived.

Commentary.

Multiplying by the matrix of kernelEmbedding gives the embedded kernel vector; LongReservoir.single_update_injective uses this to apply the kernel sampling identity to its parametrized input.

Theorem 1.6 (cokernelMatrix_mul_widthTwo).

$$\forall (palphabetagammadelta:\mathbb{N}),({LinearMap.toMatrix}^{\prime }(ReservoirSchur.cokernelEmbeddingpalphabetagammadelta)).transpose\cdot ShiftPencilBlocks.widthTwoMatrixppalphabetagammadelta=0$$

Proof. Machine-checked in Lean as D5/S3/Quantum/TensorNetworks/BridgeGraph/ReservoirSchur.cokernelMatrix_mul_widthTwo (✓ std3). ∎

Source. Repository-derived.

Commentary.

The transpose of the matrix of cokernelEmbedding annihilates widthTwoMatrix; short_reservoir_injective uses this projection to remove the original width-two term from the augmented flow equation.

Definition 1.7 (kernelSample).

$$\forall (palphabetagammadelta:\mathbb{N})(t:Finalpha\times Findelta),ReservoirSchur.kernelSamplepalphabetagammadeltat=((⟨Sum.inlt.1,⟨0⟩⟩,⟨Sum.inrt.2,⟨p⟩⟩))$$

Formalization. D5/S3/Quantum/TensorNetworks/BridgeGraph/ReservoirSchur.kernelSample (✓ std3).

Source. Repository-derived.

Commentary.

kernelSample chooses coordinates zero and p in each short-long input block; kernel_sample_identity shows that sampling at these positions recovers the kernel coefficients.

Definition 1.8 (cokernelSample).

$$\forall (palphabetagammadelta:\mathbb{N})(t:Finbeta\times Fingamma),ReservoirSchur.cokernelSamplepalphabetagammadeltat=((⟨Sum.inrt.1,⟨p⟩⟩,⟨Sum.inlt.2,⟨0⟩⟩))$$

Formalization. D5/S3/Quantum/TensorNetworks/BridgeGraph/ReservoirSchur.cokernelSample (✓ std3).

Source. Repository-derived.

Commentary.

cokernelSample chooses coordinates p and zero in each long-short output block; cokernel_sample_identity shows that insertion at these positions is a right inverse of the cokernel projection.

Theorem 1.9 (kernel_sample_identity).

$$\forall (palphabetagammadelta:\mathbb{N}),(CyclicResolvent.inclusion(ReservoirSchur.kernelSamplepalphabetagammadelta)).transpose\cdot {LinearMap.toMatrix}^{\prime }(ReservoirSchur.kernelEmbeddingpalphabetagammadelta)=1$$

Proof. Machine-checked in Lean as D5/S3/Quantum/TensorNetworks/BridgeGraph/ReservoirSchur.kernel_sample_identity (✓ std3). ∎

Source. Repository-derived.

Commentary.

Sampling an embedded anti-diagonal kernel vector returns its coefficient vector; LongReservoir.single_update_injective uses this identity to reduce the added slice to a map on the kernel coefficients.

Theorem 1.10 (cokernel_sample_identity).

$$\forall (palphabetagammadelta:\mathbb{N}),({LinearMap.toMatrix}^{\prime }(ReservoirSchur.cokernelEmbeddingpalphabetagammadelta)).transpose\cdot CyclicResolvent.inclusion(ReservoirSchur.cokernelSamplepalphabetagammadelta)=1$$

Proof. Machine-checked in Lean as D5/S3/Quantum/TensorNetworks/BridgeGraph/ReservoirSchur.cokernel_sample_identity (✓ std3). ∎

Source. Repository-derived.

Commentary.

Inserting a vector at the cokernel sample positions and then applying the cokernel projection returns that vector; LongReservoir.single_update_injective uses this to read the added slice in cokernel coordinates.

Definition 1.11 (singleCross).

$$\forall (palphabetagammadelta:\mathbb{N})(BM:Matrix(Finbeta)(Finalpha)\mathbb{Q})(DM:Matrix(Fingamma)(Findelta)\mathbb{Q}),ReservoirSchur.singleCrosspalphabetagammadeltaBMDM=(CyclicResolvent.inclusion(ReservoirSchur.cokernelSamplepalphabetagammadelta)\cdot BM.kroneckerDM\cdot (CyclicResolvent.inclusion(ReservoirSchur.kernelSamplepalphabetagammadelta)).transpose)$$

Formalization. D5/S3/Quantum/TensorNetworks/BridgeGraph/ReservoirSchur.singleCross (✓ std3).

Source. Repository-derived.

Commentary.

singleCross inserts the Kronecker map BM⊗DM between the kernel sample positions and the cokernel sample positions; LongReservoir.single_update_injective uses this map to remove the width-two kernel.

Theorem 1.12 (inclusion_prod).

$$\forall \{m:Type\}\{n:Type\}\{r:Type\}\{s:Type\}[DecidableEqm][DecidableEqr](e:n\to m)(f:s\to r),(CyclicResolvent.inclusionfun(k:n\times s)\mapsto (ek.1,fk.2))=(CyclicResolvent.inclusione).kronecker(CyclicResolvent.inclusionf)$$

Proof. Machine-checked in Lean as D5/S3/Quantum/TensorNetworks/BridgeGraph/ReservoirSchur.inclusion_prod (✓ std3). ∎

Source. Repository-derived.

Commentary.

Coordinate insertion along a product of two maps is the Kronecker product of their insertion matrices; singleCross_kronecker uses this factorization to express the added matrix as one tensor slice.

Definition 1.13 (shortZeroCol).

$$\forall (palphabeta:\mathbb{N})(i:Finalpha),ReservoirSchur.shortZeroColpalphabetai=(⟨Sum.inli,⟨0⟩⟩)$$

Formalization. D5/S3/Quantum/TensorNetworks/BridgeGraph/ReservoirSchur.shortZeroCol (✓ std3).

Source. Repository-derived.

Commentary.

shortZeroCol selects column zero in each short block; singleThirdLeft uses these columns to read the kernel sample coordinates.

Definition 1.14 (longLastRow).

$$\forall (palphabeta:\mathbb{N})(k:Finbeta),ReservoirSchur.longLastRowpalphabetak=(⟨Sum.inrk,⟨p⟩⟩)$$

Formalization. D5/S3/Quantum/TensorNetworks/BridgeGraph/ReservoirSchur.longLastRow (✓ std3).

Source. Repository-derived.

Commentary.

longLastRow selects row p in each long block; singleThirdLeft uses these rows to insert the transformed coefficients into the cokernel sample positions.

Definition 1.15 (singleThirdLeft).

$$\forall (palphabeta:\mathbb{N})(BM:Matrix(Finbeta)(Finalpha)\mathbb{Q}),ReservoirSchur.singleThirdLeftpalphabetaBM=(CyclicResolvent.inclusion(ReservoirSchur.longLastRowpalphabeta)\cdot BM\cdot (CyclicResolvent.inclusion(ReservoirSchur.shortZeroColpalphabeta)).transpose)$$

Formalization. D5/S3/Quantum/TensorNetworks/BridgeGraph/ReservoirSchur.singleThirdLeft (✓ std3).

Source. Repository-derived.

Commentary.

singleThirdLeft applies BM from the zero columns of the short blocks to the final rows of the long blocks; singleCross_kronecker uses it as the left factor of the third tensor slice.

Definition 1.16 (singleThirdRight).

$$\forall (pgammadelta:\mathbb{N})(DM:Matrix(Fingamma)(Findelta)\mathbb{Q}),ReservoirSchur.singleThirdRightpgammadeltaDM=(CyclicResolvent.inclusion(ReservoirSchur.shortZeroColpgammadelta)\cdot DM\cdot (CyclicResolvent.inclusion(ReservoirSchur.longLastRowpgammadelta)).transpose)$$

Formalization. D5/S3/Quantum/TensorNetworks/BridgeGraph/ReservoirSchur.singleThirdRight (✓ std3).

Source. Repository-derived.

Commentary.

singleThirdRight applies DM from the final rows of the long blocks to the zero columns of the short blocks in the second factor; singleCross_kronecker uses it as the right factor of the third tensor slice.

Theorem 1.17 (singleCross_kronecker).

$$\forall (palphabetagammadelta:\mathbb{N})(BM:Matrix(Finbeta)(Finalpha)\mathbb{Q})(DM:Matrix(Fingamma)(Findelta)\mathbb{Q}),ReservoirSchur.singleCrosspalphabetagammadeltaBMDM=(ReservoirSchur.singleThirdLeftpalphabetaBM).kronecker(ReservoirSchur.singleThirdRightpgammadeltaDM)$$

Proof. Machine-checked in Lean as D5/S3/Quantum/TensorNetworks/BridgeGraph/ReservoirSchur.singleCross_kronecker (✓ std3). ∎

Source. Repository-derived.

Commentary.

The update singleCross is the Kronecker product of singleThirdLeft and singleThirdRight; LongReservoir.single_reversal_injective_witness uses this equality to realize the kernel-removing update as a third bond slice.

Definition 1.18 (localSource).

$$\forall (pqalphabetagammadelta:\mathbb{N})(u:(({\Sigma }_{t:Sum(Finalpha)(Finbeta)}Fin(ShiftPencilBlocks.blockLengthpalphabetat+1)))\times ({\Sigma }_{t:Sum(Fingamma)(Findelta)}Fin(ShiftPencilBlocks.blockLengthqgammadeltat))\to \mathbb{Q})(i:Sum(Finalpha)(Finbeta))(j:Sum(Fingamma)(Findelta))(k:Fin(ShiftPencilBlocks.blockLengthpalphabetai+1)\times Fin(ShiftPencilBlocks.blockLengthqgammadeltaj)),ReservoirSchur.localSourcepqalphabetagammadeltauijk=(u(⟨i,k.1⟩,⟨j,k.2⟩))$$

Formalization. D5/S3/Quantum/TensorNetworks/BridgeGraph/ReservoirSchur.localSource (✓ std3).

Source. Repository-derived.

Commentary.

localSource restricts the input vector to one pair of shift blocks; widthTwo_mulVec_block uses this restriction to express each block equation as a rectangular pencil equation.

Theorem 1.19 (widthTwo_mulVec_block).

$$\forall (pqalphabetagammadelta:\mathbb{N})(u:(({\Sigma }_{t:Sum(Finalpha)(Finbeta)}Fin(ShiftPencilBlocks.blockLengthpalphabetat+1)))\times ({\Sigma }_{t:Sum(Fingamma)(Findelta)}Fin(ShiftPencilBlocks.blockLengthqgammadeltat))\to \mathbb{Q})(i:Sum(Finalpha)(Finbeta))(j:Sum(Fingamma)(Findelta))(s:Fin(ShiftPencilBlocks.blockLengthpalphabetai))(t:Fin(ShiftPencilBlocks.blockLengthqgammadeltaj+1)),(ShiftPencilBlocks.widthTwoMatrixpqalphabetagammadelta).mulVecu(⟨i,s⟩,⟨j,t⟩)=(ShiftPencilBlocks.pencil(ShiftPencilBlocks.blockLengthpalphabetai)(ShiftPencilBlocks.blockLengthqgammadeltaj)).mulVec(ReservoirSchur.localSourcepqalphabetagammadeltauij)(s,t)$$

Proof. Machine-checked in Lean as D5/S3/Quantum/TensorNetworks/BridgeGraph/ReservoirSchur.widthTwo_mulVec_block (✓ std3). ∎

Source. Repository-derived.

Commentary.

On any pair of blocks, multiplication by widthTwoMatrix equals pencil multiplication on localSource; sourceSL_kernel_of_updated_zero uses this to isolate the short-long kernel equations.

Definition 1.20 (sourceSL).

$$\forall (palphabetagammadelta:\mathbb{N})(u:(({\Sigma }_{t:Sum(Finalpha)(Finbeta)}Fin(ShiftPencilBlocks.blockLengthpalphabetat+1)))\times ({\Sigma }_{t:Sum(Fingamma)(Findelta)}Fin(ShiftPencilBlocks.blockLengthpgammadeltat))\to \mathbb{Q})(k:(({\Sigma }_{t:Sum(Finalpha)(Finbeta)}Fin(ShiftPencilBlocks.blockLengthpalphabetat+1)))\times ({\Sigma }_{t:Sum(Fingamma)(Findelta)}Fin(ShiftPencilBlocks.blockLengthpgammadeltat))),ReservoirSchur.sourceSLpalphabetagammadeltauk=(matchk.1.fst,k.2.fstwith|Sum.inl-,Sum.inr-\mapsto uk|-,-\mapsto 0)$$

Formalization. D5/S3/Quantum/TensorNetworks/BridgeGraph/ReservoirSchur.sourceSL (✓ std3).

Source. Repository-derived.

Commentary.

sourceSL keeps the short-long input blocks and sets all other blocks to zero; sourceSL_kernelEmbedding shows that this projection fixes every vector in the parametrized kernel.

Definition 1.21 (slLine).

$$\forall (palphabetagammadelta:\mathbb{N})(u:(({\Sigma }_{t:Sum(Finalpha)(Finbeta)}Fin(ShiftPencilBlocks.blockLengthpalphabetat+1)))\times ({\Sigma }_{t:Sum(Fingamma)(Findelta)}Fin(ShiftPencilBlocks.blockLengthpgammadeltat))\to \mathbb{Q})(rt:Fin(p+1))(k:Finalpha\times Findelta),ReservoirSchur.slLinepalphabetagammadeltaurtk=(u(⟨Sum.inlk.1,⟨p-(\mathrm{val}\left(r\right))⟩⟩,⟨Sum.inrk.2,⟨p-(\mathrm{val}\left(t\right))⟩⟩))$$

Formalization. D5/S3/Quantum/TensorNetworks/BridgeGraph/ReservoirSchur.slLine (✓ std3).

Source. Repository-derived.

Commentary.

slLine reads the short-long input blocks at the coordinate pair (p-r,p-t); slLine_kernelEmbedding computes this array for an embedded anti-diagonal vector.

Theorem 1.22 (cokernel_mulVec_formula).

$$\forall (palphabetagammadelta:\mathbb{N})(z:(({\Sigma }_{t:Sum(Finalpha)(Finbeta)}Fin(ShiftPencilBlocks.blockLengthpalphabetat)))\times ({\Sigma }_{t:Sum(Fingamma)(Findelta)}Fin(ShiftPencilBlocks.blockLengthpgammadeltat+1))\to \mathbb{Q})(k:Finbeta)(j:Fingamma),({LinearMap.toMatrix}^{\prime }(ReservoirSchur.cokernelEmbeddingpalphabetagammadelta)).transpose.mulVecz(k,j)=\sum _{t:Fin(p+1)}((-1{)}^{\mathrm{val}\left(t\right)}\cdot z(⟨Sum.inrk,⟨p-(\mathrm{val}\left(t\right))⟩⟩,⟨Sum.inlj,t⟩))$$

Proof. Machine-checked in Lean as D5/S3/Quantum/TensorNetworks/BridgeGraph/ReservoirSchur.cokernel_mulVec_formula (✓ std3). ∎

Source. Repository-derived.

Commentary.

The cokernel projection is the displayed alternating sum along each long-short anti-diagonal; cokernel_reservoir_kernel uses this formula to compute the reservoir contribution in cokernel coordinates.

Theorem 1.23 (slLine_kernelEmbedding).

$$\forall (palphabetagammadelta:\mathbb{N})(w:Finalpha\times Findelta\to \mathbb{Q})(rt:Fin(p+1)),ReservoirSchur.slLinepalphabetagammadelta((ReservoirSchur.kernelEmbeddingpalphabetagammadelta)w)rt=if(\mathrm{val}\left(r\right))+(\mathrm{val}\left(t\right))=pthen(-1{)}^{p-(\mathrm{val}\left(r\right))}\cdot welse0$$

Proof. Machine-checked in Lean as D5/S3/Quantum/TensorNetworks/BridgeGraph/ReservoirSchur.slLine_kernelEmbedding (✓ std3). ∎

Source. Repository-derived.

Commentary.

For an embedded kernel vector, slLine vanishes unless r+t=p and otherwise equals the coefficient vector multiplied by the displayed sign; cokernel_reservoir_kernel uses this to compute the projected added slice.

Theorem 1.24 (sourceSL_kernelEmbedding).

$$\forall (palphabetagammadelta:\mathbb{N})(w:Finalpha\times Findelta\to \mathbb{Q}),ReservoirSchur.sourceSLpalphabetagammadelta((ReservoirSchur.kernelEmbeddingpalphabetagammadelta)w)=(ReservoirSchur.kernelEmbeddingpalphabetagammadelta)w$$

Proof. Machine-checked in Lean as D5/S3/Quantum/TensorNetworks/BridgeGraph/ReservoirSchur.sourceSL_kernelEmbedding (✓ std3). ∎

Source. Repository-derived.

Commentary.

The short-long block projection fixes every image of kernelEmbedding; short_reservoir_injective uses this identity to recover the full kernel vector from the vanishing short-long component.

Theorem 1.25 (short_short_witness).

$$\forall (palphabetagammadelta:\mathbb{N}),0<p\to 0<beta\to beta\le alpha\to 0<delta\to delta\le gamma\to QuantumMaxFlowBound.RationalWitness(ShiftPencilBlocks.leftDimpalphabeta)(ShiftPencilBlocks.rightDimpalphabeta)(ShiftPencilBlocks.leftDimpgammadelta)(ShiftPencilBlocks.rightDimpgammadelta)$$

Proof. Machine-checked in Lean as D5/S3/Quantum/TensorNetworks/BridgeGraph/ReservoirSchur.short_short_witness (✓ std3). ∎

Source. Repository-derived.

Commentary.

For p > 0, 0 < beta ≤ alpha and 0 < delta ≤ gamma, the short reservoir construction yields rational three-slice matrices attaining the outer cut by eliminating the kernel through its Schur complement. LongReservoir.parameterized_base_witness applies this in the equal-depth case with these multiplicity orderings.

References

• Truth anchor: D5/S3/Quantum/TensorNetworks/BridgeGraph/ReservoirSchur.cokernelEmbedding
• Truth anchor: D5/S3/Quantum/TensorNetworks/BridgeGraph/ReservoirSchur.cokernelMatrix_mul_widthTwo
• Truth anchor: D5/S3/Quantum/TensorNetworks/BridgeGraph/ReservoirSchur.cokernelSample
• Truth anchor: D5/S3/Quantum/TensorNetworks/BridgeGraph/ReservoirSchur.cokernel_mulVec_formula
• Truth anchor: D5/S3/Quantum/TensorNetworks/BridgeGraph/ReservoirSchur.cokernel_sample_identity
• Truth anchor: D5/S3/Quantum/TensorNetworks/BridgeGraph/ReservoirSchur.inclusion_prod
• Truth anchor: D5/S3/Quantum/TensorNetworks/BridgeGraph/ReservoirSchur.kernelEmbedding
• Truth anchor: D5/S3/Quantum/TensorNetworks/BridgeGraph/ReservoirSchur.kernelEmbedding_injective
• Truth anchor: D5/S3/Quantum/TensorNetworks/BridgeGraph/ReservoirSchur.kernelMatrix_mulVec
• Truth anchor: D5/S3/Quantum/TensorNetworks/BridgeGraph/ReservoirSchur.kernelSample
• Truth anchor: D5/S3/Quantum/TensorNetworks/BridgeGraph/ReservoirSchur.kernel_coordinates
• Truth anchor: D5/S3/Quantum/TensorNetworks/BridgeGraph/ReservoirSchur.kernel_sample_identity
• Truth anchor: D5/S3/Quantum/TensorNetworks/BridgeGraph/ReservoirSchur.localSource
• Truth anchor: D5/S3/Quantum/TensorNetworks/BridgeGraph/ReservoirSchur.longLastRow
• Truth anchor: D5/S3/Quantum/TensorNetworks/BridgeGraph/ReservoirSchur.shortZeroCol
• Truth anchor: D5/S3/Quantum/TensorNetworks/BridgeGraph/ReservoirSchur.short_short_witness
• Truth anchor: D5/S3/Quantum/TensorNetworks/BridgeGraph/ReservoirSchur.singleCross
• Truth anchor: D5/S3/Quantum/TensorNetworks/BridgeGraph/ReservoirSchur.singleCross_kronecker
• Truth anchor: D5/S3/Quantum/TensorNetworks/BridgeGraph/ReservoirSchur.singleThirdLeft
• Truth anchor: D5/S3/Quantum/TensorNetworks/BridgeGraph/ReservoirSchur.singleThirdRight
• Truth anchor: D5/S3/Quantum/TensorNetworks/BridgeGraph/ReservoirSchur.slLine
• Truth anchor: D5/S3/Quantum/TensorNetworks/BridgeGraph/ReservoirSchur.slLine_kernelEmbedding
• Truth anchor: D5/S3/Quantum/TensorNetworks/BridgeGraph/ReservoirSchur.sourceSL
• Truth anchor: D5/S3/Quantum/TensorNetworks/BridgeGraph/ReservoirSchur.sourceSL_kernelEmbedding
• Truth anchor: D5/S3/Quantum/TensorNetworks/BridgeGraph/ReservoirSchur.widthTwo_mulVec_block
• Dependency: D5/S3/Quantum/TensorNetworks/BridgeGraph/ShiftPencilBlocks