FloorSelectorCycles

Abstract

FloorSelectorCycles 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 (jump).

$$\forall (\rho :\mathbb{Q})(n:\mathbb{Z}),FloorSelectorCycles.jump\rho n=(Int.ceil\left((Coe.coe\left(n+1\right))\cdot \rho \right)-Int.ceil\left((Coe.coe\left(n\right))\cdot \rho \right))$$

Formalization. D5/S3/Quantum/TensorNetworks/BridgeGraph/FloorSelectorCycles.jump (✓ std3).

Source. Repository-derived.

Commentary.

jump is the difference between consecutive ceilings of n*ρ; jump_zero_or_one bounds its values for slopes between zero and one, allowing it to represent selector events.

Theorem 1.2 (jump_zero_or_one).

$$\forall \{\rho :\mathbb{Q}\},0\le \rho \to \rho \le 1\to \forall (n:\mathbb{Z}),FloorSelectorCycles.jump\rho n=0\vee FloorSelectorCycles.jump\rho n=1$$

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

Source. Repository-derived.

Commentary.

For 0 ≤ ρ ≤ 1, every ceiling increment is zero or one; CyclicResolvent.forward_supported_zero applies this to the input and output slopes in the balanced-cycle recurrence.

Theorem 1.3 (opposite_direction_excess).

$$\forall \{{\rho }_I{\rho }_O:\mathbb{Q}\},{\rho }_I\le {\rho }_O\to \forall (phaseIphaseO:\mathbb{Z})(len:\mathbb{N}),\sum _{t\in Finset.rangelen}((FloorSelectorCycles.jump{\rho }_I(phaseI+(Coe.coe\left(t\right)))-FloorSelectorCycles.jump{\rho }_O(phaseO-(Coe.coe\left(t\right)))))\le 1$$

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

Source. Repository-derived.

Commentary.

When ρI ≤ ρO, the input ceiling increments along a forward interval exceed the output increments along a backward interval by at most one; CyclicResolvent.forward_supported_zero uses this as the interval balance inequality.

Theorem 1.4 (jump_one_iff_fin_selector).

$$\forall (AB:\mathbb{N}),0<B\to B\le A\to \forall (n:FinA),FloorSelectorCycles.jump(((B:\mathbb{Q}))HDiv.hDiv((A:\mathbb{Q})))(((\mathrm{val}\left(n\right)):\mathbb{Z}))=1⟺\exists (k:FinB),(\mathrm{val}\left(n\right))=(\mathrm{val}\left(k\right))\cdot AHDiv.hDivB$$

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

Source. Repository-derived.

Commentary.

For 0 < B ≤ A, a ceiling increment at n in Fin A equals one exactly when n is one of the positions floor(k*A/B) with k in Fin B; CyclicResolvent.forward_supported_zero uses this equivalence to express coordinate support as selector events.

Theorem 1.5 (monodromy_forces_zero).

$$\forall (\mu z:\mathbb{Q}),\mu <1\to z=\mu \cdot z\to z=0$$

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

Source. Repository-derived.

Commentary.

A rational value fixed by multiplication by μ < 1 must vanish; balanced_cycle_zero applies this after propagating a coordinate around a full period.

Theorem 1.6 (half_pow_lt_one).

$$\forall \{n:\mathbb{N}\},0<n\to (1HDiv.hDiv2{)}^n<1$$

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

Source. Repository-derived.

Commentary.

Every positive power of the rational number 1/2 is strictly below one; tensor_edge_product_lt_one uses this to bound the product of weights around the tensor cycle.

Theorem 1.7 (recurrence_product_bounded).

$$\forall (zf:\mathbb{N}\to \mathbb{Q})(L:\mathbb{N}),(\forall n<L,z(n+1)=fn\cdot zn)\to zL=(\prod _{t\in Finset.rangeL}(ft))\cdot z0$$

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

Source. Repository-derived.

Commentary.

Iterating a multiplicative recurrence over L steps multiplies the initial value by the product of its L factors; balanced_cycle_zero uses this identity to compare a coordinate with its value one period later.

Theorem 1.8 (balanced_cycle_zero).

