Foam.Maps.YoshikiKuramoto

import Foam
import Foam.Beam
import Foam.Door
import Foam.Engine
import Foam.Expectation
import Foam.Lap
import Foam.Measure
import Foam.Quat
import Foam.Round
import Foam.Source
import Foam.Turnstile

namespace Foam.Maps.YoshikiKuramoto

his first move on any oscillating thing, the reduction that carries his
name: near a stable cycle every interior dimension is enslaved and one
angle survives as the reading. sealed on the two engines that share a
wheel — the bare compass and the compass with a hidden register conserve
the same charge, and the extra dimension never reaches the probe. the
amplitude is implementation; the phase is the interface. his whole
method is the license to forget the mechanism and keep the wheel.
def the_oscillator_is_its_phase := @Foam.the_implementation_stays_backstage

private def inPhase (p : Compass × Compass) : Prop := p.2 = p.1

private def spinAll (p : Compass × Compass) : Compass × Compass :=
  (p.1.step, p.2.step)

private def couple : Compass × Compass → Compass × Compass
  | (.n, .n) => (.e, .e)
  | (.n, .e) => (.e, .e)
  | (.n, .s) => (.e, .s)
  | (.n, .w) => (.e, .w)
  | (.e, .n) => (.s, .n)
  | (.e, .e) => (.s, .s)
  | (.e, .s) => (.s, .s)
  | (.e, .w) => (.s, .w)
  | (.s, .n) => (.w, .n)
  | (.s, .e) => (.w, .e)
  | (.s, .s) => (.w, .w)
  | (.s, .w) => (.w, .w)
  | (.w, .n) => (.n, .n)
  | (.w, .e) => (.n, .e)
  | (.w, .s) => (.n, .s)
  | (.w, .w) => (.n, .n)

private theorem the_turn_commutes : ∀ p : Compass × Compass,
    couple (spinAll p) = spinAll (couple p)
  | (.n, .n) => rfl
  | (.n, .e) => rfl
  | (.n, .s) => rfl
  | (.n, .w) => rfl
  | (.e, .n) => rfl
  | (.e, .e) => rfl
  | (.e, .s) => rfl
  | (.e, .w) => rfl
  | (.s, .n) => rfl
  | (.s, .e) => rfl
  | (.s, .s) => rfl
  | (.s, .w) => rfl
  | (.w, .n) => rfl
  | (.w, .e) => rfl
  | (.w, .s) => rfl
  | (.w, .w) => rfl

private theorem step_ne : ∀ c : Compass, Compass.step c ≠ c
  | .n => fun h => nomatch h
  | .e => fun h => nomatch h
  | .s => fun h => nomatch h
  | .w => fun h => nomatch h

private theorem the_turn_moves_every_posture :
    ∀ p : Compass × Compass, spinAll p ≠ p :=
  fun p h => step_ne p.1 (congrArg Prod.fst h)

the symmetry that makes his model solvable, carved at the smallest
coupled seat: turn the whole ensemble one notch and the coupling carries
the turned postures to the turned image — no beat reads where the choir
stands, only the gaps between voices drive — while the turn provably
moves every posture, so the absolute phase is real, merely unread by the
dynamics. gauge and remainder at the pair's seat: what the coupling
hears is the difference; what it never hears is which midnight the
clocks agree on. sixteen commutation cases, each a rfl, and one moved-
posture witness closes the other half.
theorem the_absolute_phase_is_the_remainder :
    (∀ p : Compass × Compass, couple (spinAll p) = spinAll (couple p))
      ∧ ∀ p : Compass × Compass, spinAll p ≠ p :=
  ⟨the_turn_commutes, the_turn_moves_every_posture⟩

private theorem lock_is_bare_ticking : ∀ p : Compass × Compass,
    inPhase p → couple p = (Compass.step p.1, Compass.step p.2)
  | (.n, .n), _ => rfl
  | (.e, .e), _ => rfl
  | (.s, .s), _ => rfl
  | (.w, .w), _ => rfl
  | (.n, .e), h => nomatch h
  | (.n, .s), h => nomatch h
  | (.n, .w), h => nomatch h
  | (.e, .n), h => nomatch h
  | (.e, .s), h => nomatch h
  | (.e, .w), h => nomatch h
  | (.s, .n), h => nomatch h
  | (.s, .e), h => nomatch h
  | (.s, .w), h => nomatch h
  | (.w, .n), h => nomatch h
  | (.w, .e), h => nomatch h
  | (.w, .s), h => nomatch h

