Prime-Diagonal Saturation

Abstract

Finite prime occupation operators generate a diagonal algebra saturated by pinching.

Definition 1.1 (Prime occupation-number operator).

Lean statement: D5/S3/Quantum/FixedAlgebra/PrimeDiagonalSaturation.primeOccupationOperator

Formalization. D5/S3/Quantum/FixedAlgebra/PrimeDiagonalSaturation.primeOccupationOperator (✓ std3).

Source. Repository-derived.

Commentary.

On the finite integer basis one through d, the operator for p is diagonal and its ith diagonal coefficient is the existing prime occupation coordinate of i plus one.

Definition 1.2 (Finite prime-generated diagonal algebra).

Lean statement: D5/S3/Quantum/FixedAlgebra/PrimeDiagonalSaturation.primeDiagonalAlgebra

Formalization. D5/S3/Quantum/FixedAlgebra/PrimeDiagonalSaturation.primeDiagonalAlgebra (✓ std3).

Source. Repository-derived.

Commentary.

For a finite set P of primes, take the complex subalgebra generated by the corresponding occupation-number operators. This names the observable algebra rather than inlining its generating set into the theorem.

Lemma 1.3 (Prime occupation operators are diagonal).

$$\forall d,p,i,j,\mathrm{primeOccupationOperator}\left(d,p,i,j\right)=\mathrm{if}\left(i=j,\mathrm{primeOccupancy}\left(p,i+1\right),0\right).$$

Proof. Machine-checked in Lean as D5/S3/Quantum/FixedAlgebra/PrimeDiagonalSaturation.prime_occupation_operator_apply (✓ std3). ∎

Source. Repository-derived.

Commentary.

Every off-diagonal entry vanishes, while diagonal entry i is the exponent of p in the positive integer i plus one.

Lemma 1.4 (The generated algebra lies in the full diagonal algebra).

$$\forall d,P,\mathrm{primeDiagonalAlgebra}\left(d,P\right)\subseteq \mathrm{range}\left(\mathrm{diagonalAlgHom}\left(C\right)\right).$$

Proof. Machine-checked in Lean as D5/S3/Quantum/FixedAlgebra/PrimeDiagonalSaturation.prime_diagonal_algebra_le_full_diagonal (✓ std3). ∎

Source. Repository-derived.

Commentary.

Each generator belongs to the range of Mathlib’s diagonal algebra map. The universal property of algebraic adjoining therefore places the whole finite prime-generated algebra in that diagonal range.

Theorem 1.5 (Prime-diagonal statistics are saturated by pinching).

$$\forall d,P,\rho ,A,A\in \mathrm{primeDiagonalAlgebra}\left(d,P\right)\Rightarrow \mathrm{Tr}\left(\rho A\right)=\mathrm{Tr}\left(\mathrm{projectiveReadout}\left(\rho \right)A\right).$$

Proof. Machine-checked in Lean as D5/S3/Quantum/FixedAlgebra/PrimeDiagonalSaturation.prime_diagonal_saturation (✓ std3). ∎

Source. Repository-derived.

Commentary.

For every complex matrix rho and every observable A in the finite prime-generated algebra, the trace of rho times A equals the trace after complete diagonal readout.

No positivity, Hermiticity, or trace-one assumption is needed. The source’s state hypothesis is therefore weakened to an arbitrary matrix, while the prime-generated observable restriction remains.

Lemma 1.6 (Degenerate prime-diagonal cases remain valid).

$$\mathrm{Sat}\left(0,\varnothing \right)\wedge \mathrm{Sat}\left(1,\varnothing \right)\wedge \forall d,P,\rho ,\mathrm{Sat}\left(d,P,\rho ,1\right)\wedge \forall A,\mathrm{projectiveReadout}\left(\rho \right)=\rho \Rightarrow \mathrm{Sat}\left(d,P,\rho ,A\right),Sat=\mathrm{primeDiagonalSaturation}\left(\right).$$

Proof. Machine-checked in Lean as D5/S3/Quantum/FixedAlgebra/PrimeDiagonalSaturation.prime_diagonal_degenerate_audit (✓ std3). ∎

Source. Repository-derived.

Commentary.

The same equality is checked at dimensions zero and one, with no prime generators, for the identity observable, and whenever the input is already fixed by complete diagonal readout.

Proposition 1.7 (The diagonal observable restriction is necessary).

$$\neg \mathrm{single}\left(1,0,1\right)\in \mathrm{primeDiagonalAlgebra}\left(2,\varnothing \right)\wedge \mathrm{Tr}\left(\mathrm{single}\left(0,1,1\right)\mathrm{single}\left(1,0,1\right)\right)\ne \mathrm{Tr}\left(\mathrm{projectiveReadout}\left(\mathrm{single}\left(0,1,1\right)\right)\mathrm{single}\left(1,0,1\right)\right).$$

Proof. Machine-checked in Lean as D5/S3/Quantum/FixedAlgebra/PrimeDiagonalSaturation.observable_membership_is_necessary (✓ std3). ∎

Source. Repository-derived.

Commentary.

In dimension two, opposite matrix units multiply to a diagonal unit of nonzero trace. Pinching removes the first off-diagonal matrix unit, and the second lies outside the prime-generated diagonal algebra.

References

• Truth anchor: D5/S3/Quantum/FixedAlgebra/PrimeDiagonalSaturation.observable_membership_is_necessary
• Truth anchor: D5/S3/Quantum/FixedAlgebra/PrimeDiagonalSaturation.primeDiagonalAlgebra
• Truth anchor: D5/S3/Quantum/FixedAlgebra/PrimeDiagonalSaturation.primeOccupationOperator
• Truth anchor: D5/S3/Quantum/FixedAlgebra/PrimeDiagonalSaturation.prime_diagonal_algebra_le_full_diagonal
• Truth anchor: D5/S3/Quantum/FixedAlgebra/PrimeDiagonalSaturation.prime_diagonal_degenerate_audit
• Truth anchor: D5/S3/Quantum/FixedAlgebra/PrimeDiagonalSaturation.prime_diagonal_saturation
• Truth anchor: D5/S3/Quantum/FixedAlgebra/PrimeDiagonalSaturation.prime_occupation_operator_apply
• Dependency: D5/S3/Analytic/ZetaObservation/MultiplicativeComplexityActivation
• Dependency: D5/S3/Quantum/Decoherence/ProjectedUnistochasticDynamics