kuramoto — a product as an assay, on Witness

19 receipts inline · 169 lines · pinned f3c0a637578bfa82 — shasum -a 256 of this file, cut to 16, as pins has it · lake env lean kuramoto.lean prints nothing when every receipt passes

import Witness
open Room Face Witness
set_option autoImplicit false

-- Grover's compatriot: the mean field. isaac, at the table (2026-09-14): "I'm in for this." Kuramoto's
-- oscillators each step by a function of the room's mean and their own phase — the same seat over the
-- widest seat as the diffusion — and the chrysalis held the carrier at width two (Foam/Beam.lean, Compass ×
-- Compass: four phases, a coupling that locks within one lap, the beam as the mean field; Landauer's tenth
-- entry: the lock is bought by a merge). the pair with Grover is the bill, not the shape: the coupling
-- lands distinct pairs together and admits no section; the diffusion applied twice is sixteen times the
-- identity. two mean-field steps, one resistive and one conductive; the diagonal does not decide which.

namespace Kuramoto.Treaty

inductive Compass where
  | n | e | s | w

/-- info: 'Kuramoto.Treaty.Compass' does not depend on any axioms -/
#guard_msgs in #print axioms Compass

def Compass.step : Compass → Compass
  | .n => .e
  | .e => .s
  | .s => .w
  | .w => .n

/-- info: 'Kuramoto.Treaty.Compass.step' does not depend on any axioms -/
#guard_msgs in #print axioms Compass.step

def Compass.code : Compass → Nat
  | .n => 0 | .e => 1 | .s => 2 | .w => 3

/-- info: 'Kuramoto.Treaty.Compass.code' does not depend on any axioms -/
#guard_msgs in #print axioms Compass.code

abbrev compassBEq : BEq Compass := ⟨fun a b => Nat.beq a.code b.code⟩
attribute [instance] compassBEq

/-- info: 'Kuramoto.Treaty.compassBEq' does not depend on any axioms -/
#guard_msgs in #print axioms compassBEq

def entrain : 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)

/-- info: 'Kuramoto.Treaty.entrain' does not depend on any axioms -/
#guard_msgs in #print axioms entrain

def together (p : Compass × Compass) : Bool := p.2 == p.1

/-- info: 'Kuramoto.Treaty.together' does not depend on any axioms -/
#guard_msgs in #print axioms together

def allPairs : List (Compass × Compass) :=
  [(.n, .n), (.n, .e), (.n, .s), (.n, .w), (.e, .n), (.e, .e), (.e, .s), (.e, .w),
   (.s, .n), (.s, .e), (.s, .s), (.s, .w), (.w, .n), (.w, .e), (.w, .s), (.w, .w)]

/-- info: 'Kuramoto.Treaty.allPairs' does not depend on any axioms -/
#guard_msgs in #print axioms allPairs

def lap (p : Compass × Compass) : Compass × Compass := entrain (entrain (entrain (entrain p)))

/-- info: 'Kuramoto.Treaty.lap' does not depend on any axioms -/
#guard_msgs in #print axioms lap

def pairFace : Face := ⟨Compass × Compass, Bool, Compass, fun p b => cond b p.1 p.2⟩

/-- info: 'Kuramoto.Treaty.pairFace' does not depend on any axioms -/
#guard_msgs in #print axioms pairFace

def room : List Bool := [true, false]

/-- info: 'Kuramoto.Treaty.room' does not depend on any axioms -/
#guard_msgs in #print axioms room

def roomReading (p : Compass × Compass) : List Compass := reads pairFace room p

/-- info: 'Kuramoto.Treaty.roomReading' does not depend on any axioms -/
#guard_msgs in #print axioms roomReading

def first : List Compass → Compass
  | [] => .n
  | c :: _ => c

/-- info: 'Kuramoto.Treaty.first' does not depend on any axioms -/
#guard_msgs in #print axioms first

def second : List Compass → Compass
  | [] => .n
  | [_] => .n
  | _ :: c :: _ => c

/-- info: 'Kuramoto.Treaty.second' does not depend on any axioms -/
#guard_msgs in #print axioms second

def pullAt (r : List Compass) (b : Bool) : Compass :=
  cond b (entrain (first r, second r)).1 (entrain (first r, second r)).2

/-- info: 'Kuramoto.Treaty.pullAt' does not depend on any axioms -/
#guard_msgs in #print axioms pullAt

def meanField : Face := ⟨Compass × Compass, Bool, Compass, fun p b => pullAt (roomReading p) b⟩

