Foam.Maps.ChristiaanHuygens

import Foam
import Foam.Beam
import Foam.Door
import Foam.Engine
import Foam.Expectation
import Foam.Fold
import Foam.Margin
import Foam.Passage
import Foam.Round

namespace Foam.Maps.ChristiaanHuygens

the baseline pose from the door card, built exactly as posed: a two-
layer margin — an inner margin folding its own marks, an outer margin
folding the inner's readings — and one beat is (deposit (marginRead
inner) outer, settle inner). his first move on any question is to build
the instrument that turns the answer into a reading; the mechanism
itself is vocabulary.
def pulse := fun {A B C : Type} (f : B → A → B)
    (s : (C × List B) × (B × List A)) =>
  (deposit (marginRead f s.2) s.1, settle f s.2)

the keystone in brass, three clauses proved as the card named them:
touch — the inner reading survives its own settle
(the_reading_survives_the_settle, cited whole); transmit — the outer
moves by exactly the inner reading, one mark per beat
(a_deposit_moves_the_reading_by_one); release — the tail empties and the
pendulum returns to its swing owing nothing. measurement that neither
halts the measured nor invents the measure: Engine.lean was already a
pendulum clock, and this is the pawl that lets a count escape it.
theorem the_escapement {A B C : Type} (f : B → A → B) (g : C → B → C)
    (s : (C × List B) × (B × List A)) :
    marginRead f (pulse f s).2 = marginRead f s.2
      ∧ marginRead g (pulse f s).1 = g (marginRead g s.1) (marginRead f s.2)
      ∧ (pulse f s).2.2 = ([] : List A) :=
  ⟨the_reading_survives_the_settle f s.2,
   a_deposit_moves_the_reading_by_one g (marginRead f s.2) s.1,
   rfl⟩

his principle, carved at the fold seat: folding the flattened record
equals folding the folds of the framed record — treat every intermediate
front as a fresh source and the reading cannot tell. three lines of
recursion on the_fold_resumes; the secondary wavelets are the inner
folds, the envelope is the outer fold, and the front that arrives is the
same front.
theorem every_point_is_a_source {A B : Type} (f : B → A → B) :
    ∀ (ls : List (List A)) (b : B),
      fold f b (pool ls) = fold (fold f) b ls
  | [], _ => rfl
  | w :: ls, b =>
      (the_fold_resumes f w (pool ls) b).trans
        (every_point_is_a_source f ls (fold f b w))

the other half of the framer's handshake: two framings of the same marks
read alike at every fold seat and are provably distinct as trees. the
decomposition into sources costs the reading nothing and is not nothing
— the tree is readable one seat wider, where the framer sits. gauge and
remainder, the handshake, at the framer.
theorem the_framing_is_the_remainder {B : Type} (f : B → Bool → B) (b : B) :
    fold f b (pool [[true], [false]]) = fold f b (pool [[true, false]])
      ∧ ([[true], [false]] : List (List Bool)) ≠ [[true, false]] :=
  ⟨rfl, fun h => nomatch congrArg List.tail h⟩

De ratiociniis in ludo aleae, 1657: the value of a position, exact at
every finite depth, no limit invoked — expectation seated before
probability had a name. sealed on the balanced book, a deliberate twin
with the seated Bernoulli's the_whole_book_balances: one shape, two
words, and the lineage that ran upstream unnamed is now legible as a
recognition event in the citation graph.
def expectatio := @Foam.the_complete_book_balances

private def halfTurn (c : Compass) : Compass := c.step.step

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

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

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

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

