Closed-cap compatibility and weight transport

Abstract

Closed-cap compatibility and weight transport.

Theorem 1.1 (Closed-cap compatibility and weight transport).

$$\forall L\in Type,\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{Function}\left(\mathrm{Fin}\left(m+1\right),L\right),\forall b\in L,\mathrm{Partner}\left(M,\mathrm{CastSucc}\left(j\right)\right)=\mathrm{Succ}\left(j\right)\Rightarrow \left(\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)$$

Proof. Machine-checked in Lean as D5/S3/Combinatorics/PerfectMatchings/ClosedCapFiber.close_compatible_iff (✓ std3). ∎

Source. Repository-derived.

Commentary.

When the original endpoints already form a pair, the inserted middle label is free. Compatibility of the full detour is equivalent to compatibility of the smaller matching for every middle label.

Theorem 1.2 (Closed-cap compatibility and weight transport).

$$\forall L\in Type,\forall m\in Natural,\forall M\in \mathrm{NCMatching}\left(m+2\right),\forall j\in \mathrm{Fin}\left(m+1\right),\forall q\in \mathrm{Function}\left(L,Real\right),\forall y\in \mathrm{Function}\left(\mathrm{Fin}\left(m+1\right),L\right),\forall b\in L,\mathrm{Partner}\left(M,\mathrm{CastSucc}\left(j\right)\right)=\mathrm{Succ}\left(j\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{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)$$

Proof. Machine-checked in Lean as D5/S3/Combinatorics/PerfectMatchings/ClosedCapFiber.close_boundaryPotential (✓ std3). ∎

Source. Repository-derived.

Commentary.

For arbitrary real weights, multiplying the original boundary potential by the cap weight ratio gives its square times the smaller potential. The identity includes incompatible shorter labellings, where both sides vanish, and real division is the usual total field operation.

References

• Truth anchor: D5/S3/Combinatorics/PerfectMatchings/ClosedCapFiber.close_boundaryPotential
• Truth anchor: D5/S3/Combinatorics/PerfectMatchings/ClosedCapFiber.close_compatible_iff
• Dependency: D5/S3/Combinatorics/PerfectMatchings/BoundaryProductTransport