ShiftPencilBlocks

Abstract

ShiftPencilBlocks 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 (ParameterizedBaseWitness).

$$ShiftPencilBlocks.ParameterizedBaseWitness⟺(\forall (pqalphabetagammadelta:\mathbb{N}),0<p\to 0<q\to 0<beta\to 0<delta\to QuantumMaxFlowBound.RationalWitness(p\cdot alpha+(p+1)\cdot beta)((p+1)\cdot alpha+(p+2)\cdot beta)(q\cdot gamma+(q+1)\cdot delta)((q+1)\cdot gamma+(q+2)\cdot delta))$$

Formalization. D5/S3/Quantum/TensorNetworks/BridgeGraph/ShiftPencilBlocks.ParameterizedBaseWitness (✓ std3).

Source. Repository-derived.

Commentary.

ParameterizedBaseWitness asserts rational full-rank flows for pairs whose dimensions are sums of short and long shift-block dimensions, with positive depths and positive long-block multiplicities; base_of_parameterized uses the decomposition of strict base pairs to recover BaseWitness.

Theorem 1.2 (base_of_parameterized).

$$ShiftPencilBlocks.ParameterizedBaseWitness\to QuantumMaxFlowBound.BaseWitness$$

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

Source. Repository-derived.

Commentary.

Every strict base dimension pair can be decomposed into short and long shift blocks, so full rank for the parameterized family implies BaseWitness; LongReservoir.base_witness applies this implication to its constructions.

Definition 1.3 (rectExtend).

$$\forall (xy:\mathbb{N})(z:Finx\times Finy\to \mathbb{Q})(ik:\mathbb{N}),ShiftPencilBlocks.rectExtendzik=(ifhi:i<xthenifhk:k<ythenz(⟨i,hi⟩,⟨k,hk⟩)else0else0)$$

Formalization. D5/S3/Quantum/TensorNetworks/BridgeGraph/ShiftPencilBlocks.rectExtend (✓ std3).

Source. Repository-derived.

Commentary.

rectExtend extends a finite rectangular array by zero to natural-number coordinates; pencil_mulVec uses it to express the pencil recurrence uniformly at the boundary.

Definition 1.4 (shift1).

$$\forall (x:\mathbb{N}),ShiftPencilBlocks.shift1x=(Matrix.submatrix1(fun(i:Finx)\mapsto (\mathrm{val}\left(i\right))+1)Fin.val)$$

Formalization. D5/S3/Quantum/TensorNetworks/BridgeGraph/ShiftPencilBlocks.shift1 (✓ std3).

Source. Repository-derived.

Commentary.

shift1 has entry one when the column index is one greater than the row index and zero elsewhere; pencil combines it with the rectangular identity to couple adjacent coordinates.

Definition 1.5 (pencil).

$$\forall (xy:\mathbb{N}),ShiftPencilBlocks.pencilxy=((QuantumMaxFlowBound.rectIdx(x+1)).kronecker(QuantumMaxFlowBound.rectIdy(y+1)).transpose+(ShiftPencilBlocks.shift1x).kronecker(ShiftPencilBlocks.shift1y).transpose)$$

Formalization. D5/S3/Quantum/TensorNetworks/BridgeGraph/ShiftPencilBlocks.pencil (✓ std3).

Source. Repository-derived.

Commentary.

pencil is the sum of the unshifted and shifted Kronecker terms, mapping (x+1)y input coordinates to x(y+1) output coordinates; pencil_rank_of_le proves full row rank when x ≤ y.

Theorem 1.6 (pencil_rank_of_le).

$$\forall (xy:\mathbb{N}),x\le y\to (ShiftPencilBlocks.pencilxy).rank=x\cdot (y+1)$$

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

Source. Repository-derived.

Commentary.

When x ≤ y, pencil has full row rank x*(y+1), because its transpose recurrence propagates to a zero boundary. widthTwo_rank_of_lt applies this blockwise to dimension pairs with increasing depths.

Theorem 1.7 (block_mulVec).

$$\forall \{\iota :Type\}[Fintype\iota ][DecidableEq\iota ]\{m:\iota \to Type\}\{n:\iota \to Type\}[(i:\iota )\to Fintype(mi)][(i:\iota )\to Fintype(ni)](A:(i:\iota )\to Matrix(mi)(ni)\mathbb{Q})(z:({\Sigma }_{i:\iota }ni)\to \mathbb{Q})(i:\iota )(j:mi),({Matrix.blockDiagonal}^{\prime }A).mulVecz⟨i,j⟩=(Ai).mulVec(fun(k:ni)\mapsto z⟨i,k⟩)j$$

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

