Positive generalized lengths and flat sectors
Abstract
The entire positive six-coordinate domain has precisely the native genuine or closed flat angle patterns.
The six coordinates vary independently over the open interval (1,infinity), in the original order (12,13,14,34,24,23). Write phi(x,q)=TwoLengthAngleSum.rawCos(x,q) and alpha(x,q)=TwoLengthAngleSum.extendedAngle(x,q). The latter is arccos(max(-1,min(phi(x,q),1))). Both functions use FourCycleCurvature.frame and FourCycleEnvelopes.cosine. No upper coordinate bound, paired transverse lengths, coloring or symmetry is assumed.
Genuine(x) means -1<phi(x,q)<1 at all six positions. For k in Fin(3), first(k)=k and second(k)=k+3 in Fin(6). Sector(x,k) means phi(x,first(k))<=-1. These are the three opposite pairs. The equality fibers phi=-1 and phi=1 are included in the flat patterns.
Theorem 1.1 (Complete native classification).
Proof. Machine-checked in Lean as D5/S3/Geometry/Hyperideal/PositiveFlatClassification.positive_classification (✓ std3). ∎
Source. Repository-derived.
Commentary.
The common polynomial delta satisfies rawNum(x,q)^2-leftRad(x,q)rightRad(x,q)=(x(q)^2-1)delta(x) for every original frame. Positive radicands fix the square-root branches. Negative delta puts all raw values strictly inside (-1,1). For nonnegative delta, the cofactor triangle identity forces a negative numerator. Such a numerator forces its opposite coordinate product to dominate the other two opposite products, making the four adjacent numerators positive. A second cofactor triangle identity then makes the opposite numerator negative. The common square-gap identity places exactly that opposite pair at or below -1 and the other four values at or above 1. Clipping and the principal arccos endpoint laws give the stated complete angle pattern. The selected sector is unique.
The classification is an analytic statement about the original formula. It does not construct a hyperideal polyhedron or assert existence of a common zero-curvature global length. The positive-domain and closed-sector conclusions are those required from the length theory attributed in CFMP_GEOMETRIC_REALIZATION.md Sections 50 and 64 to Luo-Yang, arXiv:1404.5365v2, Propositions 4.4-4.5 and Lemma 4.6. The Lean proof establishes the formula statement directly; the attribution is not an imported proof.
Theorem 1.2 (Strict local logarithmic budget).
Proof. Machine-checked in Lean as D5/S3/Geometry/Hyperideal/PositiveFlatClassification.native_flat_budget (✓ std3). ∎
Source. Repository-derived.
Commentary.
Let R=r^2-1, A=rad(r,a,d), B=rad(r,b,c). Apply finite Cauchy-Schwarz to U=(sqrt(R),a-d,sqrt(2(r+1)ad)) and V=(sqrt(R),c-b,sqrt(2(r+1)bc)). Their squared norms are A and B, and their inner product is R+(a-d)(c-b)+2(r+1)sqrt(abcd). Thus this inner product is at most sqrt(A)sqrt(B). Combining this bound with the original negative-cosine inequality gives (r-1)(o-1)>=ac+bd+2sqrt(abcd)>=4sqrt(abcd). Squaring nonnegative sides gives (r-1)^2(o-1)^2>=16abcd. Positive logarithm arguments and the exact product, quotient and power laws give the displayed budget. Both correction logarithms are strictly positive. The inclusive flat boundary remains in scope. No sharpness-at-infinity or equality characterization is asserted.