Keyboard shortcuts

Press ← or → to navigate between chapters

Press ? to show this help

Press Esc to hide this help

Original side traces, twenty-cell cover and null overlaps

Abstract

The original twenty closed coefficient cells cover the common six-length cut body and have pairwise null overlaps in its explicit three-coordinate chart.

Fix six strictly positive lengths in the original order 01, 02, 03, 23, 13, 12. For a side label k, the side support is the coordinate support x_k=0. The six cyclic supports are the alternating coordinate and Gram-row supports of the three remaining labels.

Theorem 1.1 (Two supporting traces recover the corresponding closed edge).

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

Source. Repository-derived.

Commentary.

The endpoint support classification identifies exactly two original ordered endpoints on the simultaneous zero trace. The common zero-trace convex-hull lemma then identifies the whole intersection with their convex hull, which is the displayed closed segment. The result concerns the original coefficient body and its original endpoint coordinates.

For the covering application use the original LengthGramSideTrace definitions vertices(l,n), cell(l,n) and boundaryTriangle(l,n), with n in Fin(20). Thus cell is the closed convex hull of the original four-tuple and boundaryTriangle is the closed convex hull of its final three entries. The affine carrier is sum_i x_i=1. The body K=cutBody(l) is cut out by the eight original linear supports L_f(x)<=0: four coordinate supports -x_i and four rows of lengthGram(l). All six lengths are strictly positive; no determinant or Delta condition is needed for this coefficient-space statement.

Here is the finite supporting-ray certificate used twice. For distinct o,x in K let J be the supports with L_f(o)<0 and set t=max_{f in J} L_f(x-o)/(-L_f(o)). There is a coordinate q with x_q<o_q: otherwise nonnegative coordinate differences and the common sum one force x=o. Since x_q>=0, this coordinate gives o_q>0 and a strictly positive ratio in J. The inequalities at x give every ratio at most one, so 0<t<=1. Put z=o+(x-o)/t. Its coordinate sum remains one. For a support in J, maximality gives L_f(z)<=0; for a support outside J, L_f(o)=0 and L_f(z)=L_f(x)/t<=0. A maximizing support vanishes at z and is strictly negative at o. Finally x=(1-t)o+t z, so x lies on the closed segment from o to z. The case x=o is handled directly, without division by t.

The cap exit is supplied by D5/S3/Geometry/Hyperideal/CapTraceHull.cap_trace_hull. Its exact endpoint range is the three final vertices of capIndex(i), so a zero Gram-row support puts z in that original cap boundary triangle. The simultaneous zero trace of coordinate support k and Gram-row support k is empty: D5/S3/Geometry/Hyperideal/ZeroTraceHull.zero_trace_hull selects endpoints whose first label is k and whose two labels both differ from k, an impossible incidence condition. This excludes that exit without adding a diagonal-disjointness premise.

For a side k, take the original root o=sideCycle(l,k,0) and apply the same certificate within x_k=0. The interpolation formula preserves this coordinate. The supports strictly negative at o are the four cycleSupport(k,r) with r=1,2,3,4, together with Gram row k. The last cannot vanish on this side by the preceding empty-trace argument. The existing cycle_edge_hull therefore puts z on the exact closed segment from sideCycle(l,k,r) to sideCycle(l,k,r+1), for some r in {1,2,3,4}. Consequently x belongs to the convex hull of the original root and those two original consecutive vertices. This hull is exactly boundaryTriangle(l,sideIndex(k,r-1)). The root itself belongs to the first such triangle. These four specified triangles cover the whole side; cyclic convexity or fan coverage is not an extra premise.

The original barycenter b=(1/4,1/4,1/4,1/4) belongs to K by LengthGramBody.shared_radial_body. Apply the certificate with o=b. Every exit point lies either on a cap triangle or on one of the four specified triangles of a side. The original tuple identity gives cell(l,n)=convexJoin R {b} (boundaryTriangle(l,n)), using convexHull_insert. Hence every x in K belongs to one of the literal twenty cells. Conversely the barycenter and every endpoint belong to K, and K is convex by the existing twelve-endpoint hull equality, so each cell is contained in K. Thus cutBody(l) is exactly the union over n in Fin(20) of cell(l,n), for every six strictly positive original lengths.