$$\forall (io:\mathbb{Z}\to \mathbb{Z})(zc:\mathbb{Z}\to \mathbb{Q}),(\forall (n:\mathbb{Z}),in=0\vee in=1)\to (\forall (n:\mathbb{Z}),on=0\vee on=1)\to (\forall (n:\mathbb{Z}),in=on\to zn=cn\cdot z(n-1))\to (\forall (n:\mathbb{Z}),cn\ne 0)\to (\forall (n:\mathbb{Z}),in=0\to on=1\to zn=0\wedge z(n-1)=0)\to (\forall (a:\mathbb{Z})(len:\mathbb{N}),\sum _{t\in Finset.rangelen}((i(a+(Coe.coe\left(t\right)))-o(a+(Coe.coe\left(t\right)))))\le 1)\to \forall (L:\mathbb{N}),0<L\to (\forall (n:\mathbb{Z}),z(n+(Coe.coe\left(L\right)))=zn)\to (\forall (a:\mathbb{Z}),\sum _{t\in Finset.rangeL}((i(a+(Coe.coe\left(t\right)))-o(a+(Coe.coe\left(t\right)))))\le 0)\to (\forall (a:\mathbb{Z}),\prod _{t\in Finset.rangeL}(c(a+(Coe.coe\left(t\right))+1))<1)\to \forall (a:\mathbb{Z}),za=0$$

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

Source. Repository-derived.

Commentary.

Under the displayed recurrence and zero conditions, binary input and output sequences with interval excess at most one and nonpositive full-period excess force every periodic coordinate to vanish when each period product is below one. CyclicResolvent.shifted_recurrence_zero applies this to the supported reservoir equations.

Theorem 1.9 (common_node_product_bound).

$$\forall (\kappa :\mathbb{Q}),0<\kappa \to \forall (o:\mathbb{Z}\to \mathbb{Z})(w:\mathbb{Z}\to \mathbb{Q}),(\forall (n:\mathbb{Z}),0<wn)\to \forall (a:\mathbb{Z})(L:\mathbb{N}),\prod _{t\in Finset.rangeL}((ifo(a+(Coe.coe\left(t\right))+1)=1then\kappa HDiv.hDiv(\kappa +1)else1)\cdot w(a+(Coe.coe\left(t\right))+1))\le \prod _{t\in Finset.rangeL}(w(a+(Coe.coe\left(t\right))+1))$$

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

Source. Repository-derived.

Commentary.

For κ > 0 and positive weights, inserting a factor κ/(κ+1) at output events cannot increase the product of weights; CyclicResolvent.shifted_recurrence_zero uses this to preserve the strict period-product bound.

Definition 1.10 (backward).

$$\forall (A:\mathbb{N}),FloorSelectorCycles.backwardA=(Matrix.submatrix1((CoeFun.coe\left(finRotateA\right)))id)$$

Formalization. D5/S3/Quantum/TensorNetworks/BridgeGraph/FloorSelectorCycles.backward (✓ std3).

Source. Repository-derived.

Commentary.

backward is the unweighted cyclic shift obtained by rotating the rows of the identity matrix; tensor_mulVec_orbit uses it to decrease the first orbit coordinate by one.

Theorem 1.11 (backward_apply).

$$\forall (A:\mathbb{N})(ij:FinA),FloorSelectorCycles.backwardAij=if(\mathrm{val}\left(j\right))=((\mathrm{val}\left(i\right))+1)HMod.hModAthen1else0$$

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

Source. Repository-derived.

Commentary.

The entry of backward at (i,j) is one exactly when j is the cyclic successor of i and is zero otherwise; tensor_mulVec_orbit uses this entry formula to isolate the preceding orbit position.

Definition 1.12 (forwardHalf).

$$\forall (G:\mathbb{N}),FloorSelectorCycles.forwardHalfG=((Matrix.diagonalfun(k:FinG)\mapsto if(\mathrm{val}\left(k\right))=0then1HDiv.hDiv2else1).submatrixid(CoeFun.coe\left(finRotateG\right)))$$

Formalization. D5/S3/Quantum/TensorNetworks/BridgeGraph/FloorSelectorCycles.forwardHalf (✓ std3).

Source. Repository-derived.

Commentary.

forwardHalf is the opposite cyclic shift with weight 1/2 at row zero and weight one elsewhere; tensor_mulVec_orbit uses this weight to describe propagation in the second coordinate.

Theorem 1.13 (forwardHalf_apply).

