Keyboard shortcuts

Press ← or → to navigate between chapters

Press ? to show this help

Press Esc to hide this help

Mordell Cubic Orbit Independence

Abstract

Horizontal cubic rotations isolate coefficients in Mordell point relations.

Theorem 1.1 (Cubic orbit coefficient elimination).

Lean statement: D5/S3/Factorization/Mordell/GoldenCubicBlockOrbitIndependence.cubic_orbit_independent_mod_fixed

Proof. Machine-checked in Lean as D5/S3/Factorization/Mordell/GoldenCubicBlockOrbitIndependence.cubic_orbit_independent_mod_fixed (✓ std3). ∎

Source. Repository-derived.

Commentary.

Independent coordinate actions and the cubic trace reduce a base-field relation to a positive quadratic norm annihilating one non-torsion point; both integer coefficients vanish.

Theorem 1.2 (Cubic orbit independence modulo base points).

Lean statement: D5/S3/Factorization/Mordell/GoldenCubicBlockOrbitIndependence.cubic_mordell_family_independent_mod_base

Proof. Machine-checked in Lean as D5/S3/Factorization/Mordell/GoldenCubicBlockOrbitIndependence.cubic_mordell_family_independent_mod_base (✓ std3). ∎

Source. Repository-derived.

Commentary.

For a Mordell curve carrying non-torsion points on independently rotated cubic coordinates, each original point and its cubic rotation are independent modulo the base-field point group. The proof uses the horizontal three-point relation and an integral quadratic norm.

References