Source. Repository-derived.

Commentary.

Multiplication by a block-diagonal matrix acts on each block using only the corresponding input coordinates; blockKernelEquiv uses this identity to identify its kernel with the product of the individual kernels.

Definition 1.8 (tensorBlockEquiv).

$$\forall (\iota :Type)(\kappa :Type)(m:\iota \to Type)(n:\kappa \to Type),ShiftPencilBlocks.tensorBlockEquivmn=((Equiv.sigmaProdDistribm({\Sigma }_{j:\kappa }nj)).trans((Equiv.sigmaCongrRightfun(i:\iota )\mapsto (Equiv.prodComm(mi)({\Sigma }_{j:\kappa }nj)).trans((Equiv.sigmaProdDistribn(mi)).trans(Equiv.sigmaCongrRightfun(j:\kappa )\mapsto Equiv.prodComm(nj)(mi)))).transEquiv.sigmaAssocProd.symm))$$

Formalization. D5/S3/Quantum/TensorNetworks/BridgeGraph/ShiftPencilBlocks.tensorBlockEquiv (✓ std3).

Source. Repository-derived.

Commentary.

tensorBlockEquiv groups a pair of dependent block indices into a single index for the pair of blocks; widthTwo_block_decomposition uses this reindexing to express the tensor matrix as a block-diagonal family of pencils.

Theorem 1.9 (pencil_mulVec).

$$\forall (xy:\mathbb{N})(u:Fin(x+1)\times Finy\to \mathbb{Q})(r:Finx\times Fin(y+1)),(ShiftPencilBlocks.pencilxy).mulVecur=ShiftPencilBlocks.rectExtendu(\mathrm{val}\left(r.1\right))(\mathrm{val}\left(r.2\right))+if0<(\mathrm{val}\left(r.2\right))thenShiftPencilBlocks.rectExtendu((\mathrm{val}\left(r.1\right))+1)((\mathrm{val}\left(r.2\right))-1)else0$$

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

Source. Repository-derived.

Commentary.

At each output position, pencil multiplication adds the current input coordinate and the adjacent shifted coordinate, with zero extension at the boundary; antiDiagonal_kernel uses this recurrence to cancel successive alternating signs.

Definition 1.10 (antiDiagonal).

$$\forall (p:\mathbb{N})(k:Fin(p+1)\times Fin(p+1)),ShiftPencilBlocks.antiDiagonalpk=(if(\mathrm{val}\left(k.1\right))+(\mathrm{val}\left(k.2\right))=pthen(-1{)}^{\mathrm{val}\left(k.1\right)}else0)$$

Formalization. D5/S3/Quantum/TensorNetworks/BridgeGraph/ShiftPencilBlocks.antiDiagonal (✓ std3).

Source. Repository-derived.

Commentary.

antiDiagonal is supported where the two coordinate indices sum to p and has alternating signs there; antiDiagonal_kernel shows that it lies in the kernel of the short-long pencil.

Theorem 1.11 (antiDiagonal_kernel).

$$\forall (p:\mathbb{N}),(ShiftPencilBlocks.pencilp(p+1)).mulVec(ShiftPencilBlocks.antiDiagonalp)=0$$

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

Source. Repository-derived.

Commentary.

The alternating anti-diagonal vector is annihilated by pencil p (p+1); ReservoirSchur.widthTwo_kernelEmbedding applies this in every short-long block to construct kernel vectors.

Definition 1.12 (blockLength).

$$\forall (palphabeta:\mathbb{N}),ShiftPencilBlocks.blockLengthpalphabeta=Sum.elim(fu{n}_{\mapsto }p)(fu{n}_{\mapsto }p+1)$$

Formalization. D5/S3/Quantum/TensorNetworks/BridgeGraph/ShiftPencilBlocks.blockLength (✓ std3).

Source. Repository-derived.

Commentary.

blockLength assigns length p to each of the alpha short blocks and p+1 to each of the beta long blocks; arrow0 and arrow1 use these lengths to form their block-diagonal matrices.

Definition 1.13 (leftDim).

$$\forall (palphabeta:\mathbb{N}),ShiftPencilBlocks.leftDimpalphabeta=(p\cdot alpha+(p+1)\cdot beta)$$