$$\forall (G:\mathbb{N})(ij:FinG),FloorSelectorCycles.forwardHalfGij=if(\mathrm{val}\left(j\right))=((\mathrm{val}\left(i\right))+G-1)HMod.hModGthenif(\mathrm{val}\left(i\right))=0then1HDiv.hDiv2else1else0$$

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

Source. Repository-derived.

Commentary.

The entry of forwardHalf at (i,j) is nonzero only when j is the cyclic predecessor of i, with weight 1/2 at i=0 and one elsewhere; tensor_mulVec_orbit uses this formula to obtain the factor edge.

Definition 1.14 (rowSelector).

$$\forall (AB:\mathbb{N}),FloorSelectorCycles.rowSelectorAB=((Matrix.submatrix1Fin.valfun(k:FinB)\mapsto (\mathrm{val}\left(k\right))\cdot AHDiv.hDivB).transpose)$$

Formalization. D5/S3/Quantum/TensorNetworks/BridgeGraph/FloorSelectorCycles.rowSelector (✓ std3).

Source. Repository-derived.

Commentary.

rowSelector samples positions floor(k*A/B) from an A-coordinate vector into B coordinates; CyclicResolvent.input_matrix and output_matrix express the tensor input and output maps using these selectors.

Definition 1.15 (reservoir).

$$\forall (AG:\mathbb{N}),FloorSelectorCycles.reservoirAG=(1+(-FloorSelectorCycles.backwardA).kronecker(FloorSelectorCycles.forwardHalfG))$$

Formalization. D5/S3/Quantum/TensorNetworks/BridgeGraph/FloorSelectorCycles.reservoir (✓ std3).

Source. Repository-derived.

Commentary.

reservoir is the identity minus the Kronecker product of the two oppositely directed cyclic shifts; CyclicResolvent.reservoir_isUnit proves its invertibility by propagating its homogeneous equation around each orbit.

Definition 1.16 (schurMap).

$$\forall (ABGD:\mathbb{N})(\kappa :\mathbb{Q}),FloorSelectorCycles.schurMapABGD\kappa =(\kappa \cdot (FloorSelectorCycles.rowSelectorAB).kronecker(FloorSelectorCycles.rowSelectorGD).transpose+(FloorSelectorCycles.rowSelectorAB).kronecker1\cdot (FloorSelectorCycles.reservoirAG{)}^{-1}\cdot Matrix.kronecker1(FloorSelectorCycles.rowSelectorGD).transpose)$$

Formalization. D5/S3/Quantum/TensorNetworks/BridgeGraph/FloorSelectorCycles.schurMap (✓ std3).

Source. Repository-derived.

Commentary.

schurMap restricts κ times the identity plus the inverse reservoir to the selected input and output coordinates; CyclicResolvent.schur_eq_restricted expresses this restriction through coordinate-insertion matrices.

Definition 1.17 (CyclicResolventLemma).

$$FloorSelectorCycles.CyclicResolventLemma⟺(\forall (ABGD:\mathbb{N}),0<B\to B\le A\to 0<D\to D\le G\to \forall (\kappa :\mathbb{Q}),0<\kappa \to IsUnit(FloorSelectorCycles.reservoirAG)\wedge (A\cdot D\le B\cdot G\to Function.Injective(FloorSelectorCycles.schurMapABGD\kappa ).mulVec)\wedge (B\cdot G\le A\cdot D\to Function.Surjective(FloorSelectorCycles.schurMapABGD\kappa ).mulVec))$$

Formalization. D5/S3/Quantum/TensorNetworks/BridgeGraph/FloorSelectorCycles.CyclicResolventLemma (✓ std3).

Source. Repository-derived.

Commentary.

CyclicResolventLemma states invertibility of the reservoir and injectivity or surjectivity of schurMap according to the ordering of AD and BG, for positive ordered selector dimensions and κ > 0; CyclicResolvent.cyclic_resolvent_lemma proves these assertions.

Definition 1.18 (index).

$$\forall (N:\mathbb{N})(hN:0<N)(s:\mathbb{Z}),FloorSelectorCycles.indexNhNs=(⟨s.natMod(Coe.coe\left(N\right))⟩)$$

Formalization. D5/S3/Quantum/TensorNetworks/BridgeGraph/FloorSelectorCycles.index (✓ std3).

