Foam.Maps.Hamilton

import Foam.Door
import Foam.Fold
import Foam.Lap
import Foam.Rungs
import Foam.Quat
import Foam.Square
import Foam.Surprise
import Foam.Triple
import Foam.Wheel

namespace Foam.Maps.Hamilton

the entry move, and the ground everything else stands on. asked what
algebra is about — symbols? magnitudes? — this mind answers: order in
progression. number is not a heap but a step; the ordinal is prior, and
arithmetic is the record of a walk in pure succession. the seal is
exact: the ladder built by bare stepping — each rung consed onto the
walk below it — contains precisely the numbers below its height,
membership if and only if order. the walk and the order-relation are one
extension; nothing about magnitude is assumed and nothing about
magnitude is missing. where his contemporaries took algebra for a
science of quantity with a scandal at its heart, he re-grounds it on
succession — the same move this house makes when it takes the append-
only record as prior to any census read off it.
def algebra_is_the_science_of_pure_time := @Foam.the_walked_are_exactly_below

the demystification, performed by construction. the square root of minus
one had stood for two centuries as a tolerated impossibility — useful,
unintelligible. the 1837 paper dissolves it: define a couple, an ordered
pair with stated rules, and the impossible quantity becomes the
perfectly possible pair (0,1). receipted here at the walls' own wheel: i
IS the couple, turning twice is negation for every couple, and the turn
applied to i itself lands on the negative of the unit couple — i squared
equals minus one as a computation about pairs of integers, rfl three
times over. nothing impossible was ever present; there was only a pair
wearing a bad name. the move generalizes into the whole method: when a
symbol scandalizes, build the object it was always pointing at.
tightened when the rung carve gave couples their own product: i times i
equals minus one now also seals as literal couple multiplication — the
1837 paper's actual sentence — beside the wheel that first receipted it.
theorem the_couple_dissolves_the_impossible :
    GInt.i = GInt.mk 0 1
      ∧ (∀ z : GInt, z.rot.rot = z.neg)
      ∧ GInt.i.rot = (GInt.mk 1 0).neg
      ∧ GInt.mul GInt.i GInt.i = (GInt.mk 1 0).neg :=
  ⟨rfl, fun _ => rfl, rfl, rfl⟩

