Degree Zero Does Not Reconstruct Global Data

Abstract

A concrete finite integer family has degree zero but a nontrivial ideal class, while zero data is realized by the global element one.

Theorem 1.1 (Both local coordinates are genuine prime places).

$$\mathrm{IsPrime}\left(P2\right)\wedge \mathrm{IsPrime}\left(P5\right)\wedge \mathrm{IsPrincipal}\left(P5\right).$$

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

Source. Repository-derived.

Commentary.

The two quotients are identified with ZMod two and ZMod five. Both ideals are prime, and the second is principal.

Theorem 1.2 (The norm-two prime has nontrivial ideal class).

$$classP2\ne 1.$$

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

Source. Repository-derived.

Commentary.

The square of the norm-two ideal is the principal ideal generated by two, so its fractional ideal is invertible and defines a class-group element.

If that class were trivial, the class-group principal criterion would make the norm-two ideal principal, contradicting the existing quadratic norm obstruction.

Theorem 1.3 (The local integer family is explicit).

$$ell(P2)=1\wedge ell(P5)=-1.$$

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

Source. Repository-derived.

Commentary.

The family has coefficient one at the genuine norm-two prime place and coefficient minus one at a principal prime place. It therefore has finite support with exactly two coordinates.

Theorem 1.4 (Degree zero is not sufficient for global realization).

$$\begin{gathered} \mathrm{degree}\left(ell\right)=0\wedge \\ \neg \mathrm{IdealClassGloballyRealizable}\left(ell\right). \end{gathered}$$

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

Source. Repository-derived.

Commentary.

The two coefficients sum to zero. Their reconstructed ideal class is nevertheless the nontrivial norm-two class.

Every nonzero global element generates a principal fractional ideal and hence the identity class. No such element can match the displayed data even after passing to ideal classes.

This is the approved ideal-class downgrade: class compatibility is necessary for exact valuation realization, so failure at this coarser level already prevents reconstruction.

Theorem 1.5 (Zero local data is globally realizable).

$$\mathrm{IdealClassGloballyRealizable}\left(0\right).$$

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

Source. Repository-derived.

Commentary.

The zero family evaluates to the identity class, and the global element one generates a principal fractional ideal with that class. This separates insufficiency from universal failure.

References

• Truth anchor: D5/S3/ConceptDynamics/Fibers/DegreeZeroClassObstruction.degree_zero_class_data_not_globally_realizable
• Truth anchor: D5/S3/ConceptDynamics/Fibers/DegreeZeroClassObstruction.local_coordinates_are_prime
• Truth anchor: D5/S3/ConceptDynamics/Fibers/DegreeZeroClassObstruction.norm_two_ideal_class_is_nontrivial
• Truth anchor: D5/S3/ConceptDynamics/Fibers/DegreeZeroClassObstruction.obstruction_data_values
• Truth anchor: D5/S3/ConceptDynamics/Fibers/DegreeZeroClassObstruction.zero_class_data_is_globally_realizable
• Dependency: D5/S3/Factorization/QuadraticIdeals/NormTwoIdealLocalGlobalGap