Even middle-angle sums cannot close at 2*pi
Abstract
An even number of middle angles cannot sum to two pi.
Consider a finite family of real angles with even cardinality. If every angle lies strictly between pi/3 and pi/2, then the total cannot equal 2*pi.
Theorem 1.1 (Even middle angles cannot close).
Lean statement: D5/S3/Geometry/Hyperideal/EvenAngleSumObstruction.even_middle_angle_sum_ne_two_pi
Proof. Machine-checked in Lean as D5/S3/Geometry/Hyperideal/EvenAngleSumObstruction.even_middle_angle_sum_ne_two_pi (✓ std3). ∎
Source. Repository-derived.
Commentary.
For an empty family the sum is zero. For a nonempty family, write its even cardinality as twice k. If k is at most two, the strict upper bound pi/2 makes the total strictly less than 2pi. If k is at least three, the strict lower bound pi/3 makes the total strictly greater than 2pi.
This is the numerical angle-budget component of the low-face transport obstruction. It assumes the even-cardinality fact supplied by a separate face-pairing argument and does not itself construct the pairing, classify the six-length shape family, or prove a global geometric realization.
Application to one actual face-paired quotient and a common positive length field. Let T be a finite set of blocks and p a RawFacePairing on T. A local edge occurrence is (t,j) with j in Fin(6). Positions j=0,1,2,3,4,5 have endpoints 01,02,03,23,13,12, respectively.
The four faces, numbered by omitted vertex, have edge-slot lists: face 0: (3,4,5); face 1: (1,2,3); face 2: (0,2,4); face 3: (0,1,5).
Write P(t,j)=p.edgeLabel(t,j). The edge type E is p.GlobalEdge: the quotient of actual occurrences by the equivalence relation generated by p’s paired face-edge slots. In particular, if p.facePair(t,f)=(t’,f’) and m=p.faceMap(t,f)(n), then P(t,faceEdge(f,n)) = P(t’,faceEdge(f’,m)). (1)
Fix one field ell:E→R with ell(e)>0 for every e, and one common h>1. Put X(e)=cosh(ell(e)), x_t(j)=X(P(t,j)), alpha_t(j)=extendedAngle(x_t,j). Every x_t(j)>1. All local coordinates, low-face tests and angles below come from this same field and this same quotient. No independent angle assignment or independent numerical copy of an identified edge is allowed.
For each t choose a vertex permutation s_t:Fin(4)≃Fin(4), with direction NEW vertices to OLD vertices. It induces the permutation E_t of the six undirected edges by sending {a,b} to {s_t(a),s_t(b)}. This is a legal tetrahedral relabeling; an arbitrary permutation of six edge positions is not a substitute. Assume the following complete block data: for each t there exist r_t,u_t such that y_t(j) := x_t(E_t(j)) = (r_t,h,h,u_t,h,h)_j. (2)
For each block, at least one of the following two alternatives is required. The flat branch requires h<r_t, h<u_t and extendedAngle(y_t,0)=pi. The genuine branch requires 1+2h≤r_t, -1<rawCos(y_t,j)<1 for every j, and tan(arccos(cosine(r_t,h,h,u_t,h,h))/2)≤1/2. (3)
The witnesses r_t,u_t and the permutations s_t may differ from block to block. The tangent premise is imposed on the actual raw axis formula of the same vector in (2). In particular, it is not a premise that all middle angles are equal across blocks. Positivity of ell gives r_t,u_t>1, as well as the already imposed h>1.
Why legal relabeling preserves the actual data. Let C(x,y,z,o,v,w)=cosine(x,y,z,o,v,w), with numerator N=yz+vw+xyv+xzw-(x^2-1)o; its denominator is sqrt(rad(x,y,w))sqrt(rad(x,z,v)), where rad(a,b,c)=2abc+a^2+b^2+c^2-1.
The defining formula has the two symmetries C(x,y,z,o,v,w)=C(x,z,y,o,w,v), C(x,y,z,o,v,w)=C(x,w,v,o,z,y). (4)
For the first, the numerator is unchanged and the two denominator factors exchange. For the second, the numerator is unchanged and rad’s last two arguments interchange within each factor. These are polynomial identities and factor commutation; they require no strict angle hypothesis. They are precisely the changes obtained by interchanging the two remaining vertices or the two target-edge endpoints. Thus every legal vertex relabeling preserves rawCos at its corresponding actual edge. Applying the same clipping max(-1,min(c,1)) and arccos gives extendedAngle(y_t,j)=alpha_t(E_t(j)), Genuine(y_t) iff Genuine(x_t). (5) This also transports flat endpoint angles, where clipping is essential.
The same vertex map determines each face-slot change. For each new face f there is a permutation d(t,f) of Fin(3) satisfying faceEdge(s_t(f),d(t,f)(n))=E_t(faceEdge(f,n)). (6)
It is obtained by matching the explicit three-edge lists of that face; it is not an independently chosen incidence correspondence. On faces let A(t,f)=(t,s_t(f)), and on occurrences let B(t,j)=(t,E_t(j)). If normalized coordinates are used for the pairing as well, its face involution is p_s=inverse(A) composed with p.facePair composed with A. For a normalized face a=(t,f), write d(a)=d(t,f) and put a’=p_s(a). Its slot map is inverse(d(a’)) composed with p.faceMap(A(a)) composed with d(a).
Equation (6) identifies each generator of its paired-edge relation with the original generator under B, in both directions. Transporting equivalence closure therefore induces a quotient equivalence F:p_s.GlobalEdge≃E with F(P_s(t,j))=P(t,E_t(j)). (7)
The normalized field is exactly ell composed with F. Its occurrences over inverse(F)(e) correspond bijectively to original occurrences over e by B. Equation (5) identifies each summand, so the complete occurrence sums agree. One can therefore do all bookkeeping in normalized coordinates and return to the original quotient without changing the field, identifying extra edges or discarding multiplicity. The argument below is stated directly on the original quotient.
The local genuine and flat consequences. For a genuine block, omit the subscript t for this calculation and define Q=2h^2/(r-1), theta=arccos(cosine(r,h,h,u,h,h)).
The genuine premise gives 0<theta<pi. Since r-1≥2h>0, one has 0<Q≤h. Direct substitution into the existing numerator and rad formulas gives numerator(r,h,h,u,h,h)=(r+1)(2h^2-(r-1)u), rad(r,h,h)=(r+1)(r-1+2h^2), cos(theta)=(Q-u)/(Q+1). (8)
Here both radical factors for the axis are the same positive radical, so their product is rad(r,h,h). To check the hypotheses of the existing middle-angle window, write a=sin(theta/2)>0 and b=cos(theta/2)>0. The supplied tangent bound implies 2a≤b. Together with a^2+b^2=1 this gives cos(theta)=b^2-a^2≥3/5>0. Equation (8) then gives u<Q≤h. The half-angle identity also gives cot^2(theta/2)=(1+cos(theta))/(1-cos(theta)) =(2Q+1-u)/(u+1), Q-cot^2(theta/2)=(Q+1)(u-1)/(u+1)>0. (9)
Thus u<h<r, and every hypothesis of Section71AngleWindow.middle_angle_window is satisfied, including the strict cotangent condition. These computations keep the same r,h,u and the same actual theta throughout.
All four normalized middle positions j=1,2,4,5 have raw cosine C(h,h,r,h,h,u), so they share an angle beta within this block. Apply FourCycleAnisotropicMeanResponse.paired_angle_half_sum with (r,a,b,o)=(r,h,h,u). Its two transverse angles are both this beta, and its axis angle is theta. Write its coefficient as lambda=(sqrt(h^2-1)/h)*sqrt((r-1)/(r+1)). Then lambda^2=(h^2-1)/(Q+h^2).
Both lambda and sqrt((h^2-1)/(Q+h^2)) are nonnegative, so the half-sum formula becomes beta=arctan(sqrt((h^2-1)/(Q+h^2)) cot(theta/2)) =middleAngle(h,Q,theta). The existing middle_angle_window therefore gives pi/3<beta<pi/2. (10)
Restore subscripts: Q_t,theta_t and beta_t generally vary with t. What is uniform is the strict interval (10), not a common value of beta_t.
The genuine shape has precisely one coordinate below h, at j=3, and the faces containing it are precisely f=0 and f=1. These are the low faces, where “low” means the face contains at least one edge with value below h. The explicit face lists show that each middle occurrence lies in exactly one low face, at these exact slots: for j=1 the unique (f,n) is (1,0); for j=2 it is (1,1); for j=4 it is (0,1); for j=5 it is (0,2). (11)
This is the finite incidence specialization of EdgeStarTransitions’ existing localFlagEquiv. It is not an assertion that an edge has only one incident face: its other face is not low. The legal maps in (6) transfer (11) to the actual original faces and slots.
For a flat-branch block, every coordinate is at least h, with strict inequality at its two axes 0 and 3. There are no low faces. PositiveFlatClassification.positive_classification applies to this same positive vector. Its actual angle pi at position 0 places it in sector 0, and the classification gives angles pi at positions 0,3 and zero at positions 1,2,4,5. In particular the block is not Genuine, and every occurrence whose value equals h has angle zero. These are local consequences of the complete flat branch in (3); this argument does not remove the flat blocks.
The actual low-flag pairing and the occurrence bijection. Fix an original quotient edge e with X(e)=h. Let I_e be all occurrences (t,j) with P(t,j)=e. Let G_e be the subtype of I_e for which x_t is Genuine. Let L_e be the actual face-slot flags (t,f,n) such that the face (t,f) contains some m with x_t(faceEdge(f,m))<h, and P(t,faceEdge(f,n))=e. (12)
The selected slot n in (12) is an occurrence of e, hence has value h; it is not the slot witnessing the strict low value. This distinction is necessary for the count.
Define K on all actual flags by crossing the paired face: K(t,f,n)=(t’,f’,p.faceMap(t,f)(n)), where (t’,f’)=p.facePair(t,f).
Equation (1) preserves the selected label e. If a source face is low, transport its witnessing slot m through the same faceMap; equation (1) preserves that strict inequality too. Therefore K restricts to L_e. The involution and inverse-slot laws of RawFacePairing give K^2=id. A fixed flag would project to a fixed face of p.facePair, contrary to p.pairFixedFree. The restriction is consequently a fixed-point-free involution. Applying GlideCrossingParity.glide_crossing_count_even gives |L_e| is even. (13)
This is the source of low-slot parity. It uses neither ValidColoring nor global_edge_balance. In particular, a flat block has no low edges on any face, so it would not satisfy the condition that every face have one or two low edges required by that separate balance theorem.
The forgetful map (t,f,n) ↦ (t,faceEdge(f,n)) is a bijection L_e≃G_e. (14) For a flag in L_e, the local block cannot be a flat-branch block because such a block has no low face. It is therefore genuine. Its selected edge has value h; since r_t>h and u_t<h, its normalized position is one of 1,2,4,5. This proves that (14) has the claimed target. Conversely, every element of G_e has one of those four normalized middle positions and has exactly the one low-face flag supplied by (11), transferred by (6). That flag maps back to the original occurrence and still has label e. The same uniqueness proves injectivity. Thus |G_e|=|L_e| is even. (15)
Both fibers count actual occurrences and actual flags, not their distinct local labels. Several edges of the same block may have label e; each supplies its own occurrence and its own flag in (11). Faces of one block may be paired to other faces of that same block: the argument only requires the paired face itself to be different, as stipulated by p.pairFixedFree. Repeated quotient labels and these self-pairings do not require a separate simplicity assumption.
The full actual angle sum and nonemptiness. For o=(t,j) in G_e, equation (5) and the local calculation give alpha_t(j)=beta_t in (pi/3,pi/2). Apply the existing even_middle_angle_sum_ne_two_pi to the finite family indexed by G_e, using (15). This gives: the sum of alpha_t(j) over (t,j) in G_e differs from 2*pi. (16)
No equality between different beta_t is used: the theorem accepts a distinct angle for every member of an even finite index type. For completeness, if |G_e|=2k and k≤2, the strict upper bound makes a nonempty sum less than 2pi; the empty sum is zero. If k≥3, the strict lower bound makes the sum greater than 2pi.
Every occurrence of I_e outside G_e lies in a flat-branch block, because the two alternatives exhaust the assumed block data. It has value X(e)=h, so the flat calculation makes its actual extended angle zero. Splitting the finite occurrence sum gives: the sum of alpha_t(j) over I_e equals the sum over G_e plus zero, and consequently differs from 2*pi. (17)
The sum in (17) retains all original occurrences over e, including repeated local labels and flat occurrences. Only the values of the latter summands are zero; they are not removed from the indexing type by a change of geometry.
The edge-specific conclusion (15),(17) holds for every e with X(e)=h. If T is nonempty, choose any block t and its normalized middle index 1. Set e=P(t,E_t(1)); then X(e)=y_t(1)=h. Equation (17) for this edge contradicts the assertion that every original global edge has full occurrence sum 2*pi. Without nonemptiness, no such edge is supplied; the empty system would satisfy that universal assertion vacuously.
Scope of the application. The conclusion is conditional on one actual quotient E, one positive ell on E, the common h, and all the shape and branch premises (2),(3). It does not prove those premises from a more general geometric problem. Flat-branch blocks remain allowed and contribute zero at the selected h-valued occurrences; the application does not establish general flat elimination. The repeated transverse values (r_t,h,h,u_t,h,h) are essential to the local parameter substitution and the four-slot calculation. The full neighborhood argument below treats six independent variables. The paired-shape argument is combinatorial and analytic on RawFacePairing; identifying it with a particular manifold, its actual normal-circle traversal or a common geometric realization remains a separate obligation.
Uniform stability with six independent coordinates. Use the fixed vectors F0=(22,10,10,22,10,10) and G0=(22,10,10,s,10,10), where s=(579-221sqrt(5))/84 and 1<s<2. There is a single epsilon>0 with the following property. For every finite nonempty block set T, every actual RawFacePairing p, every choice of legal new-to-old vertex permutations s_t, and every common positive length field ell on the original E=p.GlobalEdge, suppose each normalized six-vector y_t(j)=cosh(ell(P(t,E_t(j)))) lies coordinatewise within epsilon of either F0 or G0. Then the complete original edge-occurrence angle sums cannot all equal 2pi. Each coordinate may vary independently within these bounds.
The local margins are explicit. At F0, rawCos is -262/221 at the two axes 0,3 and 230/221 at the four middle positions. For G(u)=(22,10,10,u,10,10), 1<u<2, the two axis raw cosines are (4600-483u)/5083 and (222-22u)/(u+199). Both lie in (0,1). For a middle position the numerator is N=230*(u+1), and the radical arguments are L=(u+1)(u+199), R=5083. They are positive and satisfy LR/4-N^2=(u+1)(799917-206517u)/4>0. Thus the actual middle raw cosine N/(sqrt(L)*sqrt(R)) lies in (0,1/2). Taking u=s certifies the center G0 using the original cosine formula.
For a six-vector whose entries all exceed 1, every radical argument is positive, so each original raw-cosine function is continuous there. Intersect the finitely many open coordinate and raw-cosine conditions at each center. Shrink to coordinatewise balls and take the smaller positive radius. This constructs epsilon before any T, pairing, relabeling or length field is chosen. Near F0 the two axes lie in (21,23), the four middle values in (9,11), and rawCos at axis 0 is less than -1. The positive flat classification then gives actual extended angles pi at both axes and zero at all middle positions.
Near G0, axis 0 lies in (21,23), axis 3 in (1,2), and the four middle values in (9,11). Every original raw cosine lies strictly in (-1,1), so the block is genuine. The four middle raw cosines lie in (0,1/2); the original clipped-arccos definition consequently places each corresponding actual angle strictly in (pi/3,pi/2). These profile and angle conclusions follow from coordinatewise closeness. Middle values and middle angles may differ both within one block and between different blocks.
Choose the low-face threshold 9 for this neighborhood argument. On either permitted profile, a local value is below 9 exactly when it belongs to the short interval (1,2). The F profile has no low face. In the G profile only edge position 3 is short, so exactly faces 0 and 1 are low. For any original edge e with 9<X(e)<11, every occurrence over e is a middle position in its normalized block. A genuine such occurrence has exactly the one low-face slot listed in (11); an F-profile occurrence has no low-face slot.
Use the original face-crossing involution with the threshold 9. It preserves the common global value at the selected slot and transports a separate short-slot witness on the same face. Its restriction to low-face flags over e is fixed-point-free, so their number is even. Forgetting the low face gives a bijection to the genuine occurrences over e: the preceding unique-slot table supplies its inverse and proves injectivity. This argument uses interval membership for the selected middle edge, so no equality among its neighboring middle coordinates is required.
Every genuine occurrence over this e has angle in (pi/3,pi/2), while every remaining occurrence has actual angle zero by the F-profile classification. The even-middle-angle theorem therefore excludes a full occurrence sum of 2*pi. The legal vertex-induced face-slot maps, equivalence-closure transport and angle-sum transport in (4)-(7) return this statement to the same original quotient and length field. Repeated local labels and different-face self-pairings retain their full occurrence multiplicities.
Finally, nonemptiness supplies a block and its normalized middle position 1. Its original edge has X(e) in (9,11), so that edge contradicts universal closure. This proves the uniform perturbative obstruction under the displayed coordinate-neighborhood hypotheses. It does not identify the face-paired quotient with a prescribed manifold or establish general flat elimination beyond these profiles.