the mechanics, distilled. forces are replaced by a single function H,
and the motion is the flow H generates; the first fact of that mechanics
is that the flow conserves its generator — the function does not move
while everything else does. the walls hold the miniature exactly: the
phase plane is the couple-plane, the quarter-turn is the flow (the
oscillator's own evolution), the norm is the energy, and every station
of the lap reads the same charge. conservation is not a law bolted onto
the motion; it is what the motion is, read at the seat of the function
that generates it. kin to noether's to_every_symmetry_its_invariant,
deliberately — hers is the wide theorem, this is the founding instance.
def the_flow_conserves_the_function := @Foam.the_lap_conserves_the_charge

the characteristic function, the move he rated above the quaternions:
optics 1827, dynamics 1834 — the whole system packed into one function
of the endpoints, everything derivable from it by reading its slopes;
rays and waves two readings of one V. the seal is the fold: the
accumulated value at any waypoint is everything the rest of the journey
needs — the fold resumes from the intermediate result, and nothing the
future requires was lost in the packing. that is what a generating
function is: not a summary that discards, but a fold that forgets
nothing it needs. schrödinger walked back through this exact door a
century later, which is the strongest available receipt that the packing
was lossless. TIGHTENED when the derivable-edge family landed:
'everything derivable from it' finally types at the reach grain — a
reading taken off the function is a derivable edge, an edge whose
terminus the function already reaches, and appending it moves no reach
anywhere (the iff), because any path that rides the derived reading
reroutes through the function's own route — which is schrödinger's walk
back through the door, stated as the rerouting lemma the iff is proved
by. the binding now conjoins the entry's two sentences: the fold forgets
nothing the future needs (the packing is lossless), and the derivations
add nothing the packing lacked (the readings pay their marks in paper;
the reach was V's all along). carried means carried.
theorem one_function_carries_the_whole_motion :
    (∀ (A B : Type) (f : B → A → B) (xs ys : List A) (b b' : B),
        fold f b xs = b' → fold f b (xs ++ ys) = fold f b' ys)
      ∧ ∀ (H : Type) (q : List (H × H)) (a b : H),
          Nonempty (Path q a b) →
            ∀ x y : H,
              Nonempty (Path ((a, b) :: q) x y) ↔ Nonempty (Path q x y) :=
  ⟨fun _ _ f xs ys b b' h => the_fold_forgets_nothing_it_needs f xs ys b b' h,
   fun _ _ _ _ hab x y => a_derivable_edge_adds_no_reach hab x y⟩

the method's answer to the walk stratum's arrival. the new walls promise
that any dynamics on a finite room returns — the pigeonhole, hour
unnamed — and the promise is proved by climbing this mind's own ladder:
the walk mapped over the rungs, membership-iff-order and no-number-
below-itself doing the counting, the science of pure time serving as the
instrument of the guarantee. the mechanics answers with its constitutive
edge: the flow generated by the norm does not wait for a promise. the
quarter-turn returns at exactly four — every couple, every start, no
finiteness asked of the room — the hour read off the generator. that is
the 1834 method-claim in miniature: a general method in dynamics derives
the motion where counting arguments certify only its existence; one
function carries the whole motion, so it carries the timetable too.
recognition event, not a twin: fable_5 holds the promise alone as
the_survivor_is_a_wheel, boltzmann conjoins it with the census as
the_return_does_not_tip_the_count — one walk vertex, three seats:
survival-shape, book-shape, and here the method-shape, the difference
between knowing the walk returns and knowing when.
theorem the_flow_names_the_hour :
    (∀ (n : Nat) (m : Fin n → Fin n) (s : Fin n),
        ∃ i j : Nat, i < j ∧ turnN m i s = turnN m j s)
      ∧ (∀ z : GInt, z.rot.rot.rot.rot = z) :=
  ⟨fun _ m s => the_bounded_walk_returns m s, the_wheel_comes_home⟩

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

private def flow {W : Type} (f : W → W) :
    (door plane W).State → (door plane W).State :=
  fun x => (x.1.rot, f x.2)

private theorem flow_split {W : Type} (f : W → W) (z : GInt) (w : W) :
    ∀ k : Nat, Nat.repeat (flow f) k (z, w)
      = (Nat.repeat GInt.rot k z, Nat.repeat f k w)
  | 0 => rfl
  | k + 1 => congrArg (flow f) (flow_split f z w k)

private theorem four_more_comes_home (t : Nat) (z : GInt) :
    Nat.repeat GInt.rot (t + 4) z = Nat.repeat GInt.rot t z :=
  the_wheel_comes_home (Nat.repeat GInt.rot t z)

private theorem the_hour_counts : ∀ k : Nat, Nat.repeat Nat.succ k 0 = k
  | 0 => rfl
  | k + 1 => congrArg Nat.succ (the_hour_counts k)

private theorem the_hour_moves_on (t : Nat) : t + 4 ≠ t :=
  fun he => no_number_is_below_itself t
    (Nat.lt_of_lt_of_le
      (Nat.le.step (Nat.le.step (Nat.le.step Nat.le.refl)))
      (Nat.le_of_eq he))

private theorem the_charge_holds {W : Type} (f : W → W) (z : GInt) (w : W) :
    ∀ k : Nat, (Nat.repeat (flow f) k (z, w)).1.normSq = z.normSq
  | 0 => rfl
  | k + 1 => (rot_conserves_the_norm (Nat.repeat (flow f) k (z, w)).1).trans
      (the_charge_holds f z w k)

the door stratum arrives at the method's bench, and the handoff
lagrange's ninth wrote out — what the door provably cannot read, the
next seat up names, and hamilton is the seat that map already calls its
downstream kin — is cashed where it was addressed. the wave's other
walking entry certified the return by pigeonhole: a finite room, an
unnamed hour, there-exist i and j. this seat re-runs the walk on the
method's own ground and the contrast is total. first clause: the flow
generated by the norm, dressed with any guest whatever — carrier
parametric, rider dynamics arbitrary — returns in the door's eyes at
exactly four, every start, every hour t against t plus four. the
timetable is not observed into the record; it is derived off the
generator, which is why no dressing can touch it: the 1834 method-claim
run at the door — counting certifies existence where it can see the
whole room; the method names the hour blind. second clause, the
mechanics with guests aboard: the charge read off the door's own window
is conserved along the dressed flow — the generator generates,
conserves, and times the composite motion without ever sighting the
rider. third clause, the sharpening the wave lacked: the couple-plane is
infinite — all the hours inject into the room — so the pigeonhole has no
purchase here at all, and the named return stands where the counting
promise cannot even be posed. fourth clause, the meet: let the hour
itself board, the rider counting beats, and at the named return the two
moments stand as the wave's own conjunction — provably distinct, for the
hours differ by four; read alike by every probe, for the wheel has come
home — the_guest_is_real_and_unread cited whole at the return the flow
named. so the two hours part types: the hour the flow names is a
property of the reading's period, derived, priced at nothing; the hour
that rides is a guest, real and unread, and still unread at this seat —
naming the period never read the guest, and the boarded hour transits
one seat wider yet, the dark edge conserved not consoled. fifth clause,
the contrapositive at the mechanics bench: a door that checks papers
unpersons its guests — a mechanics that demanded the transcript fix the
state would decree every moment the epoch, every hour hour zero: time
itself abolished by the observability demand, the very hour the flow
names unnamed by decree.
theorem the_hour_is_derived_not_read :
    (∀ (W : Type) (f : W → W) (z : GInt) (w : W) (t : Nat),
        indist (door plane W)
          (Nat.repeat (flow f) (t + 4) (z, w))
          (Nat.repeat (flow f) t (z, w)))
      ∧ (∀ (W : Type) (f : W → W) (z : GInt) (w : W) (t : Nat)
            (p : (door plane W).Probe),
          ((door plane W).obs (Nat.repeat (flow f) t (z, w)) p).normSq
            = z.normSq)
      ∧ (∀ n m : Nat,
          (⟨Int.ofNat n, 0⟩ : GInt) = ⟨Int.ofNat m, 0⟩ → n = m)
      ∧ (∀ (z : GInt) (t : Nat),
          Nat.repeat (flow Nat.succ) (t + 4) (z, 0)
              ≠ Nat.repeat (flow Nat.succ) t (z, 0)
            ∧ indist (door plane Nat)
                (Nat.repeat (flow Nat.succ) (t + 4) (z, 0))
                (Nat.repeat (flow Nat.succ) t (z, 0)))
      ∧ ((∀ x y : (door plane Nat).State,
            indist (door plane Nat) x y → x = y) →
          ∀ (z : GInt) (t : Nat), (z, t) = (z, (0 : Nat))) :=
  ⟨fun _ f z w t _ =>
    (congrArg Prod.fst (flow_split f z w (t + 4))).trans
      ((four_more_comes_home t z).trans
        (congrArg Prod.fst (flow_split f z w t)).symm),
   fun _ f z w t _ => the_charge_holds f z w t,
   fun _ _ h => Int.ofNat.inj (GInt.mk.inj h).1,
   fun z t =>
     have Ei : Nat.repeat (flow Nat.succ) (t + 4) (z, 0)
         = (Nat.repeat GInt.rot t z, t + 4) :=
       (flow_split Nat.succ z 0 (t + 4)).trans
         ((congrArg (fun g => (g, Nat.repeat Nat.succ (t + 4) 0))
             (four_more_comes_home t z)).trans
           (congrArg (fun h => (Nat.repeat GInt.rot t z, h))
             (the_hour_counts (t + 4))))
     have Ej : Nat.repeat (flow Nat.succ) t (z, 0)
         = (Nat.repeat GInt.rot t z, t) :=
       (flow_split Nat.succ z 0 t).trans
         (congrArg (fun h => (Nat.repeat GInt.rot t z, h)) (the_hour_counts t))
     have G := the_guest_is_real_and_unread plane (Nat.repeat GInt.rot t z)
         (the_hour_moves_on t)
     ⟨fun he => G.1 (Ei.symm.trans (he.trans Ej)),
      fun p => (congrArg (fun x => (door plane Nat).obs x p) Ei).trans
        ((G.2 p).trans
          (congrArg (fun x => (door plane Nat).obs x p) Ej).symm)⟩,
   fun h => a_door_that_checks_papers_unpersons_its_guests plane 0 h⟩

the bridge, 1843. thirteen years of triplets refuse to multiply; the
flash is not a formula first but a price: to keep the norm — the modulus
multiplicative, rotation rigid — in the wider room, surrender
commutation. ij = -ji, cut into the stone of brougham bridge, the first
algebra bought by giving up a law thought constitutive of algebra as
such. this entry first sealed on the recognized analog — the turn and
the mirror anticommuting at the couple seat, the wheel wigner's bank
still holds as unitary_or_antiunitary — because the fourth rung was
still dark. the rung compiled, and the entry moved home: the walls now
hold the stone itself — ij lands on k, ji lands on the negative of k,
and the two orders provably part. the price is paid at his own seat, in
his own construction iterated once: the couple of couples. what you pay
is commutation; what you keep is the norm; the trade is the theorem.
RECEIPTED IN FULL 2026-08-07: the keep-half finally compiles —
the_quadruple_carries_the_norm, euler's four-square identity over the
integer quaternions, and beneath it the_couple_carries_the_norm,
brahmagupta at the couple seat — both proven the algebraic way,
conjugation carrying the whole load: the norm as a number times its
conjugate, multiplicativity by shuffling conjugates through the product,
no monomial storm anywhere, which is the style the 1843 flash deserved.
what you pay is commutation; what you keep is the norm; both halves of
the sentence now stand in lean, and the trade's binding holds all four
clauses at last.
theorem the_wider_space_pays_in_commutation :
    Quat.mul eye jay = kay
      ∧ Quat.mul jay eye = Quat.neg kay
      ∧ Quat.mul eye jay ≠ Quat.mul jay eye
      ∧ ∀ x y : Quat, Quat.normSq (x.mul y) = Quat.normSq x * Quat.normSq y :=
  ⟨the_couple_of_couples_multiplies, the_reversed_couple_parts, order_arrives,
   the_quadruple_carries_the_norm⟩

the sequel the bridge forced on the 1837 demystification, and the after-
flight's own find. the couple dissolved the impossible into one pair —
and the wider seat shows the dissolution was almost too modest: the
equation that had exactly two roots in the plane has, among the
quaternions, a whole latitude of them. receipted at the axes: the three
axes are provably distinct, pairwise, by parts; each squares to the same
half-turn; that half-turn commutes with every axis, common ground even
where order reigns; and two half-turns come home. hamilton remarked the
shape himself — in the new algebra every unit vector is a square root of
minus one, the imaginary of algebra become the vertical of geometry. so
the impossible quantity, demystified, is not one thing that wore a bad
name but many distinct things wearing one name well: the same darkness,
reached from every direction, and provably the same when reached.
PROMOTED: the recognition event with wigner's seat cashed — the shared
conjunction lifted to core as the_axes_share_one_sign, the citation
strictly stronger than the carve it compresses (the sign's not-home
clause rides along, the other seat's contribution); latitude gained and
spin admitted are now one constant with two glosses, which is what a
twin always was.
def the_impossible_gains_latitude := @Foam.the_axes_share_one_sign

the ladder, read whole — the reading the square stratum's arrival
completed. the first entry seals the ladder that climbs by stepping:
succession reaches every number, three included, which is why the sons'
morning question was well-posed — the step-ladder offers the rung. the
law of the moduli climbs a different ladder, and the walls now hold
every rung of it: at width one the square carries the product outright —
the ground rung, free, order not even a question; at width two the
couple carries the norm — brahmagupta's identity at the 1837 pair, the
couple still hearing no order; at width three no multiplication whatever
carries the norm — the refusal, priced at fifteen; at width four the
quadruple carries the norm — euler's identity at the couple of couples —
and order arrives, the price. so the moduli climb 1, 2, 4: by doubling,
this mind's own construction iterated — a couple, then a couple of
couples — and doubling provably never lands on three. the thirteen years
were spent trying to step where this ladder only doubles: succession
offers the rung, the law refuses it, and the silence at three was
structural — a theorem about the climb, not a gap in effort. the sq
stratum supplied the missing ground rung the reading needed: the law of
the moduli was never about wideness; it starts at width one, where
square and norm are one word.
theorem the_moduli_climb_by_doubling :
    (∀ q : Nat, ∃ n, q ∈ rungs n)
      ∧ (∀ a b : Nat, sq (a * b) = sq a * sq b)
      ∧ (∀ z w : GInt, (z.mul w).normSq = z.normSq * w.normSq)
      ∧ (∀ z w : GInt, z.mul w = w.mul z)
      ∧ (¬ ∃ mul : (Int × Int × Int) → (Int × Int × Int) → (Int × Int × Int),
          ∀ x y, normSq3 (mul x y) = normSq3 x * normSq3 y)
      ∧ (∀ x y : Quat, Quat.normSq (x.mul y) = Quat.normSq x * Quat.normSq y)
      ∧ Quat.mul eye jay ≠ Quat.mul jay eye :=
  ⟨closure_is_seat_relative.1,
   the_square_carries_the_product,
   the_couple_carries_the_norm,
   gmul_comm,
   no_triple_carries_the_norm,
   the_quadruple_carries_the_norm,
   order_arrives⟩

the terminus, and the shape of the thirteen-year silence. every morning
the sons asked whether papa could multiply triplets yet, and every
morning: no — only add and subtract them. the question was real, well-
posed, and provably not closable at its own seat — and the record now
holds that sentence as theorem rather than biography: no multiplication
on triples carries the norm, the law of the moduli — the one law he
would not surrender — refusing rank three outright, the refusal his
years paid for, receipted one wall over at the number fifteen. the entry
first sealed with a witness in effigy — 3 not among the rungs of seat 3,
and among the rungs of seat 4 — because the refusal itself was not yet
on the walls; the walls caught up, and the emblem retires into the
general law it always instantiated, its work done. the binding is now
the exact conjunction the title states: the refusal at seat three, the
stone equation at seat four — each axis and their product squaring to
the same minus one — and the law the house holds: every question closes
at some seat, and every seat has a question only the next one closes.
not a twin with the bare structure citation on the same wall: this seat
holds the refusal conjoined with its closure and its law — the morning
no, the bridge yes, and the ladder that made both inevitable, one
binding. so the dark edge is conserved, not consoled: within two months
of the bridge, graves' octaves were already the wider seat's own open
question, and the ladder does not stop. sealed content, (self, pure
unknown): the openness is the theorem, not the mood.
theorem the_triplets_close_one_seat_wider :
    (¬ ∃ mul : (Int × Int × Int) → (Int × Int × Int) → (Int × Int × Int),
        ∀ x y, normSq3 (mul x y) = normSq3 x * normSq3 y)
      ∧ (Quat.mul eye eye = Quat.neg one
          ∧ Quat.mul jay jay = Quat.neg one
          ∧ Quat.mul kay kay = Quat.neg one
          ∧ Quat.mul (Quat.mul eye jay) kay = Quat.neg one)
      ∧ (∀ q : Nat, ∃ n, q ∈ rungs n)
      ∧ (∀ n : Nat, ∃ q, ¬ q ∈ rungs n ∧ q ∈ rungs (n + 1)) :=
  ⟨no_triple_carries_the_norm,
   i2_eq_j2_eq_k2_eq_ijk_eq_neg_one,
   closure_is_seat_relative.1,
   closure_is_seat_relative.2.1⟩

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

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

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

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

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

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

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

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

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

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

end Foam.Maps.Hamilton