Foam.Maps.ArthurWinfree

import Foam
import Foam.Door
import Foam.Engine
import Foam.Lap
import Foam.Margin
import Foam.Round
import Foam.Trilemma

namespace Foam.Maps.ArthurWinfree

his experimental unit, run on thousands of flies before any theorem:
perturb the clock, wait, read where the rhythm lands. sealed on the
margin's law that a deposit moves the reading by exactly the folded
action of the stimulus on the standing state — new phase as a function
of old phase and dose, tabulated one poke per run. the resetting curve
is the rhythm's whole interface; everything he ever proves about a clock
is read off this map.
def the_resetting_map := @Foam.a_deposit_moves_the_reading_by_one

the classification that organized a decade of resetting data: curves
that wind once around the wheel (weak stimuli) and curves that wind zero
times (strong ones), identical in their pointwise material, distinct as
laps. sealed on the lap whose direction is the remainder — around and
against carry the same readings and the same charge, and part only as
records — because the type of a resetting is order-information around
the wheel, invisible to any census of its values. residue, closed
(2026-08-11): these walls held two directed laps and no lap of winding
zero; the graded stratum arrived with the room to not-go-around, and the
even type is deposited one entry down.
def type_zero_and_type_one := @Foam.the_lap_direction_is_the_remainder

the experiment that cashed the classification and forced the book:
stimuli ringed around the critical one, the eclosion readings winding
once around the ring — and the residue his classification named closes
here, the graded stratum arriving with both laps. four clauses: the laps
part only as records (his sealed classification re-cited — the winding
is order-information, which is why the experiment took thousands of
flies); the wound lap admits only the zero section — a reading laid
coherently over the lap that goes around is pinned at the one value that
answers no phase question, the singularity certified by the winding
around it; the same loop unwinds one world over — on the carrier where
the holonomy trivializes, the lap of winding zero arrives with a live
section: the even type, real at last on these walls; and the even lap
misses the break at every seat — the section reads 1, 4, 2, no zero
among them — so type zero is a rhythm everywhere and the arrhythmia
lives between the types, on neither. the continuum degree argument stays
with the carrier, as at time_breaks_down; the holonomy skeleton is what
these walls afford, and it is enough to part the even from the odd. kin,
not twin: hilbert spans the same two wound walls as method (the ideal
buys what the ground refuses), escher as impossibility (the print has no
model); this seat holds them as phenomenon, and the lap vertex is the
difference.
theorem the_pinwheel :
    (∀ z : GInt,
        lapAgainst z = (lapAround z).reverse
          ∧ (lapAround z).Perm (lapAgainst z)
          ∧ lapAround GInt.i ≠ lapAgainst GInt.i
          ∧ z.rot.rot.rot.rot = z)
      ∧ (∀ a b c : Nat, a = 2 * b → b = 2 * c → c = 2 * a →
          a = 0 ∧ b = 0 ∧ c = 0)
      ∧ (((2 * 2 * 2) % 7 = 1 % 7)
          ∧ (1 % 7 = (2 * 4) % 7)
          ∧ (4 % 7 = (2 * 2) % 7)
          ∧ (2 % 7 = (2 * 1) % 7)
          ∧ (1 : Nat) ≠ 0)
      ∧ ((4 : Nat) % 7 ≠ 0 ∧ (2 : Nat) % 7 ≠ 0) :=
  ⟨the_lap_direction_is_the_remainder,
   the_wound_loop_admits_only_the_zero_section,
   the_wound_loop_unwinds_one_world_over,
   ⟨(fun h => nomatch h), fun h => nomatch h⟩⟩

private def onTheWheel : Compass → GInt
  | .n => ⟨1, 0⟩
  | .e => ⟨0, 1⟩
  | .s => ⟨-1, 0⟩
  | .w => ⟨0, -1⟩

