Keyboard shortcuts

Press ← or → to navigate between chapters

Press ? to show this help

Press Esc to hide this help

Actual rectangular residuals and port absorption

Abstract

Every feasible matching and singleton set on an actual even rectangle determines residual capacities, legal port routings, and a signed inequality for every such routing.

Theorem 1.1 (The full actual residual bridge).

Lean statement: D5/S3/Combinatorics/Graph/ActualRectangularResidualBridge.actual_even_rectangular_residual_bridge

Proof. Machine-checked in Lean as D5/S3/Combinatorics/Graph/ActualRectangularResidualBridge.actual_even_rectangular_residual_bridge (✓ std3). ∎

Source. Repository-derived.

Commentary.

For every positive natural a,b, finite type E with decidable equality, maps src,dst:E→Fin(2a)×Fin(2b), and finite set T of rectangle vertices, assume each src(e),dst(e) pair is square-grid adjacent; the endpoint map from E×Bool, sending false to src and true to dst, is injective; and src(e),dst(e) both lie outside T. Put A=(T union image(src)) union image(dst), with images over all E. For every x in T assume that the cardinality of its square-grid neighbors in A is at most one. Adjacency uses the integer embeddings of the natural coordinates and means that one coordinate agrees and the other differs by one.

Define kappa(x)=(floor(x.row/2),floor(x.column/2)) in Fin a×Fin b. Let t(Q) count T in the tile Q; h(Q) count actual edges with both endpoint tiles Q; and s(Q) count actual edges with one endpoint in Q and the other in a distinct tile with t=2. Each counted object in h or s is an original edge identity. Put r(Q)=2−(t(Q)+h(Q)+s(Q)), with natural subtraction. ER is the subtype of e in E with distinct endpoint tiles and t<2 at both ends. Define rs(e)=kappa(src(e)), rd(e)=kappa(dst(e)), and chi(Q)=decide(Odd(Q.row+Q.column)).

Let H=2ab, C=|ER|, R=sum_Q r(Q), K=sum_Q(h(Q)+s(Q)), and ell be the number of residual leaf vertices. A residual leaf is a tile Q with r(Q)=0 and degree(rs,rd,Q)=1. Degree counts endpoint incidences of the actual ER identities. Define the signed integers q=|T|+|E|−H and D=H−|T|.

For every Q, t(Q)≤2, t(Q)+h(Q)+s(Q)+r(Q)=2, and r(Q)≤2. If t(Q)=2 then h(Q)=s(Q)=degree(rs,rd,Q)=0. Every original edge with distinct endpoint tiles avoids having t=2 at both ends. For every e in ER, rs(e)≠rd(e), the endpoint tiles are square-grid adjacent, and chi(rs(e))≠chi(rd(e)).

For each Q with r(Q)=0 and degree(rs,rd,Q)=1, s(Q)≥1. Every e in ER avoids having residual capacity zero at both ends. The counts satisfy ell≤sum_Q s(Q)≤K, |E|=sum_Q h(Q)+sum_Q s(Q)+C, |T|+R+K=H, q=C−R, and D=R+K, with the last two equalities in Int.

There exist proofs hzero that r(Q)=0 implies degree(rs,rd,Q)≤1, hpos that r(Q)>0 implies degree(rs,rd,Q)≤2r(Q), hleaf that no actual residual edge joins two residual leaves, and hK that the number of residual leaf vertices is at most K. For these same proofs there exists a port routing sigma that is involutive, preserves the base of every port, and fixes a port if and only if it is an L port. Real ports are (e,false),(e,true) for actual residual identities; slack ports at Q are indexed by Fin(2r(Q)−degree(rs,rd,Q)). L ports are real ports based at a residual leaf; H ports are slack ports.

For every routing sigma on this same port carrier, and every proof hσ that sigma is involutive, hbase that it preserves bases, and hfix that it fixes exactly the L ports, capacityPortClaim(rs,rd,r,K,sigma,hσ,hbase,hfix,hzero,hpos,hleaf,hK) holds. Let rho swap the two real ports of each residual edge and fix every slack port. The port graph joins distinct ports p,t exactly when t=rho(p) or t=sigma(p); the following components belong to this graph. Every component containing a terminal has two distinct terminal ports and a simple path whose support is exactly the component, which contains every graph edge internal to the component, and whose only terminal ports are those endpoints. Membership of the false real port of each original residual identity is equivalent to its real-port pair occurring in the path, and the exact number of such real-port steps is the component’s actual length lambda.

Let Acount,Bcount,Ccount count components of types LL,HH,LH respectively, and Ocount count LL components of odd actual length. Then ell=2Acount+Ccount, sum_Q(2r(Q)−degree(rs,rd,Q))=2Bcount+Ccount, q=Acount−Bcount, and D≥3q+4Bcount+2Ccount+Ocount. For every Bool coloring that changes across each actual ER edge, every LL component, and every two distinct L ports p,t in that component, lambda is odd if and only if the colors of their bases differ. These assertions concern every legal routing, with no restriction to the constructed routing.

For every one of these routings, the additional signed integer inequality is 8ab−4|T|−3|E|≥4Bcount+2Ccount+Ocount. Here Bcount=bCount(rs,rd,r,sigma), Ccount=cCount(rs,rd,r,sigma), and Ocount=oddLLCount(rs,rd,r,sigma); all natural counts and a,b are cast to Int before this arithmetic.

The blank vertices and separation in D5/S3/Combinatorics/Graph/ActualRectangularSaturatedGeometry.actual_even_rectangular_saturated_geometry constrain the actual received attachments. Counting the original tile corners and endpoint identities gives local capacities and both global count equalities. If a residual edge had zero capacity at both ends, the actual corner analysis across that edge forces adjacent occupied points in two saturated tiles, contradicting saturated separation. These conclusions supply the hypotheses of D5/S3/Combinatorics/Graph/CapacityPortParityAbsorption.actual_capacity_port_parity_absorption for every legal routing. The count equalities convert its signed bound into the stated rectangular inequality.

Empty edge and singleton sets are included; parallel coarse edges retain their original identities. This result does not assert an odd-rectangle extension, the global LL-to-HH injection, q≤0, or the unrestricted coefficient-one grid bound.

References