Source. Repository-derived.

Commentary.

For a positive modulus N, index maps an integer to its remainder in Fin N; orbit uses it to follow both cyclic coordinates for arbitrary integer steps.

Theorem 1.19 (index_val_int).

$$\forall (N:\mathbb{N})(hN:0<N)(s:\mathbb{Z}),(((\mathrm{val}\left(FloorSelectorCycles.indexNhNs\right)):\mathbb{Z}))=sHMod.hMod((N:\mathbb{Z}))$$

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

Source. Repository-derived.

Commentary.

The integer value of index is the integer remainder modulo N; index_nat uses this equality to recover an index already in Fin N.

Theorem 1.20 (index_nat).

$$\forall (N:\mathbb{N})(hN:0<N)(i:FinN),FloorSelectorCycles.indexNhN(((\mathrm{val}\left(i\right)):\mathbb{Z}))=i$$

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

Source. Repository-derived.

Commentary.

Reducing the value of an element of Fin N modulo N returns that element; CyclicResolvent.succ_pred_relation uses this to translate cyclic successor and predecessor equations into integer shifts.

Theorem 1.21 (index_add_multiple).

$$\forall (N:\mathbb{N})(hN:0<N)(sk:\mathbb{Z}),FloorSelectorCycles.indexNhN(s+k\cdot (Coe.coe\left(N\right)))=FloorSelectorCycles.indexNhNs$$

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

Source. Repository-derived.

Commentary.

Adding any integer multiple of N leaves index unchanged; orbit_period applies this in both coordinates to obtain a period of A*G.

Theorem 1.22 (index_add_one).

$$\forall (N:\mathbb{N})(hN:0<N)(s:\mathbb{Z}),(\mathrm{val}\left(FloorSelectorCycles.indexNhN(s+1)\right))=((\mathrm{val}\left(FloorSelectorCycles.indexNhNs\right))+1)HMod.hModN$$

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

Source. Repository-derived.

Commentary.

Increasing the integer argument of index by one advances its value by one modulo N; tensor_mulVec_orbit uses this to identify the first-coordinate shift.

Theorem 1.23 (index_sub_one).

$$\forall (N:\mathbb{N})(hN:0<N)(s:\mathbb{Z}),(\mathrm{val}\left(FloorSelectorCycles.indexNhN(s-1)\right))=((\mathrm{val}\left(FloorSelectorCycles.indexNhNs\right))+N-1)HMod.hModN$$

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

Source. Repository-derived.

Commentary.

Decreasing the integer argument of index by one gives its cyclic predecessor; tensor_mulVec_orbit uses this to identify the second-coordinate shift.

Definition 1.24 (orbit).

$$\forall (AG:\mathbb{N})(hA:0<A)(hG:0<G)(abs:\mathbb{Z}),FloorSelectorCycles.orbitAGhAhGabs=((FloorSelectorCycles.indexAhA(a-s),FloorSelectorCycles.indexGhG(b+s)))$$

Formalization. D5/S3/Quantum/TensorNetworks/BridgeGraph/FloorSelectorCycles.orbit (✓ std3).

Source. Repository-derived.

Commentary.

orbit follows the positions (a-s modulo A,b+s modulo G), with the two coordinates moving in opposite directions; CyclicResolvent.reservoir_mulVec_orbit expresses the reservoir equation along this orbit.

Definition 1.25 (edge).

$$\forall (G:\mathbb{N})(hG:0<G)(s:\mathbb{Z}),FloorSelectorCycles.edgeGhGs=(if(\mathrm{val}\left(FloorSelectorCycles.indexGhGs\right))=0then1HDiv.hDiv2else1)$$

Formalization. D5/S3/Quantum/TensorNetworks/BridgeGraph/FloorSelectorCycles.edge (✓ std3).

Source. Repository-derived.

Commentary.

edge assigns weight 1/2 at positions divisible by G and one at all other positions; tensor_mulVec_orbit identifies it as the coefficient relating successive orbit coordinates.

Theorem 1.26 (orbit_period).

$$\forall (AG:\mathbb{N})(hA:0<A)(hG:0<G)(abs:\mathbb{Z}),FloorSelectorCycles.orbitAGhAhGab(s+(Coe.coe\left(A\right))\cdot (Coe.coe\left(G\right)))=FloorSelectorCycles.orbitAGhAhGabs$$

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

