An Exact Qutrit Quartic-Context Witness
Abstract
Two exact qutrit contexts give distinct quartic pricing totals for one pure state.
Theorem 1.1 (Quartic pricing is context-dependent on an exact qutrit witness).
Proof. Machine-checked in Lean as D5/S3/QuantumContext/QuarticContextWitness.quartic_pricing_context_counterexample (✓ std3). ∎
Source. Repository-derived.
Commentary.
Let rho be the rank-one qutrit density matrix whose nine entries are all one third. The declaration uniform_density_is_state proves that rho is positive semidefinite and has trace one. The standard context consists of the three coordinate projections.
The aligned context is generated by the three integer rays (1,1,1), (1,-1,0), and (1,1,-2). Dividing their outer products by 3, 2, and 6 gives the displayed rational projection matrices. The declarations standard_projection_from_ray and aligned_projection_from_ray certify these vector formulas, while the two projective-context certificates prove self-adjointness, idempotence, and exact resolution of the identity.
Quartic price is defined as the square of the real Born weight of a projection. In the standard context the three weights are all one third, so the quartic total is exactly one third. In the aligned context the weights are one, zero, and zero, so the quartic total is exactly one. The strict inequality is part of the Lean theorem and cannot be weakened to a non-strict comparison.
The companion born_control_totals certificate gives total Born weight one in both contexts. Thus the mismatch belongs to the fourth-power pricing rule, not to an incomplete context or an unnormalized state. The module proves this concrete counterexample only; it asserts no Gleason representation theorem, random-basis statistic, or general extremal classification.
References
- Truth anchor:
D5/S3/QuantumContext/QuarticContextWitness.quartic_pricing_context_counterexample - Dependency: D5/S3/Quantum/FiniteDimensional