def Hex.Modular.ratReconCheck (a : Int) (m : Nat) (P Q : Int) (x : Rat) : Bool

Check that x represents a modulo m and satisfies the requested numerator and denominator bounds. This is split from the Euclidean search so certificate replay need not unfold that search.

Equations

• Hex.Modular.ratReconCheck a m P Q x = (decide (0 < m) && decide ((Int.ofNat x.den * a - x.num) % ↑m = 0) && decide (↑x.num.natAbs ≤ P) && decide (0 < ↑x.den) && decide (↑x.den ≤ Q))

def Hex.Modular.ratRecon? (a : Int) (m : Nat) (P Q : Int) : Option Rat

Reconstruct a mod m as a rational with numerator absolute value at most P and positive denominator at most Q. The truncated Euclidean candidate is normalized and all output conditions are checked before it is returned.

Equations

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

def Hex.Modular.ratReconWide? (a : Int) (m : Nat) : Option Rat

Symmetric rational reconstruction with P = Q = ⌊√((m-1)/2)⌋, which guarantees 2 P Q < m.

Equations

• Hex.Modular.ratReconWide? a m = Hex.Modular.ratRecon? a m (Int.ofNat ((m - 1) / 2).sqrt) (Int.ofNat ((m - 1) / 2).sqrt)

theorem Hex.Modular.ratRecon?_congr {a : Int} {m : Nat} {P Q : Int} {x : Rat} (h : ratRecon? a m P Q = some x) : (Int.ofNat x.den * a - x.num) % ↑m = 0

Every rational returned by bounded reconstruction satisfies the requested modular congruence.

theorem Hex.Modular.ratRecon?_bounds {a : Int} {m : Nat} {P Q : Int} {x : Rat} (h : ratRecon? a m P Q = some x) : ↑x.num.natAbs ≤ P ∧ 0 < x.den ∧ ↑x.den ≤ Q

Every rational returned by bounded reconstruction satisfies the requested numerator and denominator bounds.

theorem Hex.Modular.ratRecon?_den_coprime {a : Int} {m : Nat} {P Q : Int} {x : Rat} (h : ratRecon? a m P Q = some x) : x.den.gcd m = 1

The reduced denominator of a successful reconstruction is coprime to the modulus.

theorem Hex.Modular.ratRecon_unique {a P Q : Int} {m : Nat} {y₁ y₂ : Rat} (hm : 2 * P * Q < ↑m) (h₁ : (Int.ofNat y₁.den * a - y₁.num) % ↑m = 0) (h₂ : (Int.ofNat y₂.den * a - y₂.num) % ↑m = 0) (b₁ : ↑y₁.num.natAbs ≤ P ∧ ↑y₁.den ≤ Q) (b₂ : ↑y₂.num.natAbs ≤ P ∧ ↑y₂.den ≤ Q) : y₁ = y₂

Rational reconstruction is unique whenever twice the product of the two bounds is strictly smaller than the modulus.

theorem Hex.Modular.ratRecon?_complete {a P Q : Int} {m : Nat} {y : Rat} (hm : 2 * P * Q < ↑m) (hy : (Int.ofNat y.den * a - y.num) % ↑m = 0) (hb : ↑y.num.natAbs ≤ P ∧ ↑y.den ≤ Q) : ratRecon? a m P Q = some y

Under the uniqueness bound, bounded reconstruction finds every rational that satisfies the congruence and bounds.

def Hex.Modular.ratReconVec? {k : Nat} (a : Vector Int k) (m : Nat) (P Q : Int) : Option (Vector Int k × Int)

Reconstruct k residues as rationals with a common denominator. The first entry seeds the denominator. Later entries first try one symmetric multiplication at that denominator, falling back to their own Euclidean run only when necessary. Denominators are combined with lcm, and the final numerator vector and denominator are reduced by their common gcd.

Equations

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

theorem Hex.Modular.ratReconVec?_spec {k : Nat} {a : Vector Int k} {m : Nat} {P Q d : Int} {y : Vector Int k} (h : ratReconVec? a m P Q = some (y, d)) : 0 < d ∧ d ≤ Q ∧ ∀ (i : Fin k), (d * a[i] - y[i]) % ↑m = 0 ∧ ↑y[i].natAbs ≤ P

A successful common-denominator vector reconstruction has a positive bounded denominator, and every coordinate satisfies its congruence and numerator bound.

theorem Hex.Modular.ratReconVec?_complete {k : Nat} {a y : Vector Int k} {m : Nat} {P Q d : Int} (hm : 2 * P * Q < ↑m) (hP : 0 ≤ P) (hd : 0 < d) (hdQ : d ≤ Q) (hy : ∀ (i : Fin k), (d * a[i] - y[i]) % ↑m = 0 ∧ ↑y[i].natAbs ≤ P) (hred : ∀ (g : Int), (∀ (i : Fin k), g ∣ y[i]) → g ∣ d → g ∣ 1) : ratReconVec? a m P Q = some (y, d)

Under the uniqueness bound, common-denominator reconstruction finds every pair that is reduced as a whole, positive and bounded in its denominator, and congruent and bounded in every coordinate. Reducedness is not decoration: at m = 18, a = (10), the pair (2, 2) satisfies every other hypothesis, but its reduced rational 1 does not satisfy the congruence and the reconstruction returns none.

def Hex.Modular.ratReconMaxQuot? (a : Int) (m : Nat) : Option Rat

Produce the maximal-quotient rational-reconstruction candidate. This is a heuristic: only the modular congruence is checked and promised.

Equations

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

theorem Hex.Modular.ratReconMaxQuot?_congr {a : Int} {m : Nat} {x : Rat} (h : ratReconMaxQuot? a m = some x) : (Int.ofNat x.den * a - x.num) % ↑m = 0

A maximal-quotient candidate always satisfies the modular congruence; no claim is made that it is the intended rational.