For the overlap application retain these same original twenty tuples and all six strictly positive lengths. No determinant assumption or simplex nondegeneracy is added. Write each point of a cell as a normalized sum of its four vertices with nonnegative coefficients. Two representations with every coefficient strictly positive cannot agree when the cell indices differ. The coefficient argument uses the original eight supports and endpoint incidences, so it does not infer disjointness from a sketch of the fan.

First suppose the two boundary triangles have different facet supports. Each facet vanishes on its own three endpoints and is strictly negative at the common barycenter. It is nonpositive on every endpoint of the other triangle, and the original endpoint-incidence table gives a strictly negative value on at least one of them. Applying that facet to equal positive combinations forces the first barycenter coefficient to be strictly larger than the second. Applying the other facet forces the reverse strict inequality, a contradiction.

If the facet supports agree, evaluating that support first makes the barycenter coefficients equal. Remove the common barycenter contribution. Distinct cells on this facet are two of the four specified side triangles, with the same original root. For each triangle its original ridge support vanishes on its two opposite-edge endpoints and is strictly negative at the root. On the other triangle that support is nonpositive, with at least one strictly negative opposite-edge endpoint. Applying the two ridge supports now forces opposite strict inequalities between the root coefficients. The original facet, ridge and endpoint tables include all twenty indices; a cap facet has only its one triangle.

It follows that every point in the intersection of two distinct closed cells has a zero coefficient in at least one of its two nonnegative normalized representations. Deleting that zero coefficient leaves the convex hull of the other three original vertices. Thus the intersection is contained in the union of the four triangular face hulls of each of the two cells. The argument needs neither affine independence nor an orientation of either four-tuple.

Use the coordinate chart on the common sum-one affine space given by dropping the fourth coordinate: pi(x)=(x_0,x_1,x_2). Its inverse is chi(y)=(y_0,y_1,y_2,1-y_0-y_1-y_2). The original vertices belong to cutBody(l), and convexity of the sum-one affine space puts every cell in that space. Hence pi is injective on all these cells, and pi(cell_n) intersect pi(cell_m) equals pi(cell_n intersect cell_m). This equality is required: an image of an intersection cannot by itself stand for an intersection of images.

For nondegeneracy retain every original ordered tuple p_j=vertices(l,n,j), with all six original lengths strictly positive. The supporting-flag criterion is elementary: suppose linear forms L,R satisfy L(p_0) different from zero, L(p_1)=L(p_2)=L(p_3)=0, R(p_1) different from zero, R(p_2)=R(p_3)=0, and p_2 different from p_3. In a relation sum_j w_j p_j=0 with sum_j w_j=0, applying L first gives w_0=0 and applying R next gives w_1=0. The weight sum gives w_3=-w_2, so the vector relation becomes w_2(p_2-p_3)=0. The distinct last two vertices force w_2=w_3=0. This is the finite weighted-vsub criterion for affine independence.

Apply this criterion to each of the literal twenty rows, using L=support(l,facet(n)) and R=support(l,ridge(n)). The first vertex is always b=(1/4,1/4,1/4,1/4). LengthGramBody.shared_radial_body supplies strict negativity of every Gram-row support at b, while each coordinate support equals -1/4 there. The endpoint classification in LengthGramPolytope.cut_body_polytope supplies exactly the zero and strictly negative entries required by the facet and ridge tables. It also makes the original ordered endpoint map injective; the final two endpoint labels in every row differ. Thus every one of the twenty original four-tuples is affinely independent in the coefficient space. No Gram determinant, Delta condition, independently postulated fan, or nondegeneracy hypothesis is used.