Source. Repository-derived.

Commentary.

For positive A and G, shifting the orbit parameter by A*G returns the same pair of coordinates; CyclicResolvent.reservoir_isUnit uses this periodicity to close the homogeneous recurrence.

Theorem 1.27 (edge_pos).

$$\forall (G:\mathbb{N})(hG:0<G)(s:\mathbb{Z}),0<FloorSelectorCycles.edgeGhGs$$

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

Source. Repository-derived.

Commentary.

Every edge weight is strictly positive; CyclicResolvent.forward_supported_zero uses this to satisfy the nonzero propagation condition in the balanced-cycle argument.

Theorem 1.28 (tensor_mulVec_orbit).

$$\forall (AG:\mathbb{N})(hA:0<A)(hG:0<G)(z:FinA\times FinG\to \mathbb{Q})(abs:\mathbb{Z}),((FloorSelectorCycles.backwardA).kronecker(FloorSelectorCycles.forwardHalfG)).mulVecz(FloorSelectorCycles.orbitAGhAhGabs)=FloorSelectorCycles.edgeGhG(b+s)\cdot z(FloorSelectorCycles.orbitAGhAhGab(s-1))$$

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

Source. Repository-derived.

Commentary.

The Kronecker shift sends the value at an orbit position to edge times the value at the preceding position; CyclicResolvent.reservoir_mulVec_orbit subtracts this contribution from the identity term.

Theorem 1.29 (whole_tensor_excess).

$$\forall (ABGD:\mathbb{N}),0<A\to 0<G\to \forall (phaseIphaseO:\mathbb{Z}),\sum _{t\in Finset.range(A\cdot G)}((FloorSelectorCycles.jump((Coe.coe\left(D\right))HDiv.hDiv(Coe.coe\left(G\right)))(phaseI+(Coe.coe\left(t\right)))-FloorSelectorCycles.jump((Coe.coe\left(B\right))HDiv.hDiv(Coe.coe\left(A\right)))(phaseO-(Coe.coe\left(t\right)))))=(Coe.coe\left(A\cdot D\right))-(Coe.coe\left(G\cdot B\right))$$

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

Source. Repository-derived.

Commentary.

Over AG steps with A,G > 0, the difference between the input and output event counts is exactly AD-G*B; CyclicResolvent.forward_supported_zero uses the dimension ordering to make this full-period excess nonpositive.

Theorem 1.30 (jump_index).

$$\forall (AB:\mathbb{N})(hA:0<A)(s:\mathbb{Z}),FloorSelectorCycles.jump(((B:\mathbb{Q}))HDiv.hDiv((A:\mathbb{Q})))(((\mathrm{val}\left(FloorSelectorCycles.indexAhAs\right)):\mathbb{Z}))=FloorSelectorCycles.jump(((B:\mathbb{Q}))HDiv.hDiv((A:\mathbb{Q})))s$$

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

Source. Repository-derived.

Commentary.

For positive A, reducing an integer modulo A does not change the ceiling increment of slope B/A; CyclicResolvent.forward_supported_zero uses this to identify selector events along integer orbit parameters.

Theorem 1.31 (edge_product).

$$\forall (GM:\mathbb{N})(hG:0<G)(phase:\mathbb{Z}),\prod _{t\in Finset.range(M\cdot G)}(FloorSelectorCycles.edgeGhG(phase+(Coe.coe\left(t\right))))=(1HDiv.hDiv2{)}^M$$

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

Source. Repository-derived.

Commentary.

Over M*G consecutive positions with G > 0, the product of edge weights is (1/2)^M, independently of the starting phase; tensor_edge_product_lt_one uses this formula over a tensor period.

Theorem 1.32 (tensor_edge_product_lt_one).

$$\forall (AG:\mathbb{N}),0<A\to \forall (hG:0<G)(phase:\mathbb{Z}),\prod _{t\in Finset.range(A\cdot G)}(FloorSelectorCycles.edgeGhG(phase+(Coe.coe\left(t\right))+1))<1$$

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

Source. Repository-derived.

Commentary.

For positive A and G, the product of edge weights over A*G consecutive orbit steps is strictly below one; CyclicResolvent.reservoir_isUnit uses this contraction to force its homogeneous kernel to vanish.

References