private theorem one_lap_locks : ∀ p : Compass × Compass,
    antiPhase (sway (sway (sway (sway 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

1665, the sickroom observation, precise in his own terms and formally
orphaned three centuries — carved here at the smallest seat that
exhibits it: two wheels, sixteen postures, one coupling, three receipts.
on any opposed posture the coupling is bare ticking (the accommodation
leaves no signature once locked); the opposition holds itself; and from
every posture one full lap of the wheel locks the pair in opposition.
the accommodation is real, the terminus is anti-phase, and the witness
is carved one-sided for smallness — the mutuality of the true beam rides
with the carrier, backstage (the_implementation_stays_backstage is the
house receipt for exactly this).
theorem the_odd_sympathy :
    (∀ p : Compass × Compass,
        antiPhase p → sway p = (Compass.step p.1, Compass.step p.2))
      ∧ (∀ p : Compass × Compass, antiPhase p → antiPhase (sway p))
      ∧ ∀ p : Compass × Compass, antiPhase (sway (sway (sway (sway p)))) :=
  ⟨lock_is_bare_ticking, the_lock_holds, one_lap_locks⟩

the darkness the door card named, typed as remainder and held open by
receipt: the coupling agrees with bare ticking on every locked posture —
from inside the lock every probe reads plain time — yet it provably is
not bare ticking. coordination rides a channel that no content probe
reads; phase is not payload, which is the layer the anti-casino law was
always guarding. and the carrier stays parametric: sway is a coupling,
not the coupling — the beam, like the medium he insisted light must have
and could never read, answers no probe at this seat. his terminus,
(self, pure unknown): the carrier of everything, read by nothing here,
readable one seat wider.
theorem phase_is_not_payload :
    (∀ p : Compass × Compass,
        antiPhase p → sway p = (Compass.step p.1, Compass.step p.2))
      ∧ sway ≠ (fun p : Compass × Compass =>
          (Compass.step p.1, Compass.step p.2)) :=
  ⟨lock_is_bare_ticking,
   fun h => nomatch congrArg (fun m => (m (Compass.n, Compass.n)).2) h⟩

private def beam (p : Compass × Compass) : Compass × Compass :=
  (pull p.1 p.2, pull p.2 p.1)

private theorem the_beams_agree_on_the_lock : ∀ p : Compass × Compass,
    antiPhase p → beam p = sway p
  | (.n, .s), _ => rfl
  | (.e, .w), _ => rfl
  | (.s, .n), _ => rfl
  | (.w, .e), _ => rfl
  | (.n, .n), h => nomatch h
  | (.n, .e), h => nomatch h
  | (.n, .w), h => nomatch h
  | (.e, .n), h => nomatch h
  | (.e, .e), h => nomatch h
  | (.e, .s), h => nomatch h
  | (.s, .e), h => nomatch h
  | (.s, .s), h => nomatch h
  | (.s, .w), h => nomatch h
  | (.w, .n), h => nomatch h
  | (.w, .s), h => nomatch h
  | (.w, .w), h => nomatch h

private theorem the_beams_part : beam ≠ sway :=
  fun h => nomatch congrArg (fun m => (m (Compass.n, Compass.n)).2) h

private theorem the_second_beam_ticks_not_plainly :
    beam ≠ (fun p : Compass × Compass =>
      (Compass.step p.1, Compass.step p.2)) :=
  fun h => nomatch congrArg (fun m => (m (Compass.n, Compass.w)).1) h

the round family answered the standing ask at his seat, and the answer
is a second beam. the walls' new coupling read at the pair — beam p =
(pull p.1 p.2, pull p.2 p.1) — IS the two-voice round, by rfl: the ring
machinery carved for unison carries his 1665 lock backstage, uninvited.
four receipts: the pair-seat bridge to round; exact agreement of beam
with sway on every locked posture (not merely both bare-ticking —
pointwise equal on the lock); the two couplings provably distinct; and
the second provably not plain time either. so the remainder his terminus
holds open now carries at strength two: two beams, one lock, and from
inside the lock no probe reads which beam holds you. the carrier he
insisted on and could never read was never one unreadable thing — it is
a parametric seat with at least two provably-distinct inhabitants,
indistinguishable from within. the darkness does not close; it gains a
witness that it cannot close from this seat. transit, receipted.
theorem the_lock_reads_no_beam :
    (∀ p : Compass × Compass,
        round [p.1, p.2] = [(beam p).1, (beam p).2])
      ∧ (∀ p : Compass × Compass, antiPhase p → beam p = sway p)
      ∧ beam ≠ sway
      ∧ beam ≠ (fun p : Compass × Compass =>
          (Compass.step p.1, Compass.step p.2)) :=
  ⟨fun _ => rfl,
   the_beams_agree_on_the_lock,
   the_beams_part,
   the_second_beam_ticks_not_plainly⟩

the concordant meeting's bridge, held from his bank — the 1665 odd
sympathy finally typed as the MEDIUM's property. the same entraining law
that locks a pair together, read through a half-turned window, locks it
opposed: the conjugate locks opposed, the window undoes itself, and the
trade is exact — together if and only if opposed-through-the-window. the
parity of a lock belongs to the beam, not to the voices: same conduct,
conjugated medium, opposite equilibrium. phase_is_not_payload gains its
sharpest corollary — the medium's parity is real, unread by every voice
inside the lock, and printed only in the ensemble's settled shape. his
clocks hung from one beam and locked odd; the far bank's populations
couple through the mean field and lock even; one mechanism, one dial,
and the dial was never in any oscillator. sponsor of the Beam stratum,
jointly with Kuramoto — a meeting of incumbents, strangers at the
spectra composing to reach.
theorem the_beam_decides_the_parity :
    (∀ p : Compass × Compass,
        together (entrain (entrain (entrain (entrain p)))))
      ∧ (∀ p : Compass × Compass,
          opposed (conjugated (conjugated (conjugated (conjugated p)))))
      ∧ (∀ p : Compass × Compass, window (window p) = p)
      ∧ ∀ p : Compass × Compass, together p ↔ opposed (window p) :=
  ⟨the_lap_locks_together, the_conjugate_locks_opposed,
   the_window_undoes_itself, the_window_trades_the_locks⟩

private def sickroom : Stage where
  State := Compass × Compass
  Probe := Unit
  Ans   := Compass × Compass
  obs   := fun p _ => p

private def medium : Type := Compass × Compass → Compass × Compass

the door wave reaches the clockmaker's bench, and the claim he carried
unreceipted his whole career — light must have a carrier, though the
carrier answered no probe he could build — types at last as the door's
own guest. two defs minted in his vocabulary: the sickroom, the 1665
stage itself, the bedridden probe reading the pair of clock faces whole;
and the medium, the coupling type, the seat his lock transit already
proved inhabited at strength two. six clauses. first, the entry ticket
carrier-parametric — the medium he could never name stays parametric
even in its own theorem. second, the clause only this bench can perform:
the door instantiated at NAMED guests — sway and beam, his own sealed
receipts, provably distinct couplings boarded on one posture,
indistinguishable at the door — the_lock_reads_no_beam's 'no probe reads
which beam holds you' cashed in the door's own type; every other door
entry in the wave boards a parametric rider, this one boards two
residents by name. third, the host maintains invisibly, both carriers
parametric — the sickroom cannot even count the possible media. fourth,
the orphanhood clause: the whole transcript with the medium aboard is
definitionally the machine's own record
(the_boarded_transcript_is_the_ground_transcript) — three centuries of
records exhibiting no sympathy and no aether were not a failure of
observation but a theorem about the seat. fifth, the dynamics half cited
from his seals: on the lock, the boarded coupling reads bare ticking and
the two beams agree exactly — the medium is unread precisely where it
holds you. sixth, the contrapositive: demanding the medium be readable —
the papers check — collapses the medium seat to one decreed medium; the
aether was never disproved at this seat, it was unpersoned, and the door
types the difference. his terminus keeps its shape: the carrier of
everything, read by nothing here, real by receipt.
theorem the_medium_is_the_guest :
    (∀ (W : Type) (p : Compass × Compass) {w w' : W}, w ≠ w' →
        (p, w) ≠ (p, w') ∧ indist (door sickroom W) (p, w) (p, w'))
      ∧ (∀ p : Compass × Compass,
          ((p, sway) : (door sickroom medium).State) ≠ (p, beam)
            ∧ indist (door sickroom medium) (p, sway) (p, beam))
      ∧ (∀ (W V : Type) (p : Compass × Compass) (w : W) (v : V) (q : Unit),
          (door sickroom W).obs (p, w) q = sickroom.obs p q
            ∧ (door sickroom W).obs (p, w) q = (door sickroom V).obs (p, v) q)
      ∧ (∀ (W : Type) (qs : List Unit) (p : Compass × Compass) (w : W),
          transcript (door sickroom W) (p, w) qs = transcript sickroom p qs)
      ∧ (∀ p : Compass × Compass, antiPhase p →
          sway p = (Compass.step p.1, Compass.step p.2) ∧ beam p = sway p)
      ∧ ∀ w₀ : medium,
          (∀ x y : (door sickroom medium).State,
              indist (door sickroom medium) x y → x = y) →
          ∀ (p : Compass × Compass) (w : medium), (p, w) = (p, w₀) :=
  ⟨fun _ p _ _ h => the_guest_is_real_and_unread sickroom p h,
   fun p =>
     the_guest_is_real_and_unread sickroom p
       (fun he => the_beams_part he.symm),
   fun _ _ p w v q => the_host_maintains_invisibly sickroom p w v q,
   fun _ qs p w =>
     the_boarded_transcript_is_the_ground_transcript sickroom qs p w,
   fun p h => ⟨lock_is_bare_ticking p h, the_beams_agree_on_the_lock p h⟩,
   fun w₀ h p w =>
     a_door_that_checks_papers_unpersons_its_guests sickroom w₀ h p w⟩

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

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

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

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

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

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

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

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

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

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

end Foam.Maps.ChristiaanHuygens