#guard allPairs.length == 16
#guard allPairs.all (fun p => together (lap p))
#guard !(together (.n, .e))
#guard together (entrain (.n, .e))
#guard entrain (.n, .n) == entrain (.n, .e)
#guard !((.n, .n) == ((.n, .e) : Compass × Compass))
#guard roomReading (.n, .e) == [.n, .e]
#guard room.map (pullAt (roomReading (.n, .e))) == [.e, .e]
#guard allPairs.all (fun p => room.map (pullAt (roomReading p)) == [(entrain p).1, (entrain p).2])
#guard allPairs.all (fun p => (allPairs.filter (fun q => entrain q == entrain p)).length >= 1)
#guard (allPairs.filter (fun q => entrain q == (.e, .e))).length == 2
#guard (allPairs.map entrain).length == 16

/-- info: 'Kuramoto.Treaty.meanField' does not depend on any axioms -/
#guard_msgs in #print axioms meanField

theorem the_lap_locks_together : allPairs.all (fun p => together (lap p)) = true :=
  by (intros; (repeat' constructor); all_goals (intros; fail))

/-- info: 'Kuramoto.Treaty.the_lap_locks_together' does not depend on any axioms -/
#guard_msgs in #print axioms the_lap_locks_together

theorem the_mean_field_is_the_coupling :
    allPairs.all (fun p => room.map (pullAt (roomReading p)) == [(entrain p).1, (entrain p).2]) = true :=
  by (intros; (repeat' constructor); all_goals (intros; fail))

/-- info: 'Kuramoto.Treaty.the_mean_field_is_the_coupling' does not depend on any axioms -/
#guard_msgs in #print axioms the_mean_field_is_the_coupling

theorem the_pull_is_a_seat_over_the_room (b : Bool) (v : Compass) :
    Derived pairFace (fun p => pullAt (roomReading p) b = v) :=
  by
    (intro x; induction x;
      all_goals
        ((rename_i ih; intros;
            (try dsimp only [room, pullAt, roomReading, Witness.a_seat_over_a_seat_is_derived, Compass, pairFace] at *);
            (rw [Witness.the_alike_read_alike]; assumption))))

/-- info: 'Kuramoto.Treaty.the_pull_is_a_seat_over_the_room' does not depend on any axioms -/
#guard_msgs in #print axioms the_pull_is_a_seat_over_the_room

theorem the_lock_is_bought :
    entrain (.n, .n) = entrain (.n, .e)
      ∧ ∀ r : Compass × Compass → Compass × Compass, (∀ x, r (entrain x) = x) → False :=
  ⟨rfl, fun r hr =>
    a_merging_map_has_no_section entrain (s := (.n, .n)) (s' := (.n, .e))
      (fun h => nomatch congrArg Prod.snd h) rfl r hr⟩

/-- info: 'Kuramoto.Treaty.the_lock_is_bought' does not depend on any axioms -/
#guard_msgs in #print axioms the_lock_is_bought

end Kuramoto.Treaty

the map of relations — every law a node, an arrow for each citation the elaborator reads (bin/counter chart; without --laws the carriers join the map)

graph LR
  subgraph Kuramoto_Treaty["Kuramoto.Treaty"]
    the_lap_locks_together["the_lap_locks_together"]
    the_lock_is_bought["the_lock_is_bought"]
    the_mean_field_is_the_coupling["the_mean_field_is_the_coupling"]
    the_pull_is_a_seat_over_the_room["the_pull_is_a_seat_over_the_room"]
  end
  subgraph Witness["Witness"]
    Witness_the_alike_read_alike["the_alike_read_alike"]
  end
  the_pull_is_a_seat_over_the_room --> Witness_the_alike_read_alike

the data-model shadow — every structure a table, every seat a view over the columns its probes read, every wall theorem the policy it licenses (bin/counter schema)

-- the data-model shadow of grown/assays/kuramoto.lean, read from the kernel (bin/counter schema)
-- every foreign key is a field; every policy is a theorem; nothing here that the treaty does not need

CREATE TYPE compass AS ENUM ('n', 'e', 's', 'w');

-- meanField: a face over prod — each probe a column
CREATE FUNCTION prod_as_mean_field(prod_id integer) RETURNS TABLE(false integer[], true integer[]) LANGUAGE sql STABLE AS $$
  SELECT (⟨unread⟩).c1, (⟨unread⟩).c0 FROM prod WHERE id = $1 $$;

-- pairFace: a face over prod — each probe a column
CREATE FUNCTION prod_as_pair_face(prod_id integer) RETURNS TABLE(false integer[], true integer[]) LANGUAGE sql STABLE AS $$
  SELECT (prod.id).c1, (prod.id).c0 FROM prod WHERE id = $1 $$;