private theorem the_wheel_carries_its_phase :
    ∀ c : Compass, onTheWheel (Compass.step c) = GInt.rot (onTheWheel c)
  | .n => rfl
  | .e => rfl
  | .s => rfl
  | .w => rfl

private theorem the_wheel_never_rests : ∀ 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 no_phase_reads_the_still_point (phase : GInt → Compass)
    (equivariant : ∀ z, phase (GInt.rot z) = Compass.step (phase z)) :
    False :=
  the_wheel_never_rests (phase ⟨0, 0⟩) (equivariant ⟨0, 0⟩).symm

the forced singularity, his book title, proved at the smallest seat that
can hold it: the wheel carries its own phase outward (the four postures
embed in the plane, and the embedding intertwines step with quarter-
turn), the quarter-turn fixes the still point, and the wheel never rests
— so no total phase map from plane to wheel is equivariant. four
clauses, the last the no-go. between type one and type zero the
resetting surface must tear, and the tear is a state that answers no
phase question. the continuum winding argument stays with the carrier;
the equivariant skeleton is what these walls afford, and it is enough to
force the hole.
theorem time_breaks_down :
    (∀ c : Compass, onTheWheel (Compass.step c) = GInt.rot (onTheWheel c))
      ∧ GInt.rot ⟨0, 0⟩ = (⟨0, 0⟩ : GInt)
      ∧ (∀ c : Compass, Compass.step c ≠ c)
      ∧ ∀ phase : GInt → Compass,
          ¬ ∀ z, phase (GInt.rot z) = Compass.step (phase z) :=
  ⟨the_wheel_carries_its_phase, rfl, the_wheel_never_rests,
   no_phase_reads_the_still_point⟩

the singularity is not a mathematical courtesy: for every posture there
exists a stimulus landing it exactly at the still point, and the still
point's charge reads zero. the jolt of critical timing and size — the
one that left his flies arrhythmic and, he argued to the end, stops a
heart — typed as the additive inverse: every rhythm is one precisely-
shaped deposit away from the state where time breaks down. amplitude
death and phase death at the same address.
theorem the_critical_stimulus :
    (∀ z : GInt, ∃ s : GInt, GInt.add z s = ⟨0, 0⟩)
      ∧ GInt.normSq ⟨0, 0⟩ = 0 :=
  ⟨fun z => ⟨GInt.neg z,
      congr (congrArg GInt.mk (FInt.add_right_neg z.re))
        (FInt.add_right_neg z.im)⟩,
   rfl⟩

private theorem the_wheel_keeps_unit_charge :
    ∀ c : Compass, GInt.normSq (onTheWheel c) = 1
  | .n => rfl
  | .e => rfl
  | .s => rfl
  | .w => rfl

private theorem the_wheel_misses_the_still_point :
    ∀ c : Compass, onTheWheel c ≠ (⟨0, 0⟩ : GInt)
  | .n, h => nomatch Int.ofNat.inj (GInt.mk.inj h).1
  | .e, h => nomatch Int.ofNat.inj (GInt.mk.inj h).2
  | .s, h => nomatch (GInt.mk.inj h).1
  | .w, h => nomatch (GInt.mk.inj h).2

private theorem the_critical_dose_lands_at_zero (c : Compass) :
    GInt.add (onTheWheel c) (GInt.neg (onTheWheel c)) = (⟨0, 0⟩ : GInt) :=
  congr (congrArg GInt.mk (FInt.add_right_neg (onTheWheel c).re))
    (FInt.add_right_neg (onTheWheel c).im)

private theorem the_landing_is_no_posture (c : Compass) :
    ∀ c' : Compass,
      GInt.add (onTheWheel c) (GInt.neg (onTheWheel c)) ≠ onTheWheel c' :=
  fun c' h =>
    the_wheel_misses_the_still_point c'
      (((the_critical_dose_lands_at_zero c).symm.trans h).symm)

