TauLib.Polarity.PrimeBridge

Reflection lemma: is_prime_bool p = true ↔ idx_prime p.

Bridges computable Boolean primality (is_prime_bool) to the propositional definition (idx_prime). This is the foundational link needed for the CRT formal proof chain.

Main Results

• no_factor_below_true_imp: forward correctness of trial division

• no_factor_below_of_spec: backward correctness of trial division

• is_prime_bool_iff: the reflection lemma

Tau.Polarity.no_factor_below_true_imp

source **theorem Tau.Polarity.no_factor_below_true_imp (n d : Denotation.TauIdx)

(hn : n ≥ 2)

(hd : d ≥ 2)

(h : Coordinates.no_factor_below n d = true)

(k : Denotation.TauIdx) :k ≥ d → k * k ≤ n → n % k ≠ 0**

If no_factor_below n d = true, then no k in [d, √n] divides n.

Tau.Polarity.no_factor_below_of_spec

source **theorem Tau.Polarity.no_factor_below_of_spec (n d : Denotation.TauIdx)

(hn : n ≥ 2)

(hd : d ≥ 2)

(hspec : ∀ (k : Denotation.TauIdx), k ≥ d → k * k ≤ n → n % k ≠ 0) :Coordinates.no_factor_below n d = true**

If no k in [d, √n] divides n, then no_factor_below n d = true.

Tau.Polarity.is_prime_of_bool

source **theorem Tau.Polarity.is_prime_of_bool (p : Denotation.TauIdx)

(h : Coordinates.is_prime_bool p = true) :Coordinates.idx_prime p**

Forward: is_prime_bool p = true → idx_prime p.

Tau.Polarity.bool_of_is_prime

source **theorem Tau.Polarity.bool_of_is_prime (p : Denotation.TauIdx)

(h : Coordinates.idx_prime p) :Coordinates.is_prime_bool p = true**

Backward: idx_prime p → is_prime_bool p = true.

Tau.Polarity.is_prime_bool_iff

source theorem Tau.Polarity.is_prime_bool_iff (p : Denotation.TauIdx) :Coordinates.is_prime_bool p = true ↔ Coordinates.idx_prime p

Boolean primality reflects propositional primality.