import Mathlib

/- Exact scalar-readout bridge, not a physical amplitude or Hamiltonian axiom. -/
namespace ClockTransportBridge

theorem clock_difference_restricts_to_flip (x y : ℚ) :
    ((-y) - x)^2 = (x+y)^2 := by ring

-- Readouts in the actual six-clock orbit: x, -y, z, -x, y, -z.
theorem six_clock_energy_restricts (x y z : ℚ) :
    ((-y)-x)^2 + (z-(-y))^2 + ((-x)-z)^2 +
      (y-(-x))^2 + ((-z)-y)^2 + (x-(-z))^2 =
      2*((x+y)^2+(y+z)^2+(z+x)^2) := by ring

theorem contrast_norm_counts_each_pole (x y z : ℚ) :
    x^2+(-y)^2+z^2+(-x)^2+y^2+(-z)^2 = 2*(x^2+y^2+z^2) := by ring

-- K = 2S-I for the contrast clock S(x,y,z)=(-y,-z,-x).
-- On the zero-sum plane K^2=-3I, hence K/sqrt(3) is a complex structure.
theorem contrast_rotation_square (x y z : ℚ) (h : x+y+z=0) :
    -(-x-2*y)-2*(-y-2*z) = -3*x ∧
    -(-y-2*z)-2*(-z-2*x) = -3*y ∧
    -(-z-2*x)-2*(-x-2*y) = -3*z := by
  constructor
  · linarith
  constructor <;> linarith

#print axioms clock_difference_restricts_to_flip
#print axioms six_clock_energy_restricts
#print axioms contrast_norm_counts_each_pole
#print axioms contrast_rotation_square
end ClockTransportBridge