Theta Arithmetic

Paper source: the period equality in cor:evenlyMarkedKGT and the gcd calculation preceding eq:multDiffMarkedPts.

The arithmetic in this file is deliberately independent of the divisor-rank and transmission APIs. It isolates the number-theoretic content of the evenly-marked condition.

theorem Bananas.nat_div_gcd_pos_of_pos {a i : ℕ} (ha : 0 < a) (_hi : 0 < i) : 0 < a / a.gcd i

A positive length divided by the gcd with a positive interior coordinate is positive.

theorem Bananas.nat_mul_eq_div_mul_add_mod (m n d : ℕ) : m * n = m * n / d * d + m * n % d

The Euclidean decomposition used by the theta multiple calculation.

theorem Bananas.nat_mul_mod_lt_of_pos (m n d : ℕ) (hd : 0 < d) : m * n % d < d

The remainder in the preceding decomposition is strictly below a positive modulus.

theorem Bananas.nat_gcd_quotient_eq_of_cross_mul {a b i j : ℕ} (ha : 0 < a) (hb : 0 < b) (_hi : 0 < i) (_hj : 0 < j) (hcross : i * b = j * a) : a / a.gcd i = b / b.gcd j

If two positive pairs represent the same positive rational ratio, their lengths have the same quotient after each pair is reduced by its gcd.

theorem Bananas.evenlyMarkedTheta_k_pos (B : Banana 2) (α β : Fin 3) (i : Utilities.Certificate.SubdivisionGraph.Spec.PathPosition B α) (j : Utilities.Certificate.SubdivisionGraph.Spec.PathPosition B β) (hEven : EvenlyMarkedTheta B α β i j) : 0 < B.length α / (B.length α).gcd ↑i

The gcd quotient in the paper's period formula is positive for an evenly marked theta.

theorem Bananas.evenlyMarkedTheta_gcd_quotients_eq (B : Banana 2) (α β : Fin 3) (i : Utilities.Certificate.SubdivisionGraph.Spec.PathPosition B α) (j : Utilities.Certificate.SubdivisionGraph.Spec.PathPosition B β) (hEven : EvenlyMarkedTheta B α β i j) : B.length α / (B.length α).gcd ↑i = B.length β / (B.length β).gcd ↑j

The two candidate gcd periods agree under the evenly-marked ratio.

The reduced numerator is the common multiplier of the endpoint relation. This is the companion arithmetic identity needed when the one-strand prefix theorem is scaled to an evenly marked pair.

theorem Bananas.evenlyMarkedTheta_reduced_coordinates_eq (B : Banana 2) (α β : Fin 3) (i : Utilities.Certificate.SubdivisionGraph.Spec.PathPosition B α) (j : Utilities.Certificate.SubdivisionGraph.Spec.PathPosition B β) (hEven : EvenlyMarkedTheta B α β i j) : ↑i / (B.length α).gcd ↑i = ↑j / (B.length β).gcd ↑j

Quotients and residues of evenly-marked multiples

The following lemmas make explicit a step that is implicit in the paper's residue calculation: every multiple of the two marked coordinates crosses the two right endpoints the same number of times. Below the gcd period, neither residue is zero and multiplication by either marked coordinate is injective modulo its strand length.

theorem Bananas.nat_mul_div_eq_of_cross_mul {a b i j m : ℕ} (ha : 0 < a) (hb : 0 < b) (hi : 0 < i) (hj : 0 < j) (hcross : i * b = j * a) : m * i / a = m * j / b

Equal positive rational ratios have equal floor quotients after both numerators are multiplied by the same natural number.

theorem Bananas.nat_mul_mod_injective_below_gcd_quotient {a i m n : ℕ} (ha : 0 < a) (hm : m < a / a.gcd i) (hn : n < a / a.gcd i) (hmod : m * i % a = n * i % a) : m = n

Multiplication by i modulo a is injective on the fundamental range 0, ..., a / gcd a i - 1.

theorem Bananas.nat_mul_mod_ne_zero_below_gcd_quotient {a i m : ℕ} (ha : 0 < a) (hm0 : 0 < m) (hmk : m < a / a.gcd i) : m * i % a ≠ 0

A nonzero multiplier strictly below the gcd quotient has nonzero residue.

theorem Bananas.evenlyMarkedTheta_common_quotient (B : Banana 2) (α β : Fin 3) (i : Utilities.Certificate.SubdivisionGraph.Spec.PathPosition B α) (j : Utilities.Certificate.SubdivisionGraph.Spec.PathPosition B β) (hEven : EvenlyMarkedTheta B α β i j) (m : ℕ) : m * ↑i / B.length α = m * ↑j / B.length β

Evenly-marked multiples have a common endpoint-crossing quotient.

theorem Bananas.evenlyMarkedTheta_mul_residue_decompositions (B : Banana 2) (α β : Fin 3) (i : Utilities.Certificate.SubdivisionGraph.Spec.PathPosition B α) (j : Utilities.Certificate.SubdivisionGraph.Spec.PathPosition B β) (hEven : EvenlyMarkedTheta B α β i j) (m : ℕ) : m * ↑i = m * ↑i / B.length α * B.length α + m * ↑i % B.length α ∧ m * ↑j = m * ↑i / B.length α * B.length β + m * ↑j % B.length β

Euclidean decompositions of the two marked multiples use the same quotient.

theorem Bananas.evenlyMarkedTheta_alpha_residue_injective (B : Banana 2) (α β : Fin 3) (i : Utilities.Certificate.SubdivisionGraph.Spec.PathPosition B α) (j : Utilities.Certificate.SubdivisionGraph.Spec.PathPosition B β) (_hEven : EvenlyMarkedTheta B α β i j) {m n : ℕ} (hm : m < B.length α / (B.length α).gcd ↑i) (hn : n < B.length α / (B.length α).gcd ↑i) (hres : m * ↑i % B.length α = n * ↑i % B.length α) : m = n

The first residue coordinate is injective throughout one gcd period.

theorem Bananas.evenlyMarkedTheta_beta_residue_injective (B : Banana 2) (α β : Fin 3) (i : Utilities.Certificate.SubdivisionGraph.Spec.PathPosition B α) (j : Utilities.Certificate.SubdivisionGraph.Spec.PathPosition B β) (hEven : EvenlyMarkedTheta B α β i j) {m n : ℕ} (hm : m < B.length α / (B.length α).gcd ↑i) (hn : n < B.length α / (B.length α).gcd ↑i) (hres : m * ↑j % B.length β = n * ↑j % B.length β) : m = n

The second residue coordinate is injective throughout the same period.

theorem Bananas.evenlyMarkedTheta_residues_ne_zero (B : Banana 2) (α β : Fin 3) (i : Utilities.Certificate.SubdivisionGraph.Spec.PathPosition B α) (j : Utilities.Certificate.SubdivisionGraph.Spec.PathPosition B β) (hEven : EvenlyMarkedTheta B α β i j) {m : ℕ} (hm0 : 0 < m) (hm : m < B.length α / (B.length α).gcd ↑i) : m * ↑i % B.length α ≠ 0 ∧ m * ↑j % B.length β ≠ 0

In the nonzero part of one gcd period, neither residue is an endpoint.