Weighted transport on actual tetrahedral face pairings

Abstract

Actual paired-corner paths lift nonnegative component weights with the occurrence bound 3B.

T and S are arbitrary finite types, including empty types. K is an arbitrary linearly ordered field. Corner=T x Fin(4), Occurrence=T x Fin(6), and Slot=(T x Fin(4)) x Fin(3). Pairing has a fixed-point-free involution p on whole faces and permutations sigma(x) with sigma(p(x))(sigma(x)(r))=r. Face f omits vertex f; its corner slots list the other vertices increasingly. Its edge slots are opposite those corners, in local order (12,13,14,34,24,23). The SAME sigma transports corners and opposite edges.

b(i) is the actual source corner and J(i)=(p(i.face),sigma(i.face)(i.slot)). Vertex is the equivalence closure quotient generated by b(i)~b(J(i)); GlobalEdge is the corresponding quotient of actual opposite-edge occurrences. label and P are these quotient maps. M(a,e) sums EVERY occurrence with P(o)=e; Q(a,c) sums the three local edges incident at c. Self-gluing, loops and parallel pairings retain their actual slot and occurrence multiplicities.

Follows(q,u,v,paths) means the slot list joins u to v with each next source equal to the preceding actual target. Define integer chi(s,i) as count(paths(s),i)-count(paths(s),J(i)), A(i)=sum_s w(s)chi(s,i), and W(z)=sum_s indicator(label(u(s))=z)w(s). localLift(i) has coefficient +1/2 on its opposite face edge, -1/2 on the other two face edges, and zero elsewhere. The SAME vector a(o)=sum_i A(i)localLift(i,o) is used in every conclusion.

Theorem 1.1 (Simple actual slot paths, component loads, conservation and the six-slot bound).

$$\forall T\in Type,S\in Type,K\in Type,q\in Pairing\left(T\right),u\in S\to Corner\left(T\right),v\in S\to Corner\left(T\right),w\in S\to K,B\in K,\left(Fintype\left(T\right)\wedge \left(Fintype\left(S\right)\wedge \left(Field\left(K\right)\wedge \left(LinearOrder\left(K\right)\wedge \left(IsStrictOrderedRing\left(K\right)\wedge \left(\left(\forall s\in S,label\left(q,u\left(s\right)\right)=label\left(q,v\left(s\right)\right)\right)\wedge \left(\left(\forall s\in S,0\le w\left(s\right)\right)\wedge \left(\forall z\in Vertex\left(q\right),mass\left(q,u,w,z\right)\le B\right)\right)\right)\right)\right)\right)\right)\right)\Rightarrow Transport\left(q,u,v,w,B\right)$$

Proof. Machine-checked in Lean as D5/S3/Geometry/Hyperideal/ActualCornerTransport.actual_corner_transport (✓ std3). ∎

Source. Repository-derived.

Commentary.

Transport(q,u,v,w,B) asserts the existence of these shared slot lists. They follow the actual pairing, have no repeated corner, and are empty when u(s)=v(s). Each slot count is at most one. chi is antisymmetric, has absolute value at most one, and vanishes outside the source component. Its corner divergence is exactly indicator(u(s)=c)-indicator(v(s)=c). A(J(i))=-A(i), |A(i)|<=W(label(b(i))), M(a,e)=0, -Q(a,c)=sum_s w(s)(indicator(u(s)=c)-indicator(v(s)=c)), and |a(o)|<=3B for every occurrence.

Mathlib supplies simple paths in the graph whose adjacency is an actual slot between distinct corners. A recursive lift selects actual slots for those steps, preserving parallel-slot witnesses. The signed counts telescope. Actual paired edge labels make M(localLift(J(i)))=M(localLift(i)); reindexing by J cancels the global edge sums. The local corner identity is Q(localLift(i))=-indicator(b(i)). Every local edge belongs to two faces with three slots each. All six half-coefficient contributions are counted before taking any quotient.

B>=0 is not a premise. An existing occurrence gives an actual slot whose nonnegative absolute load is bounded by B. If T is empty, all classes and occurrences are empty and any B is allowed. Empty S and zero weights are included. Taking B=sum_s w(s) gives the total-weight specialization. Instantiating K with the rationals gives a rational vector.

For component averaging, C(z) is the actual corner fiber, F(z)=card(C(z))>0 for every existing quotient class, and D(z)=sum_C(z) d(c). Index ALL ordered pairs in each fiber, including diagonal pairs, with w(z,u,v)=taud(v)/F(z), d>=0 and tau>=0. Their exact source mass is tauD(z). With D(z)<=Dmax the SAME construction has |A(i)|<=tauD(label(b(i))), |a(o)|<=3tauDmax, and -Q(a,c)=tau(D(label(c))/F(label(c))-d(c)). These are applications of the retained theorem, not additional retained mathematical declarations.

This linear transport theorem assumes no angle positivity, edge-degree bound, link-surface condition or common geometric length. It does not establish strictification, angle upper or lower bounds, arbitrary approximation, rational parameter selection, link topology or a geometric existence theorem.

References

• Truth anchor: D5/S3/Geometry/Hyperideal/ActualCornerTransport.actual_corner_transport