Positive Pauli Clock Order
Abstract
The positive two-dimensional clock has equal isolated reduced channels and a nontrivial implemented order overlap.
This model instantiates QUANTUM-REALITY sections 101, 103 and theorem 107.2. The overlap convention is section 85: branch zero implements Q and branch one P. All velocities, frequencies and durations below are real. The source experiment takes positive frequency; the algebraic identities also hold for arbitrary real frequency. Durations have no sign restriction.
Theorem 1.1 (Standing coefficient witnesses).
Proof. Machine-checked in Lean as D5/S3/Quantum/Dynamics/PositivePauliClockOrder.positive_clock_coefficients (✓ std3). ∎
Source. Repository-derived.
Commentary.
The Hermitian coefficients and the positive constants one half and one quarter are concrete derived data.
Theorem 1.2 (Positivity on the whole source interval).
Proof. Machine-checked in Lean as D5/S3/Quantum/Dynamics/PositivePauliClockOrder.positive_clock_model (✓ std3). ∎
Source. Repository-derived.
Commentary.
The determinant estimate is strict on the entire open interval. The model is not restricted to its two pulse directions.
Theorem 1.3 (Both pulse directions are admissible).
Proof. Machine-checked in Lean as D5/S3/Quantum/Dynamics/PositivePauliClockOrder.special_directions_mem (✓ std3). ∎
Source. Repository-derived.
Commentary.
Both specified velocities lie strictly inside the source domain.
Theorem 1.4 (The positive root is invertible).
Proof. Machine-checked in Lean as D5/S3/Quantum/Dynamics/PositivePauliClockOrder.positive_clock_speed (✓ std3). ∎
Source. Repository-derived.
Commentary.
The speed is the CFC square root of the response. Response positivity proves root positivity and invertibility.
Theorem 1.5 (Exact special positive roots).
Proof. Machine-checked in Lean as D5/S3/Quantum/Dynamics/PositivePauliClockOrder.positive_clock_special_roots (✓ std3). ∎
Source. Repository-derived.
Commentary.
Positivity and the exact squares identify the candidates uniquely with the positive functional-calculus roots.
Theorem 1.6 (Canonical maximally mixed state).
Proof. Machine-checked in Lean as D5/S3/Quantum/Dynamics/PositivePauliClockOrder.mixed_state_full_support (✓ std3). ∎
Source. Repository-derived.
Commentary.
mixedState inhabits the current Foundation density carrier, with positivity and trace one proved. Its matrix has full range, so the standing support is the identity.
Theorem 1.7 (Existing propagator and source exponential agree).
Proof. Machine-checked in Lean as D5/S3/Quantum/Dynamics/PositivePauliClockOrder.pulse_eq_exp (✓ std3). ∎
Source. Repository-derived.
Commentary.
pulse reuses hamiltonianPropagator with Hamiltonian omega times the actual positive root.
Theorem 1.8 (Unitary structure propagation).
Proof. Machine-checked in Lean as D5/S3/Quantum/Dynamics/PositivePauliClockOrder.clock_propagators (✓ std3). ∎
Source. Repository-derived.
Commentary.
The normalized generator is skew-adjoint. No additional free structure evolution is inserted.
Theorem 1.9 (Implemented controlled clock evolution).
Proof. Machine-checked in Lean as D5/S3/Quantum/Dynamics/PositivePauliClockOrder.controlled_clock_evolution (✓ std3). ∎
Source. Repository-derived.
Commentary.
The joint operator is the source’s controlled expression. Its excited-clock block acts by the actual structure propagator.
Theorem 1.10 (Mixed controlled-block trace identity).
Proof. Machine-checked in Lean as D5/S3/Quantum/Dynamics/PositivePauliClockOrder.controlled_partial_trace (✓ std3). ∎
Source. Repository-derived.
Commentary.
Q, P and rho are arbitrary complex two-dimensional matrices. branch(Q,P,0) is Q and branch(Q,P,1) is P. The identity directly expands the mixed partial trace; no damping or Gram hypothesis is assumed.
Theorem 1.11 (All entries of the actual reduced channel).
Proof. Machine-checked in Lean as D5/S3/Quantum/Dynamics/PositivePauliClockOrder.clock_reduced_entries (✓ std3). ∎
Source. Repository-derived.
Commentary.
The raw matrix identity specializes to every canonical density state. The conjugate occurs in the upper off-diagonal entry.
Theorem 1.12 (Special propagators with their global phase).
Proof. Machine-checked in Lean as D5/S3/Quantum/Dynamics/PositivePauliClockOrder.clock_pulse_special_directions (✓ std3). ∎
Source. Repository-derived.
Commentary.
Pinned Mathlib’s map_exp applied to the two-coordinate algebra map and exp_diagonal evaluate the actual exponentials. No Hadamard result is copied or reproved.
Theorem 1.13 (Equal isolated coherence functions).
Proof. Machine-checked in Lean as D5/S3/Quantum/Dynamics/PositivePauliClockOrder.isolated_clock_coherence (✓ std3). ∎
Source. Repository-derived.
Commentary.
The maximally mixed structure state gives the same coherence for both directions at every real duration.
Theorem 1.14 (Equal isolated reduced channels).
Proof. Machine-checked in Lean as D5/S3/Quantum/Dynamics/PositivePauliClockOrder.isolated_clock_channels_equal (✓ std3). ∎
Source. Repository-derived.
Commentary.
Equality quantifies over the current canonical density-state carrier and the actual partial-trace maps.
Theorem 1.15 (Actual pi-pulse operators).
Proof. Machine-checked in Lean as D5/S3/Quantum/Dynamics/PositivePauliClockOrder.pi_clock_pulses (✓ std3). ∎
Source. Repository-derived.
Commentary.
The pulse equation yields iZ and iX, including the global phase inherited from the positive roots.
Theorem 1.16 (Opposite pulse orders differ by sign).
Proof. Machine-checked in Lean as D5/S3/Quantum/Dynamics/PositivePauliClockOrder.pi_clock_orders_anticommute (✓ std3). ∎
Source. Repository-derived.
Commentary.
The exponential identities specialize the existing canonical Pauli anticommutation theorem.
Theorem 1.17 (Actual coherent order marginal).
Proof. Machine-checked in Lean as D5/S3/Quantum/Dynamics/PositivePauliClockOrder.order_control_marginal (✓ std3). ∎
Source. Repository-derived.
Commentary.
The same structure register is retained through both pulses. Branch zero carries Q and branch one P; the structure is discarded only after the coherent comparison.
Theorem 1.18 (General-duration interference coefficient).
Proof. Machine-checked in Lean as D5/S3/Quantum/Dynamics/PositivePauliClockOrder.order_interference_formula (✓ std3). ∎
Source. Repository-derived.
Commentary.
With a equal to omega tPlus over two and b equal to omega tMinus over two, the independent operator trace evaluates to one minus twice sin(a) squared sin(b) squared.
Theorem 1.19 (Relative pi phase in the implemented control).
Proof. Machine-checked in Lean as D5/S3/Quantum/Dynamics/PositivePauliClockOrder.pi_order_relative_phase (✓ std3). ∎
Source. Repository-derived.
Commentary.
The actual relative operator is minus the identity, the trace overlap is minus one, and the control state has negative off-diagonal entries.
For the classical comparison, each run has a fixed label lambda and real scalar rates nPlus(lambda), nMinus(lambda). Both phases read that same label. Define zPlus and zMinus by the scalar exponential at their respective durations, and c(lambda) as the conjugate of zPlus zMinus multiplied by zMinus zPlus.
Theorem 1.20 (Fixed-label scalar order).
Proof. Machine-checked in Lean as D5/S3/Quantum/Dynamics/PositivePauliClockOrder.fixed_scalar_clock_order (✓ std3). ∎
Source. Repository-derived.
Commentary.
These scalar phases commute and have unit modulus. The relative coefficient is one, so it cannot be minus one.
Theorem 1.21 (Arbitrary probability averaging).
Proof. Machine-checked in Lean as D5/S3/Quantum/Dynamics/PositivePauliClockOrder.averaged_fixed_scalar_clock_order (✓ std3). ∎
Source. Repository-derived.
Commentary.
The measure is any probability measure on the label space. Rates need no measurability assumption for the relative coefficient, which is pointwise constant before integration. Pointwise equal ordered amplitudes also have equal Bochner integrals. Their equality alone would not exclude a sign, since both averaged amplitudes can vanish.
Theorem 1.22 (Positive-frequency source experiment).
Proof. Machine-checked in Lean as D5/S3/Quantum/Dynamics/PositivePauliClockOrder.positive_pauli_clock_order_separation (✓ std3). ∎
Source. Repository-derived.
Commentary.
For positive omega, pi over omega supplies an actual duration satisfying the pulse equation. The combined assertion retains the positive model, canonical state, implemented joint evolution, isolated equality, general-duration overlap and pi witness, together with the fixed scalar probability-average boundary.
The exclusion concerns only fixed commuting scalar clocks. Time-varying classical backgrounds, other apparatus actions, and path-dependent models require separate exclusion. The coherent comparison consumes the actual implemented operators; isolated channel tables alone do not specify controlled implementations. The reference time is the calibrated protocol parameter. The response coefficients are clock-response operators, not a claimed complete quantum spacetime metric.
References
- Truth anchor:
D5/S3/Quantum/Dynamics/PositivePauliClockOrder.averaged_fixed_scalar_clock_order - Truth anchor:
D5/S3/Quantum/Dynamics/PositivePauliClockOrder.clock_propagators - Truth anchor:
D5/S3/Quantum/Dynamics/PositivePauliClockOrder.clock_pulse_special_directions - Truth anchor:
D5/S3/Quantum/Dynamics/PositivePauliClockOrder.clock_reduced_entries - Truth anchor:
D5/S3/Quantum/Dynamics/PositivePauliClockOrder.controlled_clock_evolution - Truth anchor:
D5/S3/Quantum/Dynamics/PositivePauliClockOrder.controlled_partial_trace - Truth anchor:
D5/S3/Quantum/Dynamics/PositivePauliClockOrder.fixed_scalar_clock_order - Truth anchor:
D5/S3/Quantum/Dynamics/PositivePauliClockOrder.isolated_clock_channels_equal - Truth anchor:
D5/S3/Quantum/Dynamics/PositivePauliClockOrder.isolated_clock_coherence - Truth anchor:
D5/S3/Quantum/Dynamics/PositivePauliClockOrder.mixed_state_full_support - Truth anchor:
D5/S3/Quantum/Dynamics/PositivePauliClockOrder.order_control_marginal - Truth anchor:
D5/S3/Quantum/Dynamics/PositivePauliClockOrder.order_interference_formula - Truth anchor:
D5/S3/Quantum/Dynamics/PositivePauliClockOrder.pi_clock_orders_anticommute - Truth anchor:
D5/S3/Quantum/Dynamics/PositivePauliClockOrder.pi_clock_pulses - Truth anchor:
D5/S3/Quantum/Dynamics/PositivePauliClockOrder.pi_order_relative_phase - Truth anchor:
D5/S3/Quantum/Dynamics/PositivePauliClockOrder.positive_clock_coefficients - Truth anchor:
D5/S3/Quantum/Dynamics/PositivePauliClockOrder.positive_clock_model - Truth anchor:
D5/S3/Quantum/Dynamics/PositivePauliClockOrder.positive_clock_special_roots - Truth anchor:
D5/S3/Quantum/Dynamics/PositivePauliClockOrder.positive_clock_speed - Truth anchor:
D5/S3/Quantum/Dynamics/PositivePauliClockOrder.positive_pauli_clock_order_separation - Truth anchor:
D5/S3/Quantum/Dynamics/PositivePauliClockOrder.pulse_eq_exp - Truth anchor:
D5/S3/Quantum/Dynamics/PositivePauliClockOrder.special_directions_mem - Dependency: D5/S3/Quantum/Dynamics/ProjectionProbabilityFlow
- Dependency: D5/S3/Quantum/EnvironmentRecords
- Dependency: D5/S3/Quantum/Foundation/FiniteStateChannel