Legal-path cap fibers

Abstract

Legal-path cap fibers.

Definition 1.1 (Legal-path cap fibers).

$$\forall L\in FiniteDecidableType,\forall R\in \mathrm{Relation}\left(L\right),\forall q\in \mathrm{Function}\left(L,Real\right),\forall s\in L,\forall m\in Natural,\forall M\in \mathrm{NCMatching}\left(m+2\right),\forall j\in \mathrm{Fin}\left(m+1\right),\mathrm{CapFiberGoal}\left(R,q,s,m,M,j\right)\iff \left(\exists N\in \mathrm{NCMatching}\left(m\right),\left(\forall k\in \mathrm{Fin}\left(m\right),\mathrm{SkipPair}\left(j,\mathrm{Partner}\left(N,k\right)\right)=\mathrm{ReconnectPartner}\left(M,j,\mathrm{SkipPair}\left(j,k\right)\right)\right)\wedge \left(\forall y\in \mathrm{LegalPath}\left(R,m,s,s\right),\left(\mathrm{Partner}\left(M,\mathrm{CastSucc}\left(j\right)\right)=\mathrm{Succ}\left(j\right)\Rightarrow \left(\left(\forall b\in \mathrm{NeighborLabels}\left(R,\mathrm{Apply}\left(y,j\right)\right),\mathrm{Compatible}\left(M,\mathrm{DetourLabels}\left(j,y,b\right)\right)\iff \mathrm{Compatible}\left(N,y\right)\right)\wedge \left(\forall b\in \mathrm{NeighborLabels}\left(R,\mathrm{Apply}\left(y,j\right)\right),\mathrm{BoundaryPotential}\left(q,M,\mathrm{DetourLabels}\left(j,y,b\right)\right)\cdot \mathrm{Divide}\left(\mathrm{Apply}\left(q,b\right),\mathrm{Apply}\left(q,\mathrm{Apply}\left(y,j\right)\right)\right)=\mathrm{Square}\left(\mathrm{Divide}\left(\mathrm{Apply}\left(q,b\right),\mathrm{Apply}\left(q,\mathrm{Apply}\left(y,j\right)\right)\right)\right)\cdot \mathrm{BoundaryPotential}\left(q,N,y\right)\right)\right)\right)\wedge \left(\mathrm{Partner}\left(M,\mathrm{CastSucc}\left(j\right)\right)\ne \mathrm{Succ}\left(j\right)\Rightarrow \left(\left(\mathrm{Compatible}\left(N,y\right)\iff \left(\exists b\in \mathrm{NeighborLabels}\left(R,\mathrm{Apply}\left(y,j\right)\right),\mathrm{Compatible}\left(M,\mathrm{DetourLabels}\left(j,y,b\right)\right)\wedge \left(\forall c\in \mathrm{NeighborLabels}\left(R,\mathrm{Apply}\left(y,j\right)\right),\mathrm{Compatible}\left(M,\mathrm{DetourLabels}\left(j,y,c\right)\right)\Rightarrow c=b\right)\right)\right)\wedge \left(\forall b\in \mathrm{NeighborLabels}\left(R,\mathrm{Apply}\left(y,j\right)\right),\mathrm{Compatible}\left(M,\mathrm{DetourLabels}\left(j,y,b\right)\right)\Rightarrow \mathrm{BoundaryPotential}\left(q,M,\mathrm{DetourLabels}\left(j,y,b\right)\right)\cdot \mathrm{Divide}\left(\mathrm{Apply}\left(q,b\right),\mathrm{Apply}\left(q,\mathrm{Apply}\left(y,j\right)\right)\right)=\mathrm{BoundaryPotential}\left(q,N,y\right)\right)\right)\right)\right)\right)$$

Formalization. D5/S3/Quantum/Algebra/Knot/CapFiberContract.CapFiberGoal (✓ std3).

Source. Repository-derived.

Commentary.

FiniteDecidableType denotes any finite label type with decidable equality. NeighborLabels(R,a) is the subtype of labels b satisfying R(a,b); formulas involving such a neighbor use its underlying label. Apply is function evaluation, CastSucc and Succ are the left and right gap inclusions, and Square is the ordinary second power. Fix an arbitrary label relation, real label weights, a root, an adjacent cap and a noncrossing matching. The goal requires a smaller matching with the exact rewiring and both complete cap-fiber laws over the existing rooted LegalPath carrier. The closed law quantifies every neighboring middle label and includes the squared ratio. The nonclosed law requires a unique legal neighbor exactly when the smaller labels are compatible, and the exact potential transport for each compatible lift.

References

• Truth anchor: D5/S3/Quantum/Algebra/Knot/CapFiberContract.CapFiberGoal
• Dependency: D5/S3/Combinatorics/PerfectMatchings/OrderedMatchingCore
• Dependency: D5/S3/Quantum/Algebra/WeightedLegalPathTemperleyLieb