counter — a product as an assay, on Counter

23 receipts inline · 171 lines · pinned 72b9c53775807e30 — shasum -a 256 of this file, cut to 16, as pins has it · lake env lean counter.lean prints nothing when every receipt passes

import Room
import Face
import Counter
open Room Face Counter
set_option autoImplicit false

namespace Counter.Treaty

def demo : List sighting := [(1, []), (2, [3]), (3, [])]

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

def afterOne : room := round empty demo

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

def afterSweep : room := round (afterOne.1, []) afterOne.2

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

def selfCiter : room := round empty [(7, [7])]

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

def circle : room := round empty [(8, [9]), (9, [8])]

#guard seated afterOne 1
#guard seated afterOne 3
#guard !(seated afterOne 2)
#guard afterOne.2.length == 1
#guard seated afterSweep 2
#guard afterSweep.2.length == 0
#guard weight afterOne [3, 2] == 1
#guard weight afterSweep [3, 2] == 0
#guard !(seated selfCiter 7)
#guard !(seated circle 8) && !(seated circle 9)

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

def offered : room := offer empty (4, [])
#guard seated offered 4
#guard !(seated (offer empty (5, [6])) 5)

-- the gate, in rows: the verdict reads the artifact only through its receipts. a body is a list
-- of moves; the kernel's reading of it (its receipt) is the moves numbered 100 and up, a
-- standard-library lemma that smuggles an axiom; the prune drops the moves numbered 0, a `fail`
-- that never closed anything. these rows fail the day the gate starts reading bodies.

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

def axiomsOf (b : List Nat) : List Nat := b.filter (fun x => Nat.ble 100 x)

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

def dropFails (b : List Nat) : List Nat := b.filter (fun x => !(Nat.beq x 0))

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

def trailA : List (Nat × List Nat) := [(1, [3, 0, 5]), (2, [0, 7]), (3, [])]

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

def trailB : List (Nat × List Nat) := rebody dropFails trailA

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

def trailC : List (Nat × List Nat) := [(1, [3, 100]), (2, [7])]

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

def gateA : Bool := gate axiomsOf trailA

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

def gateB : Bool := gate axiomsOf trailB

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

def gateC : Bool := gate axiomsOf trailC

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

def gateCpruned : Bool := gate axiomsOf (rebody dropFails trailC)

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

def shadowA : List (Nat × List Nat) := shadow axiomsOf trailA

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

def shadowB : List (Nat × List Nat) := shadow axiomsOf trailB

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

def shadowC : List (Nat × List Nat) := shadow axiomsOf trailC
#guard gateA
#guard gateB
#guard !gateC
#guard !gateCpruned
#guard shadowA == shadowB
#guard trailA != trailB
#guard shadowA == [(1, []), (2, []), (3, [])]
#guard shadowC == [(1, [100]), (2, [])]

-- the route is the remainder at the gate (2026-09-13, isaac's word: a proof route is Landauer-neutral —
-- the runner comes home, the record grew elsewhere). a body's citations are a second reading of it,
-- the chart's; two trails with the same receipts are alike at the gate and part at the chart, and the
-- prune is unheard at both. these rows fail the day the gate starts reading citations.

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

def citesOf (b : List Nat) : List Nat := b.filter (fun x => !(Nat.beq x 0) && !(Nat.ble 100 x))

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

def trailD : List (Nat × List Nat) := [(1, [3, 5]), (2, [9]), (3, [])]
#guard shadow citesOf trailA == shadow citesOf trailB
#guard shadow axiomsOf trailA == shadow axiomsOf trailD
#guard shadow citesOf trailA != shadow citesOf trailD
#guard gate axiomsOf trailD

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

theorem the_route_is_the_remainder_at_the_gate {S B A C : Type} (read : B → List A) (cite : B → List C)
    (t t' : List (S × B)) (h : shadow read t = shadow read t') (hc : shadow cite t ≠ shadow cite t') :
    alike (gateFace S B A read) t t' ∧ ¬ alike (gateFace S B C cite) t t' :=
  ⟨fun _ => h, fun ha => hc (ha ())⟩

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

theorem the_prune_is_unheard_at_the_chart :
    alike (gateFace Nat (List Nat) Nat citesOf) trailA trailB :=
  by (intro x; induction x; all_goals ((intros; rfl)))

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

theorem the_two_routes_part_at_the_chart :
    alike (gateFace Nat (List Nat) Nat axiomsOf) trailA trailD
      ∧ ¬ alike (gateFace Nat (List Nat) Nat citesOf) trailA trailD :=
  (by
    (apply the_route_is_the_remainder_at_the_gate <;>
        first
        | rfl
        | decide))

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

end Counter.Treaty

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/counter.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


-- citesOf: a function of its arguments alone, derived, never stored
-- described by the_prune_is_unheard_at_the_chart, the_two_routes_part_at_the_chart
CREATE FUNCTION cites_of(arg1 integer[]) RETURNS integer[] LANGUAGE sql IMMUTABLE AS $$
  SELECT ARRAY(SELECT x FROM unnest(arg1) WITH ORDINALITY AS u(x, o) WHERE ((NOT (x = 0)) AND (NOT (100 <= x))) ORDER BY o) $$;

-- axiomsOf: a function of its arguments alone, derived, never stored
-- described by the_two_routes_part_at_the_chart
CREATE FUNCTION axioms_of(arg1 integer[]) RETURNS integer[] LANGUAGE sql IMMUTABLE AS $$
  SELECT ARRAY(SELECT x FROM unnest(arg1) WITH ORDINALITY AS u(x, o) WHERE (100 <= x) ORDER BY o) $$;

-- dropFails: a function of its arguments alone, derived, never stored
CREATE FUNCTION drop_fails(arg1 integer[]) RETURNS integer[] LANGUAGE sql IMMUTABLE AS $$
  SELECT ARRAY(SELECT x FROM unnest(arg1) WITH ORDINALITY AS u(x, o) WHERE (NOT (x = 0)) ORDER BY o) $$;

counter — a product as an assay, on Counter

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)

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)