Ideal Recovery Does Not Imply Principality

Abstract

Exact recovery of an ideal does not supply a global generator. A concrete nonprincipal prime ideal is contrasted with principal-ideal rings and the degenerate zero and unit ideals.

Theorem 1.1 (A uniquely identified prime ideal can be nonprincipal).

$$\begin{gathered} (\exists !I:\mathrm{Ideal}\left(QuadraticOrder\right),I=normTwoIdeal)\wedge \\ \mathrm{IsPrime}\left(normTwoIdeal\right)\wedge \neg \mathrm{IsPrincipal}\left(normTwoIdeal\right). \end{gathered}$$

Proof. Machine-checked in Lean as D5/S3/ConceptDynamics/Fibers/IdealRecoveryNotPrincipality.uniquely_recovered_prime_ideal_need_not_be_principal (✓ std3). ∎

Source. Repository-derived.

Commentary.

The named data is the existing ideal generated by 2 and 1 + sqrt(-5). Equality with that named ideal determines it uniquely, while the imported D5 theorem supplies its global nonprincipality without repeating the norm obstruction.

Its quotient is identified with ZMod two. The quotient is a field, so the ideal is maximal and hence prime. Primality strengthens the witness but is not used to infer nonprincipality.

This is distinct from FPOD 191.1: that gauge theorem starts with a principal ideal and compares generators up to a unit. Here no global generator exists.

Theorem 1.2 (Every ideal is principal in a principal-ideal ring).

$$\begin{gathered} \forall R,\mathrm{Semiring}\left(R\right)\wedge \mathrm{IsPrincipalIdealRing}\left(R\right)\Rightarrow \\ \forall I:\mathrm{Ideal}\left(R\right),\mathrm{IsPrincipal}\left(I\right). \end{gathered}$$

Proof. Machine-checked in Lean as D5/S3/ConceptDynamics/Fibers/IdealRecoveryNotPrincipality.every_ideal_is_principal_in_principal_ideal_ring (✓ std3). ∎

Source. Repository-derived.

Commentary.

Mathlib’s principal-ideal-ring structure gives this conclusion directly. Only a semiring is required by the actual class definition; no field or domain hypothesis is added.

Theorem 1.3 (The principal-ideal-ring hypothesis cannot be dropped).

$$\neg \mathrm{IsPrincipalIdealRing}\left(QuadraticOrder\right).$$

Proof. Machine-checked in Lean as D5/S3/ConceptDynamics/Fibers/IdealRecoveryNotPrincipality.principal_ideal_ring_hypothesis_is_necessary (✓ std3). ∎

Source. Repository-derived.

Commentary.

The minus-five quadratic order has the concrete nonprincipal ideal from the first theorem, so it cannot carry a principal-ideal-ring instance. This is the named counterexample required by the hypothesis audit.

Theorem 1.4 (Zero and unit ideals are principal).

$$\mathrm{IsPrincipal}\left(bot\right)\wedge \mathrm{IsPrincipal}\left(top\right).$$

Proof. Machine-checked in Lean as D5/S3/ConceptDynamics/Fibers/IdealRecoveryNotPrincipality.zero_and_unit_ideals_are_principal (✓ std3). ∎

Source. Repository-derived.

Commentary.

Both degenerate ideals are principal in every semiring. The empty carrier is excluded by zero, and the singleton semiring ZMod one also has only principal ideals. Thus the counterexample must be a proper nonzero ideal outside the PID case.

References

• Truth anchor: D5/S3/ConceptDynamics/Fibers/IdealRecoveryNotPrincipality.every_ideal_is_principal_in_principal_ideal_ring
• Truth anchor: D5/S3/ConceptDynamics/Fibers/IdealRecoveryNotPrincipality.principal_ideal_ring_hypothesis_is_necessary
• Truth anchor: D5/S3/ConceptDynamics/Fibers/IdealRecoveryNotPrincipality.uniquely_recovered_prime_ideal_need_not_be_principal
• Truth anchor: D5/S3/ConceptDynamics/Fibers/IdealRecoveryNotPrincipality.zero_and_unit_ideals_are_principal
• Dependency: D5/S3/Factorization/IdealClassGroups/IdealIdentityPrincipalityGeneratorLayers