Use the same sum-one chart pi(x)=(x_0,x_1,x_2) and affine inverse chi(y)=(y_0,y_1,y_2,1-y_0-y_1-y_2). The existing body results put every original vertex in the sum-one carrier, so chi(pi(p_j))=p_j. Affine independence of the original tuple therefore implies affine independence of its three-coordinate image. In particular the actual 3 by 3 edge matrix B(l,n), whose column j is pi(vertices(l,n,j+1))-pi(vertices(l,n,0)) for j=0,1,2, has linearly independent columns and det B(l,n) different from zero, for each n in Fin(20). The matrix uses the original row order and the explicit coordinate chart, rather than an unspecified orientation convention.

The actual ordered edge determinants have signs (+,-,+,-; -,-,-,-; +,+,+,+; -,-,-,-; +,+,+,+) in the original twenty-row order. For each row n let s_n be this sign. Expanding the literal endpoint coordinates by Matrix.det_fin_three gives s_n det B(l,n)>0 for all six positive lengths, since cosh(l_k)>1. Thus |det B(l,n)|=s_n det B(l,n), and a time-dependent positive-length family retains the same orientation for every row. For the three reference faces through the first vertex, use outward reference normals nu_i=-e_i and the actual coefficient C_i=|det B| B^(-T) nu_i. The adjugate and cross-product identities give C_i=s_n A_i, where (A_0,A_1,A_2)=(-B_1 cross B_2, B_0 cross B_2, -B_0 cross B_1). Their orientation is fixed by C_i dot B_i=-|det B| and, more generally, C_i dot (B u)=-|det B| u_i<=0 when u_i>=0. These coefficients belong to the specified coordinate parametrization; an identification with geometric surface measure still requires its own measure argument. Exact whole-cell intersections, geometric surface measure, paired field flux, measured native-volume variation and the Schlaefli identity remain separate obligations. The determinant expansion, sign normalization and cofactor formulas apply existing algebraic results to the original tuples; no new standalone mathematical declaration or literature priority is asserted.

The internal triangle pairing keeps the literal twenty tuples and uses face occurrence (n,i), with n in Fin(20) and i in Fin(3), for the face containing the barycenter and omitting original vertex i+1. Let v(n,i)=(b,p,q) be its retained three vertices, in their original relative order. The thirty pairs are (0,2)-(19,1); (0,1)-(15,1); (12,2)-(16,2); (16,1)-(17,2); (12,1)-(13,2); (18,1)-(19,2); (17,1)-(18,2); (14,1)-(15,2); (13,1)-(14,2); (0,0)-(11,1); (8,2)-(19,0); (8,1)-(9,2); (10,1)-(11,2); (9,1)-(10,2); (11,0)-(15,0); (1,2)-(16,0); (1,1)-(12,0); (1,0)-(7,1); (4,2)-(17,0); (4,1)-(5,2); (6,1)-(7,2); (5,1)-(6,2); (7,0)-(13,0); (2,2)-(18,0); (2,1)-(8,0); (2,0)-(4,0); (5,0)-(9,0); (3,2)-(14,0); (3,1)-(10,0); (3,0)-(6,0). Their sixty occurrences are exactly Fin(20) times Fin(3), each used once. They give thirty unordered labelled three-vertex sets, each represented by two occurrences; the exterior face opposite the barycenter is outside this pairing.

Each pair fixes b and either keeps or exchanges its other two original endpoints. With F_(n,i)(s,t)=b+s(p-b)+t(q-b), the paired affine maps agree under (s,t) or (t,s), as specified by that endpoint order. The exchange preserves the full closed parameter triangle s>=0, t>=0, s+t<=1. Thus the paired three-vertex convex hulls are equal, with the actual point correspondence fixed. This identifies the specified shared triangles; it does not by itself prove that the intersection of the two whole cells is exactly that triangle.

