Finite-Valuation Portrait Object Layer

Abstract

Finite valuations recover a principal fractional ideal, leaving a unit ratio.

Definition 1.1 (The height-one prime valuation portrait).

Lean statement: D5/S3/Factorization/Embeddings/FiniteValuationPortraitObjectLayer.finiteValuationPortrait

Formalization. D5/S3/Factorization/Embeddings/FiniteValuationPortraitObjectLayer.finiteValuationPortrait (✓ std3).

Source. Repository-derived.

Commentary.

The height-one prime valuation portrait.

Definition 1.2 (The quotient is the image of a base-ring unit).

Lean statement: D5/S3/Factorization/Embeddings/FiniteValuationPortraitObjectLayer.IsBaseUnitRatio

Formalization. D5/S3/Factorization/Embeddings/FiniteValuationPortraitObjectLayer.IsBaseUnitRatio (✓ std3).

Source. Repository-derived.

Commentary.

The quotient is the image of a base-ring unit.

Theorem 1.3 (The portrait reconstructs the principal fractional ideal).

$$\forall R,K:Type,CommRing(R)\wedge Field(K)\wedge Algebra(R,K)\wedge IsFractionRing(R,K)\wedge IsDedekindDomain(R)\Rightarrow \forall x\in K,x\ne 0\Rightarrow (x)=\prod _{p\in HeightOneSpectrum(R)}{p}^{nu(R,K,x,p)}.$$

Proof. Machine-checked in Lean as D5/S3/Factorization/Embeddings/FiniteValuationPortraitObjectLayer.principal_fractional_ideal_reconstruction (✓ std3). ∎

Source. Repository-derived.

Commentary.

Mathlib’s Dedekind factorization theorem is applied directly to the nonzero principal fractional ideal generated by x.

Theorem 1.4 (The reconstruction formula must exclude zero).

$$(0)\ne \prod _{p\in HeightOneSpectrum(\mathbb{Z})}{p}^{nu(\mathbb{Z},\mathbb{Q},0,p)}.$$

Proof. Machine-checked in Lean as D5/S3/Factorization/Embeddings/FiniteValuationPortraitObjectLayer.reconstruction_nonzero_hypothesis_is_necessary (✓ std3). ∎

Source. Repository-derived.

Commentary.

At zero, the principal fractional ideal is zero while the totalized all-zero exponent product is one.

Theorem 1.5 (Equal portraits are exactly base-unit ratios).

$$\forall R,K:Type,CommRing(R)\wedge Field(K)\wedge Algebra(R,K)\wedge IsFractionRing(R,K)\wedge IsDedekindDomain(R)\Rightarrow \forall x,y\in K,x\ne 0\wedge y\ne 0\Rightarrow (nu(R,K,x)=nu(R,K,y)⟺IsBaseUnitRatio(R,K,x,y)).$$

Proof. Machine-checked in Lean as D5/S3/Factorization/Embeddings/FiniteValuationPortraitObjectLayer.finite_valuation_portrait_eq_iff_base_unit_ratio (✓ std3). ∎

Source. Repository-derived.

Commentary.

Prime-valuation faithfulness first identifies the two principal fractional ideals. Equality of singleton spans is then exactly multiplication by a unit of the base Dedekind domain.

Theorem 1.6 (Every nonzero ideal has prime-valuation identity completion).

$$\forall R:Type,CommRing(R)\wedge IsDedekindDomain(R)\Rightarrow \forall I\in NonzeroIdeals(R),PrimeValuationIdentityCompletion(I).$$

Proof. Machine-checked in Lean as D5/S3/Factorization/Embeddings/FiniteValuationPortraitObjectLayer.nonzero_ideal_has_prime_valuation_identity_completion (✓ std3). ∎

Source. Repository-derived.

Commentary.

This universal statement reuses the completion predicate from section 108 and contrasts with its existential separation witness.

Theorem 1.7 (Identity completion must exclude the zero ideal).

$$\neg PrimeValuationIdentityCompletion(ZeroIdeal(\mathbb{Z})).$$

Proof. Machine-checked in Lean as D5/S3/Factorization/Embeddings/FiniteValuationPortraitObjectLayer.nonzero_ideal_hypothesis_is_necessary (✓ std3). ∎

