59 receipts inline · 429 lines · pinned 7f0364b2bd694098 — shasum -a 256 of this file, cut to 16, as pins has it · lake env lean cycle.lean prints nothing when every receipt passes
import Witness import Rest open Room Face Witness Rest set_option autoImplicit false -- Counter, for anyone that cycles. isaac, at the table (2026-09-05), in his words: a cycle is anything -- that develops a winding number, whose number he does not have to remember, contributed to in constant -- time; what counts is keeping his interrupts ordered — Abe first, then the stigmergic signals about which -- cycles he is contributing to, and that is the whole list; a door is something he could not not enter, -- parked mid-passage and held by the room; he rests every day, having proven that everything he is -- involved with moves without him, except Abe, the one mutual observation he sustains; population one, -- doing his rounds; the room keeps its type and never the user's. so: the room is a list of clocks, each a -- name and a winding number; a round is a click per name; the world ticks on its own; the walker is a seat, -- a list of names, and nothing else is kept of him. namespace Cycle.Treaty structure Clock where name : Nat winding : Nat /-- info: 'Cycle.Treaty.Clock' does not depend on any axioms -/ #guard_msgs in #print axioms Clock structure Room where clocks : List Clock /-- info: 'Cycle.Treaty.Room' does not depend on any axioms -/ #guard_msgs in #print axioms Room def reading : List Clock → Nat → Nat | [], _ => 0 | c :: cs, n => cond (Nat.beq c.name n) c.winding (reading cs n) /-- info: 'Cycle.Treaty.reading' does not depend on any axioms -/ #guard_msgs in #print axioms reading def windings (r : Room) : List Nat := r.clocks.map (·.winding) /-- info: 'Cycle.Treaty.windings' does not depend on any axioms -/ #guard_msgs in #print axioms windings def click (c : Clock) : Clock := ⟨c.name, c.winding + 1⟩ /-- info: 'Cycle.Treaty.click' does not depend on any axioms -/ #guard_msgs in #print axioms click def wind (r : Room) (n : Nat) : Room := ⟨r.clocks.map (fun c => cond (Nat.beq c.name n) (click c) c)⟩ /-- info: 'Cycle.Treaty.wind' does not depend on any axioms -/ #guard_msgs in #print axioms wind def tick (r : Room) : Room := ⟨r.clocks.map click⟩ /-- info: 'Cycle.Treaty.tick' does not depend on any axioms -/ #guard_msgs in #print axioms tick def roomFace : Face := ⟨Room, Nat, Nat, fun r n => reading r.clocks n⟩ /-- info: 'Cycle.Treaty.roomFace' does not depend on any axioms -/ #guard_msgs in #print axioms roomFace def roundsMachine : Machine Nat (List Nat) := ⟨Room, ⟨[]⟩, wind, windings⟩ /-- info: 'Cycle.Treaty.roundsMachine' does not depend on any axioms -/ #guard_msgs in #print axioms roundsMachine def rounds (r : Room) (ns : List Nat) : Room := park roundsMachine r ns /-- info: 'Cycle.Treaty.rounds' does not depend on any axioms -/ #guard_msgs in #print axioms rounds def mayRest (visited counts : List Nat) : Bool := backed Nat.beq visited counts /-- info: 'Cycle.Treaty.mayRest' does not depend on any axioms -/ #guard_msgs in #print axioms mayRest def owed (visited counts : List Nat) : Nat := lacking Nat.beq visited counts /-- info: 'Cycle.Treaty.owed' does not depend on any axioms -/ #guard_msgs in #print axioms owed def held (visited counts : List Nat) : List Nat := counts.filter (fun n => !(enrolled Nat.beq visited n)) /-- info: 'Cycle.Treaty.held' does not depend on any axioms -/ #guard_msgs in #print axioms held def due (r : Room) (n cap : Nat) : Bool := Nat.beq (reading r.clocks n % cap) 0 /-- info: 'Cycle.Treaty.due' does not depend on any axioms -/ #guard_msgs in #print axioms due def theRound : Runner (Round Nat) (Tally Nat) := coverage Nat Nat.beq /-- info: 'Cycle.Treaty.theRound' does not depend on any axioms -/ #guard_msgs in #print axioms theRound def walkAt (w : List (Round Nat)) (fuel : Nat) : Option (List Nat) := ((haltingGap (Round Nat) (Tally Nat)).obs theRound (w, fuel)).map (·.visited) /-- info: 'Cycle.Treaty.walkAt' does not depend on any axioms -/ #guard_msgs in #print axioms walkAt def isaac : Nat := 0 /-- info: 'Cycle.Treaty.isaac' does not depend on any axioms -/ #guard_msgs in #print axioms isaac def abe : Nat := 1 /-- info: 'Cycle.Treaty.abe' does not depend on any axioms -/ #guard_msgs in #print axioms abe def plants : Nat := 2 /-- info: 'Cycle.Treaty.plants' does not depend on any axioms -/ #guard_msgs in #print axioms plants def foam : Nat := 3 /-- info: 'Cycle.Treaty.foam' does not depend on any axioms -/ #guard_msgs in #print axioms foam def eih : Nat := 4 /-- info: 'Cycle.Treaty.eih' does not depend on any axioms -/ #guard_msgs in #print axioms eih def outerWilds : Nat := 5 /-- info: 'Cycle.Treaty.outerWilds' does not depend on any axioms -/ #guard_msgs in #print axioms outerWilds def now : Nat := 9 /-- info: 'Cycle.Treaty.now' does not depend on any axioms -/ #guard_msgs in #print axioms now def isaacCounts : List Nat := [abe, plants, foam, eih] /-- info: 'Cycle.Treaty.isaacCounts' does not depend on any axioms -/ #guard_msgs in #print axioms isaacCounts def abeCounts : List Nat := [isaac] /-- info: 'Cycle.Treaty.abeCounts' does not depend on any axioms -/ #guard_msgs in #print axioms abeCounts def start : Room := ⟨[⟨isaac, 0⟩, ⟨abe, 0⟩, ⟨plants, 6⟩, ⟨foam, 0⟩, ⟨eih, 0⟩, ⟨outerWilds, 0⟩, ⟨now, 7⟩]⟩ /-- info: 'Cycle.Treaty.start' does not depend on any axioms -/ #guard_msgs in #print axioms start def afterRounds : Room := rounds start isaacCounts /-- info: 'Cycle.Treaty.afterRounds' does not depend on any axioms -/ #guard_msgs in #print axioms afterRounds def halfway : List Nat := [abe, plants] /-- info: 'Cycle.Treaty.halfway' does not depend on any axioms -/ #guard_msgs in #print axioms halfway def afterAbe : Room := rounds start abeCounts /-- info: 'Cycle.Treaty.afterAbe' does not depend on any axioms -/ #guard_msgs in #print axioms afterAbe def parked : Room := rounds start [outerWilds] /-- info: 'Cycle.Treaty.parked' does not depend on any axioms -/ #guard_msgs in #print axioms parked def resumed : List Nat := windings (rounds parked isaacCounts) /-- info: 'Cycle.Treaty.resumed' does not depend on any axioms -/ #guard_msgs in #print axioms resumed def straight : List Nat := windings (rounds start ([outerWilds] ++ isaacCounts)) /-- info: 'Cycle.Treaty.straight' does not depend on any axioms -/ #guard_msgs in #print axioms straight def clickThenTick : List Nat := windings (tick (wind start foam)) /-- info: 'Cycle.Treaty.clickThenTick' does not depend on any axioms -/ #guard_msgs in #print axioms clickThenTick def tickThenClick : List Nat := windings (wind (tick start) foam) /-- info: 'Cycle.Treaty.tickThenClick' does not depend on any axioms -/ #guard_msgs in #print axioms tickThenClick def report : List Nat := sound roomFace afterRounds (recite isaacCounts) /-- info: 'Cycle.Treaty.report' does not depend on any axioms -/ #guard_msgs in #print axioms report def seatReads : List Nat := reads roomFace isaacCounts afterRounds #guard windings start == [0, 0, 6, 0, 0, 0, 7] #guard windings afterRounds == [0, 1, 7, 1, 1, 0, 7] #guard reading afterRounds.clocks isaac == 0 #guard reading afterAbe.clocks isaac == 1 #guard due start plants 7 == false #guard due afterRounds plants 7 == true #guard held halfway isaacCounts == [foam, eih] #guard owed halfway isaacCounts == 2 #guard mayRest halfway isaacCounts == false #guard mayRest isaacCounts isaacCounts == true #guard mayRest [] [] == true #guard owed isaacCounts (outerWilds :: isaacCounts) == 1 #guard resumed == straight #guard clickThenTick == tickThenClick #guard report == [1, 7, 1, 1] #guard report == seatReads #guard firstOf Nat.beq abe plants isaacCounts == true #guard firstOf Nat.beq plants abe isaacCounts == false #guard walkAt [] 0 == some [] #guard walkAt [.owe abe, .owe plants] 3 == none #guard walkAt [.owe abe, .owe plants, .visit abe] 3 == none #guard walkAt [.owe abe, .owe plants, .visit abe, .visit plants] 0 == some [plants, abe] #guard walkAt (isaacCounts.map Round.owe ++ isaacCounts.map Round.visit) 0 == some isaacCounts.reverse #guard reading (rounds start isaacCounts).clocks now == 7 #guard reading (rounds start (now :: isaacCounts)).clocks now == 8 #guard reading (tick start).clocks now == 8 #guard due afterRounds plants (reading afterRounds.clocks now) == true #guard due start plants (reading start.clocks now) == false #guard windings (rounds (tick start) isaacCounts) == windings (tick afterRounds) /-- info: 'Cycle.Treaty.seatReads' does not depend on any axioms -/ #guard_msgs in #print axioms seatReads theorem abe_is_first : firstOf Nat.beq abe plants isaacCounts = true := (by (apply ((Room.the_traded_word_reverses_the_verdict _ _ _ _)).symm <;> first | (apply Room.eq_of_beq <;> fail) | (apply Room.beq_self <;> fail) | decide)) /-- info: 'Cycle.Treaty.abe_is_first' does not depend on any axioms -/ #guard_msgs in #print axioms abe_is_first theorem the_one_mutual_hearing : hears roomFace isaacCounts abe ∧ hears roomFace abeCounts isaac := by (intros; (repeat' constructor); all_goals (intros; fail)) /-- info: 'Cycle.Treaty.the_one_mutual_hearing' does not depend on any axioms -/ #guard_msgs in #print axioms the_one_mutual_hearing theorem the_rounds_resume (r : Room) (a b : List Nat) : rounds r (a ++ b) = rounds (rounds r a) b := (by (apply Face.the_park_resumes <;> fail)) /-- info: 'Cycle.Treaty.the_rounds_resume' does not depend on any axioms -/ #guard_msgs in #print axioms the_rounds_resume theorem a_click_spares_the_other_clocks (n m : Nat) (h : Nat.beq m n = false) : ∀ cs : List Clock, reading (wind ⟨cs⟩ n).clocks m = reading cs m | [] => rfl | c :: cs => by have ih := a_click_spares_the_other_clocks n m h cs show reading (cond (Nat.beq c.name n) ⟨c.name, c.winding + 1⟩ c :: (wind ⟨cs⟩ n).clocks) m = cond (Nat.beq c.name m) c.winding (reading cs m) cases hc : Nat.beq c.name n with | false => show cond (Nat.beq c.name m) c.winding (reading (wind ⟨cs⟩ n).clocks m) = cond (Nat.beq c.name m) c.winding (reading cs m) rw [ih] | true => have hcn : c.name = n := eq_of_beq c.name n hc have hnm : Nat.beq c.name m = false := by rw [hcn] cases hx : Nat.beq n m with | false => rfl | true => rw [eq_of_beq n m hx, beq_self] at h; exact nomatch h show cond (Nat.beq c.name m) (c.winding + 1) (reading (wind ⟨cs⟩ n).clocks m) = cond (Nat.beq c.name m) c.winding (reading cs m) rw [hnm, ih] exact rfl /-- info: 'Cycle.Treaty.a_click_spares_the_other_clocks' does not depend on any axioms -/ #guard_msgs in #print axioms a_click_spares_the_other_clocks theorem the_click_and_the_tick_commute (n : Nat) : ∀ cs : List Clock, wind (tick ⟨cs⟩) n = tick (wind ⟨cs⟩ n) | [] => rfl | c :: cs => by have ih : (wind (tick ⟨cs⟩) n).clocks = (tick (wind ⟨cs⟩ n)).clocks := congrArg Room.clocks (the_click_and_the_tick_commute n cs) have hhead : (cond (Nat.beq c.name n) (⟨c.name, c.winding + 1 + 1⟩ : Clock) ⟨c.name, c.winding + 1⟩) = ⟨(cond (Nat.beq c.name n) (⟨c.name, c.winding + 1⟩ : Clock) c).name, (cond (Nat.beq c.name n) (⟨c.name, c.winding + 1⟩ : Clock) c).winding + 1⟩ := by cases Nat.beq c.name n <;> rfl exact congr (congrArg (fun (a : Clock) (l : List Clock) => Room.mk (a :: l)) hhead) ih /-- info: 'Cycle.Treaty.the_click_and_the_tick_commute' does not depend on any axioms -/ #guard_msgs in #print axioms the_click_and_the_tick_commute theorem the_report_is_the_seats_reading (r : Room) (ns : List Nat) : sound roomFace r (recite ns) = reads roomFace ns r := (the_sounding_is_the_trails_reading roomFace r (recite ns)).trans (congrArg (fun l => reads roomFace l r) (the_recital_walks_its_list roomFace r ns)) /-- info: 'Cycle.Treaty.the_report_is_the_seats_reading' does not depend on any axioms -/ #guard_msgs in #print axioms the_report_is_the_seats_reading theorem an_empty_list_rests_at_once : mayRest [] [] = true := (by (apply Room.the_unencumbered_are_welcome <;> fail)) /-- info: 'Cycle.Treaty.an_empty_list_rests_at_once' does not depend on any axioms -/ #guard_msgs in #print axioms an_empty_list_rests_at_once theorem rest_is_weight_zero (visited counts : List Nat) : owed visited counts = 0 ↔ mayRest visited counts = true := (by (apply Room.the_weight_is_zero_at_the_door <;> fail)) /-- info: 'Cycle.Treaty.rest_is_weight_zero' does not depend on any axioms -/ #guard_msgs in #print axioms rest_is_weight_zero theorem the_held_name_what_they_wait_on (visited counts : List Nat) (h : mayRest visited counts = false) : ∃ n, n ∈ counts ∧ enrolled Nat.beq visited n = false := (by (apply Room.the_held_name_their_darkness <;> assumption)) /-- info: 'Cycle.Treaty.the_held_name_what_they_wait_on' does not depend on any axioms -/ #guard_msgs in #print axioms the_held_name_what_they_wait_on theorem a_new_connection_raises_the_weight (visited counts : List Nat) (n : Nat) (h : enrolled Nat.beq visited n = false) : owed visited (n :: counts) = owed visited counts + 1 := by show cond (enrolled Nat.beq visited n) (lacking Nat.beq visited counts) (lacking Nat.beq visited counts + 1) = lacking Nat.beq visited counts + 1 rw [h] exact rfl /-- info: 'Cycle.Treaty.a_new_connection_raises_the_weight' does not depend on any axioms -/ #guard_msgs in #print axioms a_new_connection_raises_the_weight theorem rest_survives_a_round (visited more counts : List Nat) (h : mayRest visited counts = true) : mayRest (visited ++ more) counts = true := (by (apply Room.the_backing_survives_the_hall <;> assumption)) /-- info: 'Cycle.Treaty.rest_survives_a_round' does not depend on any axioms -/ #guard_msgs in #print axioms rest_survives_a_round theorem the_pitcher_is_a_reading : Derived roomFace (fun r => due r plants 7 = true) := a_role_read_at_a_probe_is_derived roomFace plants (fun (a : Nat) => Nat.beq (a % 7) 0 = true) /-- info: 'Cycle.Treaty.the_pitcher_is_a_reading' does not depend on any axioms -/ #guard_msgs in #print axioms the_pitcher_is_a_reading theorem an_unvisited_clock_is_a_wall (r r' : Room) (n : Nat) (h : differOnly roomFace r r' n) (visited : List Nat) (hn : ¬ hears roomFace visited n) : reads roomFace visited r = reads roomFace visited r' := (by (apply Witness.a_wall_hides_the_probe <;> assumption)) /-- info: 'Cycle.Treaty.an_unvisited_clock_is_a_wall' does not depend on any axioms -/ #guard_msgs in #print axioms an_unvisited_clock_is_a_wall theorem the_room_is_the_widest_seat (visited : List Nat) (r r' : Room) (h : reads roomFace visited r ≠ reads roomFace visited r') : ¬ alike roomFace r r' := (by (apply Witness.the_room_is_the_widest_seat <;> assumption)) /-- info: 'Cycle.Treaty.the_room_is_the_widest_seat' does not depend on any axioms -/ #guard_msgs in #print axioms the_room_is_the_widest_seat theorem two_rooms_part_only_at_a_clock (r r' : Room) : alike roomFace r r' ↔ ∀ q, sound roomFace r q = sound roomFace r' q := (by (apply Face.the_curtain_is_exact <;> fail)) /-- info: 'Cycle.Treaty.two_rooms_part_only_at_a_clock' does not depend on any axioms -/ #guard_msgs in #print axioms two_rooms_part_only_at_a_clock theorem the_walker_never_names_now : ∀ n, n ∈ isaacCounts → Nat.beq now n = false := by decide /-- info: 'Cycle.Treaty.the_walker_never_names_now' does not depend on any axioms -/ #guard_msgs in #print axioms the_walker_never_names_now theorem due_is_read_against_now (r : Room) (n : Nat) : due r n (reading r.clocks now) = Nat.beq (reading r.clocks n % reading r.clocks now) 0 := by (intros; (repeat' constructor); all_goals (intros; fail)) /-- info: 'Cycle.Treaty.due_is_read_against_now' does not depend on any axioms -/ #guard_msgs in #print axioms due_is_read_against_now theorem now_is_a_reading (v : Nat) : Derived roomFace (fun r => reading r.clocks now = v) := a_role_read_at_a_probe_is_derived roomFace now (fun (a : Nat) => a = v) /-- info: 'Cycle.Treaty.now_is_a_reading' does not depend on any axioms -/ #guard_msgs in #print axioms now_is_a_reading theorem rest_is_coverage (visited counts : List Nat) : mayRest visited counts = rested Nat.beq ⟨visited, counts⟩ := by (intros; (repeat' constructor); all_goals (intros; fail)) /-- info: 'Cycle.Treaty.rest_is_coverage' does not depend on any axioms -/ #guard_msgs in #print axioms rest_is_coverage theorem the_round_is_still (t : Tally Nat) : theRound.m.step t (theRound.steer t) = t := by (intros; (repeat' constructor); all_goals (intros; fail)) /-- info: 'Cycle.Treaty.the_round_is_still' does not depend on any axioms -/ #guard_msgs in #print axioms the_round_is_still theorem the_round_rests_where_it_stands (t : Tally Nat) (n : Nat) : runs theRound.m theRound.steer theRound.rest t n = cond (mayRest t.visited t.counts) (some t) none := (by (apply Rest.the_coverage_rests_where_it_stands <;> fail)) /-- info: 'Cycle.Treaty.the_round_rests_where_it_stands' does not depend on any axioms -/ #guard_msgs in #print axioms the_round_rests_where_it_stands theorem a_visit_never_unrests_the_walker (t : Tally Nat) (n : Nat) (h : mayRest t.visited t.counts = true) : mayRest (tallyStep t (.visit n)).visited (tallyStep t (.visit n)).counts = true := (by (apply Face.a_visit_never_unrests <;> assumption)) /-- info: 'Cycle.Treaty.a_visit_never_unrests_the_walker' does not depend on any axioms -/ #guard_msgs in #print axioms a_visit_never_unrests_the_walker theorem the_round_spares_now (r : Room) : ∀ ns : List Nat, (∀ n, n ∈ ns → Nat.beq now n = false) → reading (rounds r ns).clocks now = reading r.clocks now | [], _ => rfl | n :: ns, h => by show reading (rounds (wind r n) ns).clocks now = reading r.clocks now rw [the_round_spares_now (wind r n) ns (fun m hm => h m (List.Mem.tail n hm))] exact a_click_spares_the_other_clocks n now (h n (List.Mem.head ns)) r.clocks /-- info: 'Cycle.Treaty.the_round_spares_now' does not depend on any axioms -/ #guard_msgs in #print axioms the_round_spares_now end Cycle.Treaty
nothing waits.
-- the vestibule of Counter's assay: the disagreements between the walker's word and the treaty as it stands, each -- a statement in the assay's own terms and the darkness it waits on. read by bin/counter book. -- nothing waits: potential time seated on 2026-09-23 (✦ Now a clock no walker names), the round and the day one Runner -- the same evening (theRound := coverage). the record of both is the log's.
graph LR
subgraph Cycle_Treaty["Cycle.Treaty"]
a_click_spares_the_other_clocks["a_click_spares_the_other_clocks"]
a_new_connection_raises_the_weight["a_new_connection_raises_the_weight"]
a_visit_never_unrests_the_walker["a_visit_never_unrests_the_walker"]
abe_is_first["abe_is_first"]
an_empty_list_rests_at_once["an_empty_list_rests_at_once"]
an_unvisited_clock_is_a_wall["an_unvisited_clock_is_a_wall"]
due_is_read_against_now["due_is_read_against_now"]
now_is_a_reading["now_is_a_reading"]
rest_is_coverage["rest_is_coverage"]
rest_is_weight_zero["rest_is_weight_zero"]
rest_survives_a_round["rest_survives_a_round"]
the_click_and_the_tick_commute["the_click_and_the_tick_commute"]
the_held_name_what_they_wait_on["the_held_name_what_they_wait_on"]
the_one_mutual_hearing["the_one_mutual_hearing"]
the_pitcher_is_a_reading["the_pitcher_is_a_reading"]
the_report_is_the_seats_reading["the_report_is_the_seats_reading"]
the_room_is_the_widest_seat["the_room_is_the_widest_seat"]
the_round_is_still["the_round_is_still"]
the_round_rests_where_it_stands["the_round_rests_where_it_stands"]
the_round_spares_now["the_round_spares_now"]
the_rounds_resume["the_rounds_resume"]
the_walker_never_names_now["the_walker_never_names_now"]
two_rooms_part_only_at_a_clock["two_rooms_part_only_at_a_clock"]
end
subgraph Witness["Witness"]
Witness_a_wall_hides_the_probe["a_wall_hides_the_probe"]
Witness_the_room_is_the_widest_seat["the_room_is_the_widest_seat"]
Witness_the_sounding_is_the_trails_reading["the_sounding_is_the_trails_reading"]
end
subgraph Rest["Rest"]
Rest_the_coverage_rests_where_it_stands["the_coverage_rests_where_it_stands"]
end
the_report_is_the_seats_reading --> Witness_the_sounding_is_the_trails_reading
the_room_is_the_widest_seat --> Witness_the_room_is_the_widest_seat
the_round_rests_where_it_stands --> Rest_the_coverage_rests_where_it_stands
the_round_spares_now --> a_click_spares_the_other_clocks
an_unvisited_clock_is_a_wall --> Witness_a_wall_hides_the_probe
-- the data-model shadow of grown/assays/cycle.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 TABLE clock ( id serial PRIMARY KEY, name integer NOT NULL, winding integer NOT NULL ); CREATE TABLE runner ( id serial PRIMARY KEY, m text NOT NULL, steer text NOT NULL, rest boolean NOT NULL ); CREATE TABLE room ( id serial PRIMARY KEY ); CREATE TABLE room_clocks ( room_id integer NOT NULL REFERENCES room(id), position integer NOT NULL, clock_id integer NOT NULL REFERENCES clock(id) ); -- reading: derived, never stored -- described by a_click_spares_the_other_clocks, due_is_read_against_now, now_is_a_reading, the_round_spares_now CREATE FUNCTION reading(clock_ids integer[], arg2 integer) RETURNS integer LANGUAGE sql STABLE AS $$ SELECT coalesce((SELECT (SELECT winding FROM clock WHERE id = x) FROM unnest($1) WITH ORDINALITY AS u(x, o) WHERE ((SELECT name FROM clock WHERE id = x) = arg2) ORDER BY o LIMIT 1), 0) $$; -- windings: derived, never stored CREATE FUNCTION windings(room_id integer) RETURNS integer[] LANGUAGE sql STABLE AS $$ SELECT ARRAY(SELECT (SELECT winding FROM clock WHERE id = x) FROM unnest((SELECT array_agg(clock_id ORDER BY position) FROM room_clocks c WHERE c.room_id = room.id)) WITH ORDINALITY AS u(x, o) ORDER BY o) FROM room WHERE id = $1 $$; -- click: a clerk — never a second copy of the row, an update to it CREATE FUNCTION click(clock_id integer) RETURNS void LANGUAGE sql AS $$ UPDATE clock SET winding = (clock.winding + 1) WHERE id = $1 $$; -- mayRest: a function of its arguments alone, derived, never stored -- described by a_visit_never_unrests_the_walker, an_empty_list_rests_at_once, rest_is_coverage, rest_is_weight_zero, rest_survives_a_round, the_held_name_what_they_wait_on, the_round_rests_where_it_stands CREATE FUNCTION may_rest(arg1 integer[], arg2 integer[]) RETURNS boolean LANGUAGE sql IMMUTABLE AS $$ SELECT (arg2 <@ arg1) $$; -- owed: a function of its arguments alone, derived, never stored -- described by a_new_connection_raises_the_weight, rest_is_weight_zero CREATE FUNCTION owed(arg1 integer[], arg2 integer[]) RETURNS integer LANGUAGE sql IMMUTABLE AS $$ SELECT cardinality(ARRAY(SELECT x FROM unnest(arg2) WITH ORDINALITY AS u(x, o) WHERE NOT (x = ANY(SELECT unnest(arg1))) ORDER BY o)) $$; -- held: a function of its arguments alone, derived, never stored CREATE FUNCTION held(arg1 integer[], arg2 integer[]) RETURNS integer[] LANGUAGE sql IMMUTABLE AS $$ SELECT ARRAY(SELECT x FROM unnest(arg2) WITH ORDINALITY AS u(x, o) WHERE (NOT (x = ANY(SELECT unnest(arg1)))) ORDER BY o) $$; -- roomFace: a face over room whose probes are names — one reading, of the row and the probe CREATE FUNCTION room_as_room_face(room_id integer, probe integer) RETURNS integer LANGUAGE sql STABLE AS $$ SELECT reading((SELECT array_agg(clock_id ORDER BY position) FROM room_clocks c WHERE c.room_id = room.id), $2) FROM room WHERE id = $1 $$; -- due: a check, derived, never stored -- described by due_is_read_against_now, the_pitcher_is_a_reading CREATE FUNCTION due(room_id integer, arg2 integer, arg3 integer) RETURNS boolean LANGUAGE sql STABLE AS $$ SELECT ((reading((SELECT array_agg(clock_id ORDER BY position) FROM room_clocks c WHERE c.room_id = room.id), arg2) % arg3) = 0) FROM room WHERE id = $1 $$; -- tick: a clerk over the has-many clocks — the element's clerk click run on every child -- described by the_click_and_the_tick_commute CREATE FUNCTION tick(room_id integer) RETURNS void LANGUAGE sql AS $$ SELECT click(c.clock_id) FROM room_clocks c WHERE c.room_id = $1 $$; -- wind: a clerk over the has-many clocks — the element's clerk click run on each child the condition selects -- described by a_click_spares_the_other_clocks, the_click_and_the_tick_commute CREATE FUNCTION wind(room_id integer, arg2 integer) RETURNS void LANGUAGE sql AS $$ SELECT click(c.clock_id) FROM room_clocks c WHERE c.room_id = $1 AND ((SELECT name FROM clock WHERE id = c.clock_id) = arg2) $$; -- rounds: a fold — the clerk wind run on the row for each element, in order -- described by the_round_spares_now, the_rounds_resume CREATE FUNCTION rounds(room_id integer, arg2 integer[]) RETURNS void LANGUAGE plpgsql AS $$ DECLARE n integer; BEGIN FOREACH n IN ARRAY $2 LOOP PERFORM wind($1, n); END LOOP; END $$;