Exact nonlinear flat criterion

Abstract

The exact nonlinear correction separates the flat boundary from the symmetric transverse case.

Use the six independent positive coordinates in the order (r,a,b,o,c,d). Set A=rad(r,a,d), B=rad(r,b,c), C=r^2-1+(a-d)(c-b)+2(r+1)sqrt(abcd), S=sqrt(ac)+sqrt(bd), and J=(sqrt(AB)-C)/(r+1). The auxiliary C is the inner product of the two explicit three-dimensional vectors used in the Cauchy bound.

The correction J is nonnegative. The original cosine is at most -1 exactly when the opposite product (r-1)(o-1) reaches S^2+J. Equality J=0 occurs exactly on the opposite-pair symmetry a=c and b=d; there the criterion reduces to (r-1)(o-1)>=(a+b)^2.

Theorem 1.1 (Nonnegative nonlinear correction).

$\forall r \in R e a l, a \in R e a l, b \in R e a l, c \in R e a l, d \in R e a l, ((((1 < r \land 1 < a) \land 1 < b) \land 1 < c) \land 1 < d) \Rightarrow 0 \leq J (r, a, b, c, d)$

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

Source. Repository-derived.

Commentary.

Finite Cauchy-Schwarz applied to the explicit three-coordinate vectors proves C<=sqrt(AB), and the positive factor r+1 preserves the inequality.

Theorem 1.2 (Exact flat iff).

$\forall r \in R e a l, a \in R e a l, b \in R e a l, o \in R e a l, c \in R e a l, d \in R e a l, (((((1 < r \land 1 < a) \land 1 < b) \land 1 < o) \land 1 < c) \land 1 < d) \Rightarrow (cos in e (r, a, b, o, c, d) \leq - 1 \Leftrightarrow (r - 1) \cdot (o - 1) \geq S (a, b, c, d)^{2} + J (r, a, b, c, d))$

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

Source. Repository-derived.

Commentary.

Expanding numerator+C gives (r+1)(S^2-(r-1)(o-1)); replacing sqrt(AB) by C+(r+1)J and using the positive denominator yields the iff.

Theorem 1.3 (Equality characterization).

$\forall r \in R e a l, a \in R e a l, b \in R e a l, c \in R e a l, d \in R e a l, ((((1 < r \land 1 < a) \land 1 < b) \land 1 < c) \land 1 < d) \Rightarrow (J (r, a, b, c, d) = 0 \Leftrightarrow (a = c \land b = d))$

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

Source. Repository-derived.

Commentary.

The Gram determinant is a sum of three squares. Its vanishing forces equality of the two vector coordinates and then a=c and b=d; the converse follows by direct substitution.

Theorem 1.4 (Symmetric transverse reduction).

$\forall r \in R e a l, a \in R e a l, b \in R e a l, o \in R e a l, (((1 < r \land 1 < a) \land 1 < b) \land 1 < o) \Rightarrow (cos in e (r, a, b, o, a, b) \leq - 1 \Leftrightarrow (r - 1) \cdot (o - 1) \geq (a + b)^{2})$

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

Source. Repository-derived.

Commentary.

When c=a and d=b, the square-root terms reduce to a and b and the equality characterization gives J=0, yielding the sharp reduced product test.

References

Truth anchor: D5/S3/Geometry/Hyperideal/FlatNonlinearCriterion.J_eq_zero_iff
Truth anchor: D5/S3/Geometry/Hyperideal/FlatNonlinearCriterion.J_nonneg
Truth anchor: D5/S3/Geometry/Hyperideal/FlatNonlinearCriterion.cosine_le_neg_one_iff
Truth anchor: D5/S3/Geometry/Hyperideal/FlatNonlinearCriterion.symmetric_cosine_le_neg_one_iff
Dependency: D5/S3/Geometry/Hyperideal/FourCycleEnvelopes

Keyboard shortcuts

trureturing — Discovering truth

Exact nonlinear flat criterion

Abstract

References