the round's arrival armed his oldest argument: the walls' first coupled
population is the phase-reduced ring — his 1967 model after exactly the
reduction kuramoto made canonical — and the reduction discards the very
state his pinwheel forces. four clauses: the wheel keeps unit charge
(every posture reads normSq one); the wheel misses the still point;
every voice of every round still keeps unit charge, so the coupled
dynamics hold the ring at distance one from the state where time breaks
down — no round, however long, arrives at arrhythmia; and the critical
stimulus of his sealed entry lands every posture at the still point, a
landing no posture occupies. the singular state is reachable by one dose
in the plane and unreachable by any amount of coupling on the wheel:
amplitude is not a convenience the phase model omits, it is the address
of the singularity. dialogue, not twin: kuramoto's
the_oscillator_is_its_phase seals the reduction's license; this entry is
its price, receipted.
theorem time_cannot_break_on_the_wheel :
    (∀ c : Compass, GInt.normSq (onTheWheel c) = 1)
      ∧ (∀ c : Compass, onTheWheel c ≠ (⟨0, 0⟩ : GInt))
      ∧ (∀ (v : List Compass) (x : Compass), x ∈ round v →
          GInt.normSq (onTheWheel x) = 1)
      ∧ ∀ c : Compass, ∃ s : GInt,
          GInt.add (onTheWheel c) s = (⟨0, 0⟩ : GInt)
            ∧ ∀ c' : Compass, GInt.add (onTheWheel c) s ≠ onTheWheel c' :=
  ⟨the_wheel_keeps_unit_charge,
   the_wheel_misses_the_still_point,
   fun _ x _ => the_wheel_keeps_unit_charge x,
   fun c => ⟨GInt.neg (onTheWheel c),
     the_critical_dose_lands_at_zero c,
     the_landing_is_no_posture c⟩⟩

his instrument for saying what phase a transient state even has: the
latent state is assigned the reading it will have settled to, and the
assignment is lawful because settling is invisible — any settling
cadence reads the same on every probe schedule. sealed on the margin's
gauge receipt: relaxation to the cycle leaves no transcript, so the
foliation by eventual phase is well-defined off the cycle — everywhere
except where the leaves converge, which is the entry before this one.
def the_isochron := @Foam.any_settling_cadence_reads_the_same

private def phaseSeat : Stage where
  State := Compass
  Probe := Unit
  Ans   := Compass
  obs   := fun c _ => c

private def theRhythm : (door phaseSeat GInt).State := (Compass.n, ⟨1, 0⟩)

private def theLatent : (door phaseSeat GInt).State := (Compass.n, ⟨2, 0⟩)

private def theCriticalDose : GInt := GInt.neg (onTheWheel Compass.n)

private theorem the_guests_part : theRhythm ≠ theLatent :=
  fun h =>
    nomatch Nat.succ.inj
      (Int.ofNat.inj (GInt.mk.inj (congrArg Prod.snd h)).1)