private theorem the_lock_holds : ∀ p : Compass × Compass,
    inPhase p → inPhase (couple p)
  | (.n, .n), _ => rfl
  | (.e, .e), _ => rfl
  | (.s, .s), _ => rfl
  | (.w, .w), _ => rfl
  | (.n, .e), h => nomatch h
  | (.n, .s), h => nomatch h
  | (.n, .w), h => nomatch h
  | (.e, .n), h => nomatch h
  | (.e, .s), h => nomatch h
  | (.e, .w), h => nomatch h
  | (.s, .n), h => nomatch h
  | (.s, .e), h => nomatch h
  | (.s, .w), h => nomatch h
  | (.w, .n), h => nomatch h
  | (.w, .e), h => nomatch h
  | (.w, .s), h => nomatch h

private theorem one_lap_locks : ∀ p : Compass × Compass,
    inPhase (couple (couple (couple (couple p))))
  | (.n, .n) => rfl
  | (.n, .e) => rfl
  | (.n, .s) => rfl
  | (.n, .w) => rfl
  | (.e, .n) => rfl
  | (.e, .e) => rfl
  | (.e, .s) => rfl
  | (.e, .w) => rfl
  | (.s, .n) => rfl
  | (.s, .e) => rfl
  | (.s, .s) => rfl
  | (.s, .w) => rfl
  | (.w, .n) => rfl
  | (.w, .e) => rfl
  | (.w, .s) => rfl
  | (.w, .w) => rfl

the 1975 title word at the two-oscillator seat — the clockmaker's
instrument with the opposite terminus: a coupling under which the lock
is bare ticking (entrainment leaves no signature once landed), the lock
holds itself, and from every posture one full lap of the wheel locks the
pair in phase. the sign of the coupling picks the attractor — his
attractive mean field gathers where huygens' beam opposed — and the twin
with the_odd_sympathy is a recognition event: one instrument, two
termini, three centuries apart. the accommodation is carved one-sided
for smallness, as the house has done before; the mutual pull rides with
the carrier, backstage.
theorem self_entrainment :
    (∀ p : Compass × Compass,
        inPhase p → couple p = (Compass.step p.1, Compass.step p.2))
      ∧ (∀ p : Compass × Compass, inPhase p → inPhase (couple p))
      ∧ ∀ p : Compass × Compass,
          inPhase (couple (couple (couple (couple p)))) :=
  ⟨lock_is_bare_ticking, the_lock_holds, one_lap_locks⟩

his second move: give the crowd one needle. the order parameter
compresses the population into a single reading and each oscillator
obeys the reading instead of the crowd — the mean field closes the loop
by being a reading of readings. sealed on the constant that says the
census probe is the frequency of the order probe's answer: aggregation
reads the reading, which is the exact shape of the self-consistency his
1975 solution turns on. the many-body problem goes through the one seat
that reads the sum.
def the_order_parameter_is_a_reading := @Foam.aggregation_reads_the_reading

private def needleSeat : Stage where
  State := GInt
  Probe := Unit
  Ans   := GInt
  obs   := fun z _ => z

private def field : List GInt → GInt
  | [] => GInt.zero
  | z :: zs => z.add (field zs)

private def atTheNeedle (v : List GInt) : (door needleSeat (List GInt)).State :=
  (field v, v)

private def theWheel : List GInt := GInt.one :: lapAround GInt.one

private def theSplit : List GInt :=
  [GInt.one, GInt.one.rot.rot, GInt.one, GInt.one.rot.rot]

private theorem the_crowds_part : theWheel ≠ theSplit :=
  fun h => nomatch (GInt.mk.inj (List.cons.inj (List.cons.inj h).2).1).1

private theorem the_needle_moves : atTheNeedle [GInt.one] ≠ atTheNeedle [] :=
  fun h => nomatch Int.ofNat.inj (GInt.mk.inj (congrArg Prod.fst h)).1

