Finitely Blind Prime Ideals

Abstract

Dedekind reductions have finite blind sets and a coarse-property counterexample.

Theorem 1.1 (Reduction equality is divisibility of the difference).

$$\forall v,a,b\Rightarrow \mathrm{primeIdealReduction}\left(v,a\right)=\mathrm{primeIdealReduction}\left(v,b\right)⟺\mathrm{IdealDvdSpan}\left(v,a-b\right).$$

Proof. Machine-checked in Lean as D5/S3/Arith/PrimeIdeals/FinitelyBlindPrimeIdeals.reduction_eq_iff_dvd_difference (✓ std3). ∎

Source. Repository-derived.

Commentary.

The canonical ideal quotient map identifies two elements exactly when their difference lies in the prime ideal. In a Dedekind domain, membership is the same as divisibility of its principal ideal.

Theorem 1.2 (Distinct elements have finitely many blind prime ideals).

$$\forall a,b,a\ne b\Rightarrow \mathrm{Finite}(\mathrm{blindPrimeIdeals}\left(a,b\right)).$$

Proof. Machine-checked in Lean as D5/S3/Arith/PrimeIdeals/FinitelyBlindPrimeIdeals.finite_blind_prime_ideals (✓ std3). ∎

Source. Repository-derived.

Commentary.

The nonzero principal ideal generated by a - b has only finitely many height-one prime divisors. The equality theorem transports that finite support to the set of prime ideals where reduction is blind.

Theorem 1.3 (A unit difference has no blind prime ideal).

$$\mathrm{IsUnit}\left(a-b\right)\Rightarrow \mathrm{blindPrimeIdeals}\left(a,b\right)=\varnothing .$$

Proof. Machine-checked in Lean as D5/S3/Arith/PrimeIdeals/FinitelyBlindPrimeIdeals.unit_difference_has_no_blind_prime_ideals (✓ std3). ∎

Source. Repository-derived.

Commentary.

When a - b is a unit, no proper prime ideal can contain it. Thus the exceptional blind set is empty, explicitly covering the unit case.

Theorem 1.4 (The zero-reduction property merges one and negative one everywhere).

$$1\ne -1\wedge \forall v\in \mathbb{Z},\mathrm{zeroReductionObservation}\left(v,1\right)⟺\mathrm{zeroReductionObservation}\left(v,-1\right).$$

Proof. Machine-checked in Lean as D5/S3/Arith/PrimeIdeals/FinitelyBlindPrimeIdeals.coarse_zero_observation_counterexample (✓ std3). ∎

Source. Repository-derived.

Commentary.

In the concrete integer ring, 1 and -1 are distinct global elements, but both are units. Their reduction is therefore nonzero at every prime ideal, so the coarse zero/nonzero property agrees everywhere.

Theorem 1.5 (Distinctness is necessary for separation).

$$\neg \exists v\in \mathbb{Z},\mathrm{primeIdealReduction}\left(v,0\right)\ne \mathrm{primeIdealReduction}\left(v,0\right).$$

Proof. Machine-checked in Lean as D5/S3/Arith/PrimeIdeals/FinitelyBlindPrimeIdeals.distinctness_is_necessary_for_separation (✓ std3). ∎

Source. Repository-derived.

Commentary.

For the concrete equal pair 0, 0, every prime ideal gives the same reduction. This records why the distinctness premise is required for a separation conclusion.

References

• Truth anchor: D5/S3/Arith/PrimeIdeals/FinitelyBlindPrimeIdeals.coarse_zero_observation_counterexample
• Truth anchor: D5/S3/Arith/PrimeIdeals/FinitelyBlindPrimeIdeals.distinctness_is_necessary_for_separation
• Truth anchor: D5/S3/Arith/PrimeIdeals/FinitelyBlindPrimeIdeals.finite_blind_prime_ideals
• Truth anchor: D5/S3/Arith/PrimeIdeals/FinitelyBlindPrimeIdeals.reduction_eq_iff_dvd_difference
• Truth anchor: D5/S3/Arith/PrimeIdeals/FinitelyBlindPrimeIdeals.unit_difference_has_no_blind_prime_ideals