Exact nonclosed-cap boundary potential

Abstract

Exact nonclosed-cap boundary potential.

Theorem 1.1 (Exact nonclosed-cap boundary potential).

$$\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)\ne \mathrm{Succ}\left(j\right)\Rightarrow \left(\left(\forall a\in L,\mathrm{Apply}\left(q,a\right)\ne 0\right)\Rightarrow \left(\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,\mathrm{CapSurgery}\left(M,j\right),y\right)\right)\right)$$

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

Source. Repository-derived.

Commentary.

For an arbitrary finite label type and everywhere nonzero real weights, a compatible detour satisfies the nonclosed-cap potential identity. The affected opening factors cancel using nonvanishing, while the entire unaffected product remains common. No positivity, eigenvector equation, or special label graph is assumed.

References

• Truth anchor: D5/S3/Combinatorics/PerfectMatchings/NonclosedCapPotential.nonclose_boundaryPotential
• Dependency: D5/S3/Combinatorics/PerfectMatchings/NonclosedCapLabels