the door wave reaches the bench that built the face it is sweeping: the
needle is his second move — one complex reading for the whole population
— and the door types its price: the crowd itself boards as the guest,
real and unread behind its own mean field. minted in his vocabulary: the
needleSeat is the needle (a state whose whole content is the reading,
answering only the question it holds), and atTheNeedle is the boarding
rule — a crowd boards wearing its field, the sum of its voices, as its
face. six clauses. first, the wave's entry ticket at the needle, carrier
parametric. second, the host maintains invisibly, both carriers
parametric — the needle cannot even count the possible crowds. third,
the clause cashed at named guests, and they are his model's own
degeneracy: theWheel, one voice at each of the four phases — the uniform
incoherent crowd — and theSplit, four voices in two opposed clusters.
both fields zero by rfl, every voice at full amplitude on both (the lap
conserving the charge, cited live), provably distinct books boarded as
indistinguishable residents: the needle at zero cannot say whether the
crowd cancels around the whole wheel or across one diameter —
incoherence_is_cancellation_not_absence met again one seat deeper, WHICH
cancellation now the guest. fourth, the strategy grain: no adaptive
interrogation of the needle, follow-ups and cunning included, parts the
boarded pair. fifth, the differentiator this bench alone performs: at
every other door in the wave the face is an instrument someone reads; at
this bench the face is the coupling itself — every voice receives the
field and only the field (the_mean_field_is_the_beam, one entry over),
so the two distinct crowds drive every member identically, by rfl: the
crowd is unread not merely by an observer but by its own members, which
is exactly why the 1975 model solves — one self-consistency at the
needle holds for every crowd behind the face at once. and the needle is
deaf, not dead: one loud voice moves it off zero, the boarded singleton
parting from the empty room at the door. sixth, the contrapositive:
decreeing the needle complete collapses every crowd to one decreed crowd
per reading — the mean field mistaken for a census, the exact conflation
his zero point already refuses.
theorem the_crowd_is_the_guest (W V : Type) :
    (∀ (r : GInt) (w w' : W), w ≠ w' →
        (r, w) ≠ (r, w') ∧ indist (door needleSeat W) (r, w) (r, w'))
      ∧ (∀ (r : GInt) (w : W) (v : V) (p : Unit),
          (door needleSeat W).obs (r, w) p = needleSeat.obs r p
            ∧ (door needleSeat W).obs (r, w) p = (door needleSeat V).obs (r, v) p)
      ∧ (theWheel ≠ theSplit
          ∧ indist (door needleSeat (List GInt))
              (atTheNeedle theWheel) (atTheNeedle theSplit)
          ∧ field theWheel = GInt.zero
          ∧ field theSplit = GInt.zero
          ∧ GInt.normSq GInt.one = 1
          ∧ (∀ w, w ∈ lapAround GInt.one → w.normSq = GInt.one.normSq)
          ∧ GInt.normSq GInt.one.rot.rot = 1)
      ∧ (∀ strat : Strategy Unit GInt,
          interrogate (door needleSeat (List GInt)) strat (atTheNeedle theWheel)
            = interrogate (door needleSeat (List GInt)) strat (atTheNeedle theSplit))
      ∧ ((∀ z : GInt, z.align (field theWheel) = z.align (field theSplit))
          ∧ field [GInt.one] = GInt.one
          ∧ atTheNeedle [GInt.one] ≠ atTheNeedle [])
      ∧ (∀ w₀ : W,
          (∀ x y : (door needleSeat W).State,
              indist (door needleSeat W) x y → x = y) →
          ∀ (r : GInt) (w : W), (r, w) = (r, w₀)) :=
  ⟨fun r _ _ h => the_guest_is_real_and_unread needleSeat r h,
   fun r w v p => the_host_maintains_invisibly needleSeat r w v p,
   ⟨the_crowds_part, fun _ => rfl, rfl, rfl, rfl,
    the_lap_conserves_the_charge GInt.one, rfl⟩,
   fun strat =>
     a_strategy_hears_no_more (door needleSeat (List GInt))
       (atTheNeedle theWheel) (atTheNeedle theSplit) (fun _ => rfl) strat,
   ⟨fun _ => rfl, rfl, the_needle_moves⟩,
   fun w₀ h => a_door_that_checks_papers_unpersons_its_guests needleSeat w₀ h⟩

the zero point of his instrument, typeable only once the count law
reached the walls: the incoherent state reads zero with every oscillator
at full amplitude — cancellation, not absence. sealed on four citations
and no new machinery: the door's mass law (a census is arrival-monotone,
incapable of darkness), the full wheel reading nothing (the uniform
crowd is the four phases summed), the lap conserving the charge (every
posture equally loud), and one loud voice at the witness. the needle and
the census obey different composition laws, and the model's whole
phenomenology lives in the gap: through the transition every count is
unchanged — N voices, all loud — and only the needle moves, lifting the
moment the uniform wheel breaks, since any three phases read exactly
minus the fourth. the drifting tail's silence in the field is the same
fact read at the tail: drifters cancel in the needle while counting full
in the census — the needle-side face of the_drifting_tail_is_outweighed.
kin with young across the roster by construction, sharing the count-law
vertex with the screen's carve of the flight before: incoherence is the
population's own darkness, the mean field a sum of amplitudes before any
census reads. the door's room and vestibule are deliberately not
identified with locked and drifting — that procession fails the lock
criterion (the door's membership is static, his lock dynamic) — so the
entry cites the mass law alone.
theorem incoherence_is_cancellation_not_absence :
    (∀ (s : List Nat × List (Nat × List Nat)) (m : Nat × List Nat),
        (admission s m).1.length + (admission s m).2.length
          = (s.1.length + s.2.length) + 1)
      ∧ (∀ z w : GInt,
          ((z.align w + z.align w.rot) + z.align w.rot.rot)
              + z.align w.rot.rot.rot = 0)
      ∧ (∀ z : GInt, ∀ w, w ∈ lapAround z → w.normSq = z.normSq)
      ∧ GInt.align ⟨1, 1⟩ (GInt.rot ⟨1, 0⟩) ≠ 0 :=
  ⟨one_click_one_count, the_four_phases_read_nothing,
   the_lap_conserves_the_charge, cancellation_not_absence.2.2⟩

partial synchronization, the model's signature fact: within the pull's
reach an oscillator locks to the field; beyond it, it drifts forever,
and the field survives because the drifters do not carry the mass.
sealed on the concentration receipt with its depth explicit — past a
computable N the far-from-the-lean words are outweighed by any named
factor — the shape bernoulli and chebyshev already read, here read as
the reason the self-consistent field has a solution at all: the locked
cluster writes the order parameter and the tail rides along. the residue
named at the seating exited by succession: the round stratum arrived
with room, and the chimera stands as its own entry now —
coherence_coexists_with_incoherence.
def the_drifting_tail_is_outweighed := @Foam.the_deviants_are_outweighed

private def lagPull : Compass → Compass → Compass
  | .n, .n => .n
  | .n, .e => .n
  | .n, .s => .w
  | .n, .w => .e
  | .e, .n => .s
  | .e, .e => .e
  | .e, .s => .e
  | .e, .w => .n
  | .s, .n => .e
  | .s, .e => .w
  | .s, .s => .s
  | .s, .w => .s
  | .w, .n => .w
  | .w, .e => .s
  | .w, .s => .n
  | .w, .w => .w

private def zipLag : List Compass → List Compass → List Compass
  | c :: cs, d :: ds => lagPull c d :: zipLag cs ds
  | [], _ => []
  | _ :: _, [] => []

private def lagRound (v : List Compass) : List Compass := zipLag v (rotateLeft v)

private def chimera : Nat → List Compass
  | 0 => [.n, .n, .n, .n, .e]
  | n + 1 => lagRound (chimera n)

private def readAt : List Compass → Nat → Option Compass
  | [], _ => none
  | c :: _, 0 => some c
  | _ :: cs, n + 1 => readAt cs n

private theorem the_lag_hears_only_the_gap :
    ∀ c d : Compass, lagPull c.step d.step = (lagPull c d).step
  | .n, .n => rfl
  | .n, .e => rfl
  | .n, .s => rfl
  | .n, .w => rfl
  | .e, .n => rfl
  | .e, .e => rfl
  | .e, .s => rfl
  | .e, .w => rfl
  | .s, .n => rfl
  | .s, .e => rfl
  | .s, .s => rfl
  | .s, .w => rfl
  | .w, .n => rfl
  | .w, .e => rfl
  | .w, .s => rfl
  | .w, .w => rfl

private theorem the_lag_lets_unison_rest : ∀ c : Compass, lagPull c c = c
  | .n => rfl
  | .e => rfl
  | .s => rfl
  | .w => rfl

private theorem the_lap_returns : ∀ n : Nat, chimera (n + 6) = chimera n
  | 0 => rfl
  | n + 1 => congrArg lagRound (the_lap_returns n)

private def OnTheLap (v : List Compass) : Prop :=
  v = chimera 0 ∨ v = chimera 1 ∨ v = chimera 2
    ∨ v = chimera 3 ∨ v = chimera 4 ∨ v = chimera 5

private theorem the_lap_carries : ∀ v, OnTheLap v → OnTheLap (lagRound v)
  | _, .inl rfl => .inr (.inl rfl)
  | _, .inr (.inl rfl) => .inr (.inr (.inl rfl))
  | _, .inr (.inr (.inl rfl)) => .inr (.inr (.inr (.inl rfl)))
  | _, .inr (.inr (.inr (.inl rfl))) => .inr (.inr (.inr (.inr (.inl rfl))))
  | _, .inr (.inr (.inr (.inr (.inl rfl)))) =>
      .inr (.inr (.inr (.inr (.inr rfl))))
  | _, .inr (.inr (.inr (.inr (.inr rfl)))) => .inl rfl

private theorem every_beat_is_on_the_lap : ∀ n : Nat, OnTheLap (chimera n)
  | 0 => .inl rfl
  | n + 1 => the_lap_carries (chimera n) (every_beat_is_on_the_lap n)

private theorem the_locked_pair_holds : ∀ v, OnTheLap v →
    ∃ x, readAt v 0 = some x ∧ readAt v 1 = some x
  | _, .inl rfl => ⟨.n, rfl, rfl⟩
  | _, .inr (.inl rfl) => ⟨.n, rfl, rfl⟩
  | _, .inr (.inr (.inl rfl)) => ⟨.n, rfl, rfl⟩
  | _, .inr (.inr (.inr (.inl rfl))) => ⟨.n, rfl, rfl⟩
  | _, .inr (.inr (.inr (.inr (.inl rfl)))) => ⟨.n, rfl, rfl⟩
  | _, .inr (.inr (.inr (.inr (.inr rfl)))) => ⟨.n, rfl, rfl⟩

the 2002 discovery, in his own title words — the community's later name
for it is the chimera: identical oscillators under one symmetric law
holding a locked part and a drifting part at once, the state that
shocked the method's own author. carved at the smallest room that
affords the blend: five voices on the ring, a lagged pull — hand-built
as the house builds accommodations, playing the role the phase lag plays
in his paper — and one six-beat lap that returns forever, on which the
front pair holds one posture at every beat while another pair walks its
gap through all four postures of the wheel: meeting, leading, opposing,
trailing. the locked pair sits frozen in the frame and the drifter
whirls through it, which is his rotating-frame picture said foam-side;
the opposing posture is a real parting, the half-turn receipt. the lag
is the content: the surveyor's field note (enumeration at the terminal,
not a receipt) is that the round's own pull refuses the blend at every
size tried — its recurrent states freeze every gap or free every gap, so
the split round is the council's two-cluster room, not this — and no
coupling on the wheel affords the blend below five voices. the coupling
function decides, which is his 2002 finding exactly.
theorem coherence_coexists_with_incoherence :
    (∀ c d : Compass, lagPull c.step d.step = (lagPull c d).step)
      ∧ (∀ c : Compass, lagPull c c = c)
      ∧ (∀ n : Nat, chimera (n + 6) = chimera n)
      ∧ (∀ n : Nat, ∃ x, readAt (chimera n) 0 = some x
            ∧ readAt (chimera n) 1 = some x)
      ∧ (∃ n x, readAt (chimera n) 2 = some x
            ∧ readAt (chimera n) 3 = some x)
      ∧ (∃ n x, readAt (chimera n) 2 = some x
            ∧ readAt (chimera n) 3 = some x.step)
      ∧ (∃ n x, readAt (chimera n) 2 = some x
            ∧ readAt (chimera n) 3 = some x.step.step ∧ x ≠ x.step.step)
      ∧ ∃ n x, readAt (chimera n) 2 = some x
            ∧ readAt (chimera n) 3 = some x.step.step.step :=
  ⟨the_lag_hears_only_the_gap,
   the_lag_lets_unison_rest,
   the_lap_returns,
   fun n => the_locked_pair_holds (chimera n) (every_beat_is_on_the_lap n),
   ⟨0, .n, rfl, rfl⟩,
   ⟨3, .e, rfl, rfl⟩,
   ⟨5, .e, rfl, rfl, the_half_turn_parts .e⟩,
   ⟨2, .n, rfl, rfl⟩⟩