Formalization. D5/S3/Quantum/TensorNetworks/BridgeGraph/ShiftPencilBlocks.leftDim (✓ std3).

Source. Repository-derived.

Commentary.

leftDim is the total row dimension p*alpha+(p+1)*beta of the shift blocks; rows_card identifies it with the cardinality of the dependent row-index type.

Definition 1.14 (rightDim).

$$\forall (palphabeta:\mathbb{N}),ShiftPencilBlocks.rightDimpalphabeta=((p+1)\cdot alpha+(p+2)\cdot beta)$$

Formalization. D5/S3/Quantum/TensorNetworks/BridgeGraph/ShiftPencilBlocks.rightDim (✓ std3).

Source. Repository-derived.

Commentary.

rightDim is the total column dimension (p+1)*alpha+(p+2)*beta of the shift blocks; cols_card identifies it with the cardinality of the dependent column-index type.

Theorem 1.15 (rows_card).

$$\forall (palphabeta:\mathbb{N}),Fintype.card(({\Sigma }_{t:Sum(Finalpha)(Finbeta)}Fin(ShiftPencilBlocks.blockLengthpalphabetat)))=ShiftPencilBlocks.leftDimpalphabeta$$

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

Source. Repository-derived.

Commentary.

The dependent row-index type has cardinality leftDim; same_depth_kernel_dimension uses this count with the rank calculation to compute the kernel dimension.

Theorem 1.16 (cols_card).

$$\forall (palphabeta:\mathbb{N}),Fintype.card(({\Sigma }_{t:Sum(Finalpha)(Finbeta)}Fin(ShiftPencilBlocks.blockLengthpalphabetat+1)))=ShiftPencilBlocks.rightDimpalphabeta$$

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

Source. Repository-derived.

Commentary.

The dependent column-index type has cardinality rightDim; same_depth_kernel_dimension uses this count as the domain dimension in rank-nullity.

Definition 1.17 (arrow0).

$$\forall (palphabeta:\mathbb{N}),ShiftPencilBlocks.arrow0palphabeta=({Matrix.blockDiagonal}^{\prime }fun(t:Sum(Finalpha)(Finbeta))\mapsto QuantumMaxFlowBound.rectId(ShiftPencilBlocks.blockLengthpalphabetat)(ShiftPencilBlocks.blockLengthpalphabetat+1))$$

Formalization. D5/S3/Quantum/TensorNetworks/BridgeGraph/ShiftPencilBlocks.arrow0 (✓ std3).

Source. Repository-derived.

Commentary.

arrow0 is the block-diagonal sum of the rectangular identity maps for the short and long blocks; widthTwoMatrix pairs it with the transpose of the second dimension pair’s unshifted map.

Definition 1.18 (arrow1).

$$\forall (palphabeta:\mathbb{N}),ShiftPencilBlocks.arrow1palphabeta=({Matrix.blockDiagonal}^{\prime }fun(t:Sum(Finalpha)(Finbeta))\mapsto ShiftPencilBlocks.shift1(ShiftPencilBlocks.blockLengthpalphabetat))$$

Formalization. D5/S3/Quantum/TensorNetworks/BridgeGraph/ShiftPencilBlocks.arrow1 (✓ std3).

Source. Repository-derived.

Commentary.

arrow1 is the block-diagonal sum of the one-step shift maps for the short and long blocks; widthTwoMatrix pairs it with the transpose of the second dimension pair’s shifted map.

Definition 1.19 (widthTwoMatrix).

$$\forall (pqalphabetagammadelta:\mathbb{N}),ShiftPencilBlocks.widthTwoMatrixpqalphabetagammadelta=((ShiftPencilBlocks.arrow0palphabeta).kronecker(ShiftPencilBlocks.arrow0qgammadelta).transpose+(ShiftPencilBlocks.arrow1palphabeta).kronecker(ShiftPencilBlocks.arrow1qgammadelta).transpose)$$

Formalization. D5/S3/Quantum/TensorNetworks/BridgeGraph/ShiftPencilBlocks.widthTwoMatrix (✓ std3).

Source. Repository-derived.

Commentary.

widthTwoMatrix is the sum of the two Kronecker products formed from arrow0 and arrow1; widthTwo_block_decomposition splits it into rectangular pencils indexed by pairs of blocks.

Theorem 1.20 (widthTwo_block_decomposition).

