TauLib.Coordinates.Descent

Remainder descent and prime stratum descent for greedy peel.

Registry Cross-References

• [I.L04] Remainder Descent — div_lt_of_ge_two, descent checks

Ground Truth Sources

• chunk_0241_M002280: Remainder descent D < X, prime stratum descent

Mathematical Content

When X ≥ 2, the greedy peel extracts T(A,B,C) with T ≥ 2. Since D = X / T and T ∣ X, we have D < X (strict descent).

Additionally, the largest prime of D is strictly less than A (prime stratum descent). This ensures the spine terminates with strictly decreasing primes.

Tau.Coordinates.div_lt_of_ge_two

source **theorem Tau.Coordinates.div_lt_of_ge_two {x d : Nat}

(hx : x ≥ 1)

(hd : d ≥ 2)

(_hdvd : d ∣ x) :x / d < x**

If d ≥ 2 divides x and x ≥ 1, then x / d < x.

Tau.Coordinates.lt_mul_of_ge_two

source **theorem Tau.Coordinates.lt_mul_of_ge_two {a b : Nat}

(ha : a ≥ 2)

(hb : b ≥ 1) :b < a * b**

A product a * b with a ≥ 2 is strictly larger than b (when b ≥ 1).

Tau.Coordinates.descent_check

source def Tau.Coordinates.descent_check (x : Denotation.TauIdx) :Bool

[I.L04] Check that greedy_peel remainder D < X for X ≥ 2. Also checks T(A,B,C) * D = X (reconstruction). Equations

• One or more equations did not get rendered due to their size. Instances For

Tau.Coordinates.prime_stratum_descent_check

source def Tau.Coordinates.prime_stratum_descent_check (x : Denotation.TauIdx) :Bool

Check that the largest prime of D is strictly less than A. Equations

• One or more equations did not get rendered due to their size. Instances For

Tau.Coordinates.full_descent_check

source def Tau.Coordinates.full_descent_check (x : Denotation.TauIdx) :Bool

Combined descent: remainder descent + prime stratum descent. Equations

• Tau.Coordinates.full_descent_check x = (Tau.Coordinates.descent_check x && Tau.Coordinates.prime_stratum_descent_check x) Instances For

Tau.Coordinates.verify_descent_up_to_go

source@[irreducible]

def Tau.Coordinates.verify_descent_up_to_go (i n fuel : Nat) :Bool

Verify descent for all X from 2 to n. Equations

• One or more equations did not get rendered due to their size. Instances For

Tau.Coordinates.verify_descent_up_to

source def Tau.Coordinates.verify_descent_up_to (n : Denotation.TauIdx) :Bool

Equations

• Tau.Coordinates.verify_descent_up_to n = Tau.Coordinates.verify_descent_up_to_go 2 n n Instances For