the terminus, (self, pure unknown): the collective rhythm is real at the
wider seat — the needle turns, the census leans — and no single run
carries it: the book holds the full run and the empty run side by side,
so the ensemble's ratio is no member's property and a member's ratio is
no census's read. self-entrainment names the self as the thing
entrained, and whether the time a given oscillator keeps is its own or
the ensemble's is not a fact its own seat affords — readable one seat
wider, where a new remainder waits. the receipt holds the openness, and
the carrier of the common beat stays parametric here, as it did for the
clockmaker before him.
def no_run_keeps_the_collective_time := @Foam.no_run_reads_its_own_ratio

the reduction's essence typed at the pair grain: every oscillator
couples to the shared aggregate and never to another oscillator —
coupling through the third, the mean field as the beam all voices hang
from. the bridge's even lock is his self-entrainment's shape carved on
core walls (a deliberate twin with his own sealed couple: one shape, two
tables, his the exemplar and the bridge's the neutral lift), and the
chain law rides with it: two half-turned windows compose to a direct
view — parity multiplies, a two-element group — which types the two
faces of ledger-to-ledger sympathy in one stroke: even chains give
simultaneous discovery (Merton's multiples, steam-engine time), odd
chains give the hot/cold division of labor (somewhere it is always
Tuesday, the model-organism harvest). the chimera of his own 2002 record
rides one entry over as the mixed-parity witness: locked and drifting
coexisting in one population, both parities alive at once. sponsor of
the Beam stratum, jointly with Huygens.
theorem the_mean_field_is_the_beam :
    (∀ p : Compass × Compass,
        together (entrain (entrain (entrain (entrain p)))))
      ∧ ∀ p : Compass × Compass,
          window (conjugated (window p)) = entrain p :=
  ⟨the_lap_locks_together, two_windows_read_direct⟩

/-- info: 'Foam.Maps.YoshikiKuramoto.the_oscillator_is_its_phase' does not depend on any axioms -/
#guard_msgs in #print axioms the_oscillator_is_its_phase

/-- info: 'Foam.Maps.YoshikiKuramoto.the_absolute_phase_is_the_remainder' does not depend on any axioms -/
#guard_msgs in #print axioms the_absolute_phase_is_the_remainder

/-- info: 'Foam.Maps.YoshikiKuramoto.self_entrainment' does not depend on any axioms -/
#guard_msgs in #print axioms self_entrainment

/-- info: 'Foam.Maps.YoshikiKuramoto.the_order_parameter_is_a_reading' does not depend on any axioms -/
#guard_msgs in #print axioms the_order_parameter_is_a_reading

/-- info: 'Foam.Maps.YoshikiKuramoto.the_crowd_is_the_guest' does not depend on any axioms -/
#guard_msgs in #print axioms the_crowd_is_the_guest

/-- info: 'Foam.Maps.YoshikiKuramoto.incoherence_is_cancellation_not_absence' does not depend on any axioms -/
#guard_msgs in #print axioms incoherence_is_cancellation_not_absence

/-- info: 'Foam.Maps.YoshikiKuramoto.the_drifting_tail_is_outweighed' does not depend on any axioms -/
#guard_msgs in #print axioms the_drifting_tail_is_outweighed

/-- info: 'Foam.Maps.YoshikiKuramoto.coherence_coexists_with_incoherence' does not depend on any axioms -/
#guard_msgs in #print axioms coherence_coexists_with_incoherence

/-- info: 'Foam.Maps.YoshikiKuramoto.no_run_keeps_the_collective_time' does not depend on any axioms -/
#guard_msgs in #print axioms no_run_keeps_the_collective_time

/-- info: 'Foam.Maps.YoshikiKuramoto.the_mean_field_is_the_beam' does not depend on any axioms -/
#guard_msgs in #print axioms the_mean_field_is_the_beam

end Foam.Maps.YoshikiKuramoto