Source. Repository-derived.

Commentary.

The imported completion predicate explicitly requires its ideal to be nonzero, so the zero ideal is a concrete counterexample.

Theorem 1.8 (The rational residual is rank zero and a sign).

$$\forall x,y\in \mathbb{Q},x\ne 0\wedge y\ne 0\Rightarrow (nu(\mathbb{Q},x)=nu(\mathbb{Q},y)⟺rank(\mathbb{Q})=0\wedge (x=y\vee x=-y)).$$

Proof. Machine-checked in Lean as D5/S3/Factorization/Embeddings/FiniteValuationPortraitObjectLayer.rational_finite_profile_eq_iff_rank_zero_sign (✓ std3). ∎

Source. Repository-derived.

Commentary.

The concrete rational portrait from section 178 leaves exactly plus or minus sign, while section 182 supplies the zero unit rank.

Theorem 1.9 (Both nonzero hypotheses are necessary).

$$(nu(\mathbb{Z},\mathbb{Q},0)=nu(\mathbb{Z},\mathbb{Q},1)\wedge \neg IsBaseUnitRatio(\mathbb{Z},\mathbb{Q},0,1))\wedge (nu(\mathbb{Z},\mathbb{Q},1)=nu(\mathbb{Z},\mathbb{Q},0)\wedge \neg IsBaseUnitRatio(\mathbb{Z},\mathbb{Q},1,0)).$$

Proof. Machine-checked in Lean as D5/S3/Factorization/Embeddings/FiniteValuationPortraitObjectLayer.nonzero_hypotheses_are_necessary (✓ std3). ∎

Source. Repository-derived.

Commentary.

The totalized count assigns the zero fractional ideal the same all-zero portrait as one, but their quotient is not a base-ring unit.

Theorem 1.10 (A composite-modulus readout is not faithful).

$$v(4,1)=v(4,2)\wedge \neg IsBaseUnitRatio(\mathbb{Z},\mathbb{Q},1,2).$$

Proof. Machine-checked in Lean as D5/S3/Factorization/Embeddings/FiniteValuationPortraitObjectLayer.composite_readout_is_not_faithful (✓ std3). ∎

Source. Repository-derived.

Commentary.

At modulus four, one and two both have value zero although one half is not an integer unit. Prime coordinates are therefore load-bearing.

References

• Truth anchor: D5/S3/Factorization/Embeddings/FiniteValuationPortraitObjectLayer.IsBaseUnitRatio
• Truth anchor: D5/S3/Factorization/Embeddings/FiniteValuationPortraitObjectLayer.composite_readout_is_not_faithful
• Truth anchor: D5/S3/Factorization/Embeddings/FiniteValuationPortraitObjectLayer.finiteValuationPortrait
• Truth anchor: D5/S3/Factorization/Embeddings/FiniteValuationPortraitObjectLayer.finite_valuation_portrait_eq_iff_base_unit_ratio
• Truth anchor: D5/S3/Factorization/Embeddings/FiniteValuationPortraitObjectLayer.nonzero_hypotheses_are_necessary
• Truth anchor: D5/S3/Factorization/Embeddings/FiniteValuationPortraitObjectLayer.nonzero_ideal_has_prime_valuation_identity_completion
• Truth anchor: D5/S3/Factorization/Embeddings/FiniteValuationPortraitObjectLayer.nonzero_ideal_hypothesis_is_necessary
• Truth anchor: D5/S3/Factorization/Embeddings/FiniteValuationPortraitObjectLayer.principal_fractional_ideal_reconstruction
• Truth anchor: D5/S3/Factorization/Embeddings/FiniteValuationPortraitObjectLayer.rational_finite_profile_eq_iff_rank_zero_sign
• Truth anchor: D5/S3/Factorization/Embeddings/FiniteValuationPortraitObjectLayer.reconstruction_nonzero_hypothesis_is_necessary
• Dependency: D5/S3/Factorization/Embeddings/DirichletUnitCompletion
• Dependency: D5/S3/Factorization/Embeddings/RationalValuationRecovery
• Dependency: D5/S3/Observer/Completion/ThreeCompletionOrthogonality