$$\forall (pqalphabetagammadelta:\mathbb{N}),ShiftPencilBlocks.widthTwoMatrixpqalphabetagammadelta=({Matrix.blockDiagonal}^{\prime }fun(t:(Sum(Finalpha)(Finbeta))\times (Sum(Fingamma)(Findelta)))\mapsto ShiftPencilBlocks.pencil(ShiftPencilBlocks.blockLengthpalphabetat.1)(ShiftPencilBlocks.blockLengthqgammadeltat.2)).submatrix(CoeFun.coe\left(ShiftPencilBlocks.tensorBlockEquiv(fun(t:Sum(Finalpha)(Finbeta))\mapsto Fin(ShiftPencilBlocks.blockLengthpalphabetat))fun(t:Sum(Fingamma)(Findelta))\mapsto Fin(ShiftPencilBlocks.blockLengthqgammadeltat+1)\right))(CoeFun.coe\left(ShiftPencilBlocks.tensorBlockEquiv(fun(t:Sum(Finalpha)(Finbeta))\mapsto Fin(ShiftPencilBlocks.blockLengthpalphabetat+1))fun(t:Sum(Fingamma)(Findelta))\mapsto Fin(ShiftPencilBlocks.blockLengthqgammadeltat)\right))$$

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

Source. Repository-derived.

Commentary.

Reindexing the rows and columns identifies widthTwoMatrix with a block-diagonal family of rectangular pencils; widthTwo_rank_sum uses this decomposition to add their ranks.

Theorem 1.21 (witness_of_typed_slices).

$$\forall \{I:Type\}\{J:Type\}\{K:Type\}\{L:Type\}[FintypeI][FintypeJ][FintypeK][FintypeL]\{abcd:\mathbb{N}\},Fintype.cardI=a\to Fintype.cardJ=b\to Fintype.cardK=c\to Fintype.cardL=d\to \forall (M:Fin3\to MatrixIJ\mathbb{Q})(N:Fin3\to MatrixLK\mathbb{Q}),(\sum _{r:Fin3}((Mr).kronecker(Nr))).rank=min(a\cdot d)(b\cdot c)\to QuantumMaxFlowBound.RationalWitnessabcd$$

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

Source. Repository-derived.

Commentary.

A rational three-slice contraction attaining the smaller outer cut on arbitrary finite index types can be reindexed to Fin a, Fin b, Fin c and Fin d without changing rank; witness_of_widthTwo_rank applies this to the block-indexed construction.

Theorem 1.22 (different_depth_witness).

$$\forall (pqalphabetagammadelta:\mathbb{N}),p\ne q\to QuantumMaxFlowBound.RationalWitness(ShiftPencilBlocks.leftDimpalphabeta)(ShiftPencilBlocks.rightDimpalphabeta)(ShiftPencilBlocks.leftDimqgammadelta)(ShiftPencilBlocks.rightDimqgammadelta)$$

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

Source. Repository-derived.

Commentary.

When the two depths differ, the width-two pencil already gives rational matrices attaining min(ad,bc) for the parameterized dimensions; LongReservoir.parameterized_base_witness uses this for the unequal-depth case.

Theorem 1.23 (same_depth_kernel_dimension).

$$\forall (palphabetagammadelta:\mathbb{N}),Module.finrank\mathbb{Q}(CoeSort.coe\left((ShiftPencilBlocks.widthTwoMatrixppalphabetagammadelta).mulVecLin.ker\right))=alpha\cdot delta$$

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

Source. Repository-derived.

Commentary.

At equal depths, the kernel of widthTwoMatrix has dimension alpha*delta; ReservoirSchur.kernelEmbedding_range combines this count with its injective kernel parametrization to show that every kernel vector has those coordinates.

Theorem 1.24 (zero_defect_witness).

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

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

Source. Repository-derived.

Commentary.

At equal depths, if alphadelta or betagamma vanishes, the width-two matrix attains the smaller outer cut; LongReservoir.parameterized_base_witness uses this for the zero-defect cases.

Theorem 1.25 (double_fin_pick).

$$\forall (nmrs:\mathbb{N})(ab:\mathbb{Q})(u:Finn\times Finm\to \mathbb{Q}),\sum _{i:Finn}(\sum _{j:Finm}(((if(\mathrm{val}\left(i\right))=rthenaelse0)\cdot if(\mathrm{val}\left(j\right))=sthenbelse0)\cdot u(i,j)))=a\cdot b\cdot ShiftPencilBlocks.rectExtendurs$$

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