• Truth anchor: D5/S3/Quantum/TensorNetworks/BridgeGraph/FloorSelectorCycles.CyclicResolventLemma
• Truth anchor: D5/S3/Quantum/TensorNetworks/BridgeGraph/FloorSelectorCycles.backward
• Truth anchor: D5/S3/Quantum/TensorNetworks/BridgeGraph/FloorSelectorCycles.backward_apply
• Truth anchor: D5/S3/Quantum/TensorNetworks/BridgeGraph/FloorSelectorCycles.balanced_cycle_zero
• Truth anchor: D5/S3/Quantum/TensorNetworks/BridgeGraph/FloorSelectorCycles.common_node_product_bound
• Truth anchor: D5/S3/Quantum/TensorNetworks/BridgeGraph/FloorSelectorCycles.edge
• Truth anchor: D5/S3/Quantum/TensorNetworks/BridgeGraph/FloorSelectorCycles.edge_pos
• Truth anchor: D5/S3/Quantum/TensorNetworks/BridgeGraph/FloorSelectorCycles.edge_product
• Truth anchor: D5/S3/Quantum/TensorNetworks/BridgeGraph/FloorSelectorCycles.forwardHalf
• Truth anchor: D5/S3/Quantum/TensorNetworks/BridgeGraph/FloorSelectorCycles.forwardHalf_apply
• Truth anchor: D5/S3/Quantum/TensorNetworks/BridgeGraph/FloorSelectorCycles.half_pow_lt_one
• Truth anchor: D5/S3/Quantum/TensorNetworks/BridgeGraph/FloorSelectorCycles.index
• Truth anchor: D5/S3/Quantum/TensorNetworks/BridgeGraph/FloorSelectorCycles.index_add_multiple
• Truth anchor: D5/S3/Quantum/TensorNetworks/BridgeGraph/FloorSelectorCycles.index_add_one
• Truth anchor: D5/S3/Quantum/TensorNetworks/BridgeGraph/FloorSelectorCycles.index_nat
• Truth anchor: D5/S3/Quantum/TensorNetworks/BridgeGraph/FloorSelectorCycles.index_sub_one
• Truth anchor: D5/S3/Quantum/TensorNetworks/BridgeGraph/FloorSelectorCycles.index_val_int
• Truth anchor: D5/S3/Quantum/TensorNetworks/BridgeGraph/FloorSelectorCycles.jump
• Truth anchor: D5/S3/Quantum/TensorNetworks/BridgeGraph/FloorSelectorCycles.jump_index
• Truth anchor: D5/S3/Quantum/TensorNetworks/BridgeGraph/FloorSelectorCycles.jump_one_iff_fin_selector
• Truth anchor: D5/S3/Quantum/TensorNetworks/BridgeGraph/FloorSelectorCycles.jump_zero_or_one
• Truth anchor: D5/S3/Quantum/TensorNetworks/BridgeGraph/FloorSelectorCycles.monodromy_forces_zero
• Truth anchor: D5/S3/Quantum/TensorNetworks/BridgeGraph/FloorSelectorCycles.opposite_direction_excess
• Truth anchor: D5/S3/Quantum/TensorNetworks/BridgeGraph/FloorSelectorCycles.orbit
• Truth anchor: D5/S3/Quantum/TensorNetworks/BridgeGraph/FloorSelectorCycles.orbit_period
• Truth anchor: D5/S3/Quantum/TensorNetworks/BridgeGraph/FloorSelectorCycles.recurrence_product_bounded
• Truth anchor: D5/S3/Quantum/TensorNetworks/BridgeGraph/FloorSelectorCycles.reservoir
• Truth anchor: D5/S3/Quantum/TensorNetworks/BridgeGraph/FloorSelectorCycles.rowSelector
• Truth anchor: D5/S3/Quantum/TensorNetworks/BridgeGraph/FloorSelectorCycles.schurMap
• Truth anchor: D5/S3/Quantum/TensorNetworks/BridgeGraph/FloorSelectorCycles.tensor_edge_product_lt_one
• Truth anchor: D5/S3/Quantum/TensorNetworks/BridgeGraph/FloorSelectorCycles.tensor_mulVec_orbit
• Truth anchor: D5/S3/Quantum/TensorNetworks/BridgeGraph/FloorSelectorCycles.whole_tensor_excess