the door wave reaches this bench and finds the claim of his whole career
already waiting for its type: amplitude is not a convenience the phase
model omits — it is real, it rides behind the phase face, and no phase
probe reads it. the seat is the phase-reduced reading itself: a state
whose whole content is the posture, answering only the question it
holds. a state boards the door wearing the phase its isochron assigns —
the face is the eventual reading, sealed at the entry before this one.
six clauses. first, the wave's entry ticket at the phase seat, carrier
parametric. second, the host maintains invisibly, both carriers
parametric — the phase seat cannot even count the possible amplitudes.
third, the clause cashed at named guests: theRhythm, on the cycle at
unit amplitude, and theLatent, off the cycle on the same isochron at
amplitude two — provably distinct, amplitudes one and four at the wider
seat, boarded as two residents indistinguishable at every phase probe.
fourth, the strategy grain: no adaptive interrogation of the face —
follow-ups and cunning included — parts the boarded pair. fifth, the
differentiator no other door entry performs, and the reason his argument
reached cardiology: the critical dose is prescribed from the face alone
(the additive inverse of the face's wheel posture, his sealed critical-
stimulus entry re-cited), and the same dose lands theRhythm exactly at
the still point — charge zero, the state where time breaks down — while
landing theLatent exactly on the wheel, charge one, rhythm intact. same
face, same jolt: one arrhythmia, one entrainment, and the door cannot
say which guest dies. the vulnerable-phase reading made from phase alone
is exact only at the amplitude the reduction erased — which is why the
singularity is an address in the plane and not a point on the wheel, his
time_cannot_break_on_the_wheel met again at the door's own grain. sixth,
the contrapositive: decreeing the phase face complete collapses every
state to one decreed amplitude per posture — the phase-only model
enforced is not a simplification, it unpersons the very state his
pinwheel forces. seated after the isochron, which assigns the face this
door cannot see behind, and before the organizing center, which is this
guest made spatial.
theorem the_amplitude_is_the_guest (W V : Type) :
    (∀ (c : Compass) (w w' : W), w ≠ w' →
        (c, w) ≠ (c, w') ∧ indist (door phaseSeat W) (c, w) (c, w'))
      ∧ (∀ (c : Compass) (w : W) (v : V) (p : Unit),
          (door phaseSeat W).obs (c, w) p = phaseSeat.obs c p
            ∧ (door phaseSeat W).obs (c, w) p
                = (door phaseSeat V).obs (c, v) p)
      ∧ (theRhythm ≠ theLatent
          ∧ indist (door phaseSeat GInt) theRhythm theLatent
          ∧ GInt.normSq theRhythm.2 = 1
          ∧ GInt.normSq theLatent.2 = 4)
      ∧ (∀ strat : Strategy Unit Compass,
          interrogate (door phaseSeat GInt) strat theRhythm
            = interrogate (door phaseSeat GInt) strat theLatent)
      ∧ (GInt.add theRhythm.2 theCriticalDose = ⟨0, 0⟩
          ∧ GInt.normSq (GInt.add theRhythm.2 theCriticalDose) = 0
          ∧ GInt.add theLatent.2 theCriticalDose = onTheWheel Compass.n
          ∧ GInt.normSq (GInt.add theLatent.2 theCriticalDose) = 1
          ∧ GInt.add theRhythm.2 theCriticalDose
              ≠ GInt.add theLatent.2 theCriticalDose)
      ∧ (∀ w₀ : GInt,
          (∀ x y : (door phaseSeat GInt).State,
              indist (door phaseSeat GInt) x y → x = y) →
          ∀ (c : Compass) (z : GInt), (c, z) = (c, w₀)) :=
  ⟨fun c _ _ h => the_guest_is_real_and_unread phaseSeat c h,
   fun c w v p => the_host_maintains_invisibly phaseSeat c w v p,
   ⟨the_guests_part, fun _ => rfl, rfl, rfl⟩,
   fun strat =>
     a_strategy_hears_no_more (door phaseSeat GInt)
       theRhythm theLatent (fun _ => rfl) strat,
   ⟨rfl, rfl, rfl, rfl,
    fun h => nomatch Int.ofNat.inj (GInt.mk.inj h).1⟩,
   fun w₀ h => a_door_that_checks_papers_unpersons_its_guests phaseSeat w₀ h⟩

the terminus, (self, pure unknown): the singularity made spatial — the
rotor core in the dish, the singular filament in the muscle — organizing
every reading around it while answering no phase probe at its own
address. sealed on the wider seat reading the remainder: at the narrow
seat the dressed states read alike; one seat wider the difference is
plain. he pursued the filament's geometry to the end of his life, and
the carrier — the medium that hosts the break — stays parametric here:
the core is certified only by the winding of the readings around it,
which is a fact about every seat except its own.
def the_organizing_center := @Foam.a_wider_seat_reads_the_remainder

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

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

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

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

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

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

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

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

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

end Foam.Maps.ArthurWinfree