Source. Repository-derived.

Commentary.

A double finite sum supported at a single pair of indices equals the product of the two coefficients times the zero-extended array value; ReservoirSchur.reservoirCross_SL_short_row uses this to compute the added slice at a short-row position.

Theorem 1.26 (neg_one_pow_square).

$$\forall (n:\mathbb{N}),(-1{)}^n\cdot (-1{)}^n=1$$

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

Source. Repository-derived.

Commentary.

The square of every integer power of -1 is one; ReservoirSchur.cokernel_reservoir_kernel uses this identity to cancel the two anti-diagonal signs in the projected reservoir equation.

Theorem 1.27 (short_short_cyclic_schur_rank).

$$\forall (ABGDp:\mathbb{N}),0<B\to B\le A\to 0<D\to D\le G\to 0<p\to (((Coe.coe\left(p\right))+1)\cdot (FloorSelectorCycles.rowSelectorAB).kronecker(FloorSelectorCycles.rowSelectorGD).transpose-(FloorSelectorCycles.rowSelectorAB).kronecker(FloorSelectorCycles.forwardHalfG)\cdot (FloorSelectorCycles.reservoirAG{)}^{-1}\cdot (-FloorSelectorCycles.backwardA).kronecker(FloorSelectorCycles.rowSelectorGD).transpose).rank=min(A\cdot D)(B\cdot G)$$

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

Source. Repository-derived.

Commentary.

For 0 < B ≤ A, 0 < D ≤ G and p > 0, the short reservoir Schur complement has rank min(AD,BG); ReservoirSchur.short_short_injective_witness combines this with the relevant dimension ordering to obtain an injective Schur map.

Theorem 1.28 (long_long_cyclic_schur_rank).

$$\forall (ABGDp:\mathbb{N}),0<A\to A\le B\to 0<G\to G\le D\to 0<p\to (((Coe.coe\left(p\right))+1)\cdot (FloorSelectorCycles.rowSelectorBA).transpose.kronecker(FloorSelectorCycles.rowSelectorDG)-(-FloorSelectorCycles.backwardB).transpose.kronecker(FloorSelectorCycles.rowSelectorDG)\cdot (1+(-FloorSelectorCycles.backwardB).transpose.kronecker(FloorSelectorCycles.forwardHalfD).transpose{)}^{-1}\cdot (FloorSelectorCycles.rowSelectorBA).transpose.kronecker(FloorSelectorCycles.forwardHalfD).transpose).rank=min(A\cdot D)(B\cdot G)$$

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

Source. Repository-derived.

Commentary.

For 0 < A ≤ B, 0 < G ≤ D and p > 0, the long reservoir Schur complement has rank min(AD,BG); LongReservoir.long_long_injective_witness uses this rank to eliminate the remaining kernel coordinates.

Theorem 1.29 (matrix_injective_of_rank).

$$\forall \{m:Type\}\{n:Type\}[Fintypem][Fintypen][DecidableEqn](A:Matrixmn\mathbb{Q}),A.rank=Fintype.cardn\to Function.Injective(CoeFun.coe\left(A.mulVecLin\right))$$

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

Source. Repository-derived.

Commentary.

A rational matrix whose rank equals its number of columns defines an injective linear map; LongReservoir.long_long_injective_witness applies this to its full-column-rank Schur complement.

Theorem 1.30 (schur_two_equations).

$$\forall \{m:Type\}\{n:Type\}\{k:Type\}[Fintypem][Fintypen][Fintypek][DecidableEqm][DecidableEqn][DecidableEqk](R:Matrixmm\mathbb{Q})(T:Matrixmn\mathbb{Q})(L:Matrixkm\mathbb{Q})(H:Matrixkn\mathbb{Q}),IsUnitR\to Function.Injective(H-L\cdot R^{-1}\cdot T).mulVec\to \forall (v:m\to \mathbb{Q})(w:n\to \mathbb{Q}),R.mulVecv+T.mulVecw=0\to L.mulVecv+H.mulVecw=0\to v=0\wedge w=0$$

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

Source. Repository-derived.

Commentary.

If R is invertible and H-LR⁻¹T is injective, the two displayed coupled homogeneous equations imply v=w=0; ReservoirSchur.short_reservoir_injective and LongReservoir.long_reservoir_injective use this to prove injectivity of the augmented flow matrices.

References