The same original outward coordinate coefficients C_(n,i)=|det B_n| B_n^(-T)(-e_i) are opposite in every listed pair. Indeed C_(n,i)=s_n times (-B_1 cross B_2, B_0 cross B_2, -B_0 cross B_1)i; the explicit endpoint correspondence and the fixed original signs cancel these vectors pair by pair. The occurrence bijection then gives sum_n sum_i C(n,i)=0 with all sixty occurrences retained. This vector identity is a coordinate coefficient statement. Flux cancellation for a varying field still needs its common point values, the compatible face integration and geometric surface-measure transfer; measured volume variation and the Schlaefli identity are not consequences of the coefficient sum alone.

For the native-volume application impose the original genuine-realization condition in addition to the six positive lengths: with c_k=cosh(l_k), FourCycleEnvelopes.cosine(c_0,c_1,c_2,c_3,c_4,c_5) lies strictly between -1 and 1. Use the same matrix M and continuous injective realization f:cutBody(l)->HyperbolicThreeSpace supplied by LengthGramBody.shared_radial_body, so lorentz(M_i,M_j)=lengthGram(l)_(i,j), det M>0 and range(f) is compact. Put S=pi(cutBody(l)), chi(z)=(z_0,z_1,z_2,1-z_0-z_1-z_2), u(z)=chi(z) M, r(z)=-lorentz(u(z),u(z)) and d(z)=u_3(z)-u_2(z). The original coordinate witness gives r(z)=-gramQuadratic(l,chi(z))>0, d(z)>0 and coordinates(f(chi(z)))=((u_0/d)+i(u_1/d),sqrt(r)/d). Thus the upper-half-space chart T(z)=(u_0/d,u_1/d,sqrt(r)/d) describes this same realization; its injectivity follows from that of f and the sum-one lift/drop inverse.

The chart derivative is computed from the displayed affine u, rather than assumed. Its determinant is det(DT)=det(M)/(sqrt(r) d^3), while -(det(lengthGram(l)))=(det M)^2. Multiplying the absolute Jacobian by the height density (T_2)^(-3) therefore gives rho_l(z)=sqrt(-det(lengthGram(l)))/(-gramQuadratic(l,chi(z)))^2. The real-triple to complex-height coordinate map preserves Lebesgue measure. For the measure normalization, let a be the three-dimensional Hausdorff measure of the standard orthonormal parallelepiped in the actual L2 ambient space Ambient(Complex). Haar uniqueness gives 0<a<infinity. The existing HyperbolicNormalizedDensity.raw_native_density identity, together with this same calibration, identifies the coordinate image of nu=a^(-1) times rawNativeMeasure with ambient Lebesgue measure restricted to positive height and weighted by height^(-3). No value a=1 is assumed.

Change of variables on the measurable set S now gives nu(range(f))=integral_S rho_l(z) dz. The set S is compact and the denominator stays strictly positive on it, so rho_l is continuous and integrable there. The exact original twenty-cell cover and the null-overlap statement below then give nu(range(f))=sum_(n in Fin(20)) integral_(pi(cell_n)) rho_l(z) dz, with finite value. Equivalently the nonnegative integral is the sum of the twenty extended nonnegative cell integrals and equals ENNReal.ofReal of the displayed real sum. These are applications of the existing realization, normalized-density, Haar, change-of-variables and finite-union integration results. They identify the calibrated native measure and establish finite volume for the original body; geometric surface measure, moving-domain variation and the Schlaefli identity remain separate obligations.

A linear map sends each three-vertex face hull to the convex hull of three points in R^3. Its affine span is proper, since its affine dimension is at most two; the existing Haar-measure theorem for a proper affine subspace makes that hull Lebesgue-null. The preceding finite union therefore proves that pi(cell_n) intersect pi(cell_m) has three-dimensional Lebesgue measure zero for every n different from m. This is a null-overlap statement in the explicit coefficient chart. Exact pairwise face descriptions, geometric surface measure, paired flux cancellation, volume variation and the Schlaefli identity require their separate arguments. These are applications of the existing support, convex-hull, affine-span and Haar-measure results; no new standalone mathematical declaration or literature priority is asserted.

References