Keyboard shortcuts

Press ← or → to navigate between chapters

Press ? to show this help

Press Esc to hide this help

One shared body from the actual length Gram matrix

Abstract

The common six-length cut body has a Lorentz and upper-half-space coordinate realization.

Let l be six positive real lengths in the order (01,02,03,23,13,12). The symmetric matrix G has diagonal entries one and off-diagonal entries minus cosh of the corresponding length. The set C consists of nonnegative four-coordinate vectors whose coordinates sum to one and whose four G-row values are nonpositive. Write q(v)=v-transpose G v, r(v)=v/sqrt(-q(v)), and b=(1/4,1/4,1/4,1/4). R6 and R4 denote real coordinate spaces. B is the Lorentz form with signs (+,+,+,-). The function phi01 is the original six-variable cosine formula applied to cosh(l). For a future unit timelike y, Psi(y) has horizontal coordinate (y0+i*y1)/(y3-y2) and height 1/(y3-y2). H3 denotes the repository’s HyperbolicThreeSpace with its actual metric topology.

Theorem 1.1 (Compactness, explicit frame and shared coordinate map).

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

Source. Repository-derived.

Commentary.

The barycenter strictly satisfies every cut. A cut equality at a positive coordinate forces that coordinate to exceed one half. If q vanished, every positive coordinate would require a cut equality. Two positive coordinates cannot both exceed one half, while a singleton support violates its own cut. Thus q is strictly negative throughout the same C.

The positive square-root denominator makes r continuous. The sum of the image coordinates recovers its reciprocal scale, so r is injective. Its image is compact and nonempty, and the quadratic value there equals minus one.

The strict condition on phi01 makes the final square root in the explicit four-vector frame positive. The frame’s Lorentz Gram is exactly G and its determinant is positive. Congruence with diag(1,1,1,-1) gives det(G)<0. Every point of the same radial body is future unit timelike. Its positive denominator y3-y2 defines Psi throughout C. The coordinate inverse proves injectivity, and the existing coordinate homeomorphism proves continuity into actual H3.

This closes the shared compact coordinate-body and frame step of the original six-length construction. It does not yet assert three-dimensional interior, complete triangular/hexagonal incidence, geodesic intervals, prescribed edge distances, dihedral angles or relabeling isometries. Those obligations retain the original all-six strict source cosine domain; one strict condition suffices for this frame step.

References