• Truth anchor: D5/S3/Quantum/TensorNetworks/BridgeGraph/ShiftPencilBlocks.ParameterizedBaseWitness
• Truth anchor: D5/S3/Quantum/TensorNetworks/BridgeGraph/ShiftPencilBlocks.antiDiagonal
• Truth anchor: D5/S3/Quantum/TensorNetworks/BridgeGraph/ShiftPencilBlocks.antiDiagonal_kernel
• Truth anchor: D5/S3/Quantum/TensorNetworks/BridgeGraph/ShiftPencilBlocks.arrow0
• Truth anchor: D5/S3/Quantum/TensorNetworks/BridgeGraph/ShiftPencilBlocks.arrow1
• Truth anchor: D5/S3/Quantum/TensorNetworks/BridgeGraph/ShiftPencilBlocks.base_of_parameterized
• Truth anchor: D5/S3/Quantum/TensorNetworks/BridgeGraph/ShiftPencilBlocks.blockLength
• Truth anchor: D5/S3/Quantum/TensorNetworks/BridgeGraph/ShiftPencilBlocks.block_mulVec
• Truth anchor: D5/S3/Quantum/TensorNetworks/BridgeGraph/ShiftPencilBlocks.cols_card
• Truth anchor: D5/S3/Quantum/TensorNetworks/BridgeGraph/ShiftPencilBlocks.different_depth_witness
• Truth anchor: D5/S3/Quantum/TensorNetworks/BridgeGraph/ShiftPencilBlocks.double_fin_pick
• Truth anchor: D5/S3/Quantum/TensorNetworks/BridgeGraph/ShiftPencilBlocks.leftDim
• Truth anchor: D5/S3/Quantum/TensorNetworks/BridgeGraph/ShiftPencilBlocks.long_long_cyclic_schur_rank
• Truth anchor: D5/S3/Quantum/TensorNetworks/BridgeGraph/ShiftPencilBlocks.matrix_injective_of_rank
• Truth anchor: D5/S3/Quantum/TensorNetworks/BridgeGraph/ShiftPencilBlocks.neg_one_pow_square
• Truth anchor: D5/S3/Quantum/TensorNetworks/BridgeGraph/ShiftPencilBlocks.pencil
• Truth anchor: D5/S3/Quantum/TensorNetworks/BridgeGraph/ShiftPencilBlocks.pencil_mulVec
• Truth anchor: D5/S3/Quantum/TensorNetworks/BridgeGraph/ShiftPencilBlocks.pencil_rank_of_le
• Truth anchor: D5/S3/Quantum/TensorNetworks/BridgeGraph/ShiftPencilBlocks.rectExtend
• Truth anchor: D5/S3/Quantum/TensorNetworks/BridgeGraph/ShiftPencilBlocks.rightDim
• Truth anchor: D5/S3/Quantum/TensorNetworks/BridgeGraph/ShiftPencilBlocks.rows_card
• Truth anchor: D5/S3/Quantum/TensorNetworks/BridgeGraph/ShiftPencilBlocks.same_depth_kernel_dimension
• Truth anchor: D5/S3/Quantum/TensorNetworks/BridgeGraph/ShiftPencilBlocks.schur_two_equations
• Truth anchor: D5/S3/Quantum/TensorNetworks/BridgeGraph/ShiftPencilBlocks.shift1
• Truth anchor: D5/S3/Quantum/TensorNetworks/BridgeGraph/ShiftPencilBlocks.short_short_cyclic_schur_rank
• Truth anchor: D5/S3/Quantum/TensorNetworks/BridgeGraph/ShiftPencilBlocks.tensorBlockEquiv
• Truth anchor: D5/S3/Quantum/TensorNetworks/BridgeGraph/ShiftPencilBlocks.widthTwoMatrix
• Truth anchor: D5/S3/Quantum/TensorNetworks/BridgeGraph/ShiftPencilBlocks.widthTwo_block_decomposition
• Truth anchor: D5/S3/Quantum/TensorNetworks/BridgeGraph/ShiftPencilBlocks.witness_of_typed_slices
• Truth anchor: D5/S3/Quantum/TensorNetworks/BridgeGraph/ShiftPencilBlocks.zero_defect_witness
• Dependency: D5/S3/Quantum/TensorNetworks/BridgeGraph/CyclicResolvent
• Dependency: D5/S3/Quantum/TensorNetworks/BridgeGraph/QuantumMaxFlowBound