A cap support trace is an endpoint hull

Abstract

A coordinate support zero trace is the convex hull of the endpoints on that cap.

Fix a coordinate i in the six-length cut body. The zero trace of the support given by the i-th Gram row is exactly the convex hull of the endpoints whose ordered label starts at i.

Theorem 1.1 (The cap zero trace is generated by its three endpoints).

$$capTraceHull$$

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

Source. Repository-derived.

Commentary.

Every endpoint lies in the nonpositive support halfspace. The common-zero convex-hull theorem therefore reduces the trace to the endpoints where the support vanishes. The endpoint support classification identifies those precisely as the labels starting at i.

References

• Truth anchor: D5/S3/Geometry/Hyperideal/CapTraceHull.cap_trace_hull
• Dependency: D5/S3/Geometry/Hyperideal/LengthGramPolytope
• Dependency: D5/S3/Geometry/Hyperideal/ZeroTraceHull