Adjacent cap fibers of rooted legal paths

Abstract

Adjacent cap fibers of rooted legal paths.

Definition 1.1 (Adjacent cap fibers of rooted legal paths).

$$\forall L\in FiniteDecidableType,\forall R\in \mathrm{Relation}\left(L\right),\forall s\in L,\forall m\in Natural,\forall j\in \mathrm{Fin}\left(m+1\right),\forall y\in \mathrm{LegalPath}\left(R,m,s,s\right),\forall b\in \mathrm{NeighborLabels}\left(R,\mathrm{Apply}\left(y,j\right)\right),\mathrm{Symmetric}\left(R\right)\Rightarrow \mathrm{UnderlyingLabels}\left(\mathrm{LegalDetour}\left(R,s,j,y,b\right)\right)=\mathrm{DetourLabels}\left(j,y,b\right)$$

Formalization. D5/S3/Quantum/Algebra/Knot/LegalCapFibers.legalDetour (✓ std3).

Source. Repository-derived.

Commentary.

A neighbor of the cap gap gives a genuine rooted legal detour of length two more. Symmetry of the relation supplies its reverse edge, the original endpoints stay fixed, and every unaffected edge comes from the original path.

Theorem 1.2 (Adjacent cap fibers of rooted legal paths).

$$\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),\forall y\in \mathrm{LegalPath}\left(R,m,s,s\right),\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(\mathrm{CapSurgery}\left(M,j\right),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,\mathrm{CapSurgery}\left(M,j\right),y\right)\right)\right)$$

Proof. Machine-checked in Lean as D5/S3/Quantum/Algebra/Knot/LegalCapFibers.capSurgery_close_fiber (✓ std3). ∎

Source. Repository-derived.

Commentary.

The closed compatibility and squared-weight identities hold for the complete neighbor fiber, including empty fibers.

Theorem 1.3 (Adjacent cap fibers of rooted legal paths).

$$\forall L\in FiniteDecidableType,\forall R\in \mathrm{Relation}\left(L\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),\forall y\in \mathrm{LegalPath}\left(R,m,s,s\right),\mathrm{Partner}\left(M,\mathrm{CastSucc}\left(j\right)\right)\ne \mathrm{Succ}\left(j\right)\Rightarrow \left(\mathrm{Symmetric}\left(R\right)\Rightarrow \left(\mathrm{Compatible}\left(\mathrm{CapSurgery}\left(M,j\right),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)\right)$$

Proof. Machine-checked in Lean as D5/S3/Quantum/Algebra/Knot/LegalCapFibers.nonclose_legal_fiber (✓ std3). ∎

Source. Repository-derived.

Commentary.

The nonclosed compatible middle label is a genuine neighbor. Its legality follows from the surviving path edge and symmetry, and subtype extensionality gives uniqueness. No nonempty path-space assumption is required.

References

• Truth anchor: D5/S3/Quantum/Algebra/Knot/LegalCapFibers.capSurgery_close_fiber
• Truth anchor: D5/S3/Quantum/Algebra/Knot/LegalCapFibers.legalDetour
• Truth anchor: D5/S3/Quantum/Algebra/Knot/LegalCapFibers.nonclose_legal_fiber
• Dependency: D5/S3/Combinatorics/PerfectMatchings/NonclosedCapLabels
• Dependency: D5/S3/Quantum/Algebra/Knot/CapFiberContract