Keyboard shortcuts

Press or to navigate between chapters

Press ? to show this help

Press Esc to hide this help

Typed Prime-Language Hierarchy

Abstract

Prime-observation languages have strict comparisons only on shared state types.

Theorem 1.1 (Equal radical and support do not determine multiplicity).

Proof. Machine-checked in Lean as D5/S3/ConceptDynamics/ObservationOrder/TypedPrimeLanguageHierarchy.support_multiplicity_witness (✓ std3). ∎

Source. Repository-derived.

Commentary.

The positive naturals two and four have the same radical and the same prime support, while their exponent tables differ at two.

This is the named witness used to refute recovery of valuations from support alone.

Theorem 1.2 (Support is strictly coarser than valuation).

Proof. Machine-checked in Lean as D5/S3/ConceptDynamics/ObservationOrder/TypedPrimeLanguageHierarchy.support_strictly_coarser_than_valuation (✓ std3). ∎

Source. Repository-derived.

Commentary.

Finite support factors through the canonical prime-exponent language. The reverse factor would identify the exponent tables of two and four, contradicting the named witness.

Both readouts have the common state type of positive naturals; no cross-type comparison is asserted.

Theorem 1.3 (Equal prime diagonals do not determine relative phase).

Proof. Machine-checked in Lean as D5/S3/ConceptDynamics/ObservationOrder/TypedPrimeLanguageHierarchy.relative_phase_density_witness (✓ std3). ∎

Source. Repository-derived.

Commentary.

The equal-superposition density operator and its Pauli-Z phase flip are positive trace-one matrices with equal diagonal entries.

Canonical prime dephasing therefore gives the same matrix, while the full operator readout distinguishes their off-diagonal entries.

Theorem 1.4 (Prime-diagonal readout is strictly coarser than operators).

Proof. Machine-checked in Lean as D5/S3/ConceptDynamics/ObservationOrder/TypedPrimeLanguageHierarchy.prime_diagonal_strictly_coarser_than_operator (✓ std3). ∎

Source. Repository-derived.

Commentary.

Prime dephasing factors through the full density-operator readout. The reverse factor is impossible because the named phase pair has one dephased output and two distinct operator outputs.

This theorem compares readouts only on qubit density states. The source’s warning against a transport-free global order remains a metalevel typing statement and is intentionally not encoded.

References