grover — a product as an assay, on Witness

28 receipts inline · 226 lines · pinned a0135af9cfbb0fbf — shasum -a 256 of this file, cut to 16, as pins has it · lake env lean grover.lean prints nothing when every receipt passes

import Witness
open Room Face Witness
set_option autoImplicit false

-- luck, as a way to access results in fewer moves. isaac, at the table (2026-09-14), rotating the
-- runner's affordment: "what about luck? as a way to access results in fewer moves?" the record's own
-- luck theorem is the Born cross term (ac7ad39: born (field + act) = born field + born act + 2·align·align;
-- luck cannot be farmed, only met; the four phase placements cancel). run forward, that is amplitude
-- amplification: Grover (1996) finds one marked item among four with ONE query and certainty, where a
-- scan needs three in the worst case. a checksum with a community never met. amplitudes are integers
-- (the uniform state [1,1,1,1], the diffusion scaled by the room's width) so every row computes.
-- the diagonal (isaac, the same sitting: "I am extremely in for this"): the diffusion restated as a face
-- whose reading at every probe is a function of the room's reading — a seat over the widest seat. below
-- it, a mark at one probe is hidden from every seat that does not hear the probe (a wall); at the
-- diagonal the same mark moves every probe (no wall), and a reading at the diagonal is Derived below.
-- the surplus at the door (isaac, 2026-09-14, deposed): W is dark per seat, not per term — the host reads
-- the field half of the door and the act half is unheard there; one seat wider, where both halves are
-- read at the same probe, the cross term is Derived. what a W built to carry the surplus makes
-- addressable is the surplus as a reading, at the seat that built it, and never at the seat below.

namespace Grover.Treaty

def uniform : List Int := [1, 1, 1, 1]

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

def mark (t : Nat) (a : List Int) : List Int :=
  (a.zip (List.range a.length)).map (fun p => cond (Nat.beq p.2 t) (-p.1) p.1)

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

def diffuse (a : List Int) : List Int := a.map (fun x => 2 * a.sum - 4 * x)

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

def grover (t : Nat) : List Int := diffuse (mark t uniform)

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

def amp : List Int → Nat → Int
  | [], _ => 0
  | x :: _, 0 => x
  | _ :: xs, n + 1 => amp xs n

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

def weight (a : List Int) (i : Nat) : Int := amp a i * amp a i

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

def total (a : List Int) : Int := (a.map (fun x => x * x)).sum

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

def scanQueries (t : Nat) : Nat := cond (Nat.ble 3 t) 3 (t + 1)

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

def field : List Int := diffuse uniform

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

def act (t : Nat) : List Int := diffuse ((mark t uniform).zip uniform |>.map (fun p => p.1 - p.2))

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

def ampFace : Face := ⟨List Int, Nat, Int, amp⟩

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

def room : List Nat := [0, 1, 2, 3]

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

def roomReading (s : List Int) : List Int := reads ampFace room s

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

def diffuseAt (s : List Int) (i : Nat) : Int :=
  2 * (roomReading s).sum - 4 * amp (roomReading s) i

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

def diffusionFace : Face := ⟨List Int, Nat, Int, diffuseAt⟩

#guard grover 2 == [0, 0, 8, 0]
#guard [0, 1, 2, 3].all (fun t => weight (grover t) t == total (grover t))
#guard [0, 1, 2, 3].all (fun t => scanQueries t <= 3)
#guard scanQueries 3 == 3
#guard [0, 1, 2, 3].all (fun t => (field.zip (act t)).map (fun p => p.1 + p.2) == grover t)
#guard weight (grover 2) 2 == weight field 2 + weight (act 2) 2 + 2 * amp field 2 * amp (act 2) 2
#guard weight (grover 2) 0 == weight field 0 + weight (act 2) 0 + 2 * amp field 0 * amp (act 2) 0
#guard 2 * amp field 2 * amp (act 2) 2 == 32
#guard 2 * amp field 0 * amp (act 2) 0 == -32
#guard 2 * amp field 2 * amp (act 2) 2 + 2 * amp field 2 * amp (act 2) 0 == 0
#guard diffuse uniform == [4, 4, 4, 4]
#guard weight (diffuse uniform) 2 * 4 == total (diffuse uniform)
#guard room.map (amp (mark 2 uniform)) == [1, 1, -1, 1]
#guard room.map (diffuseAt (mark 2 uniform)) == grover 2
#guard room.map (diffuseAt uniform) == diffuse uniform
#guard [0, 1, 3].map (amp (mark 2 uniform)) == [0, 1, 3].map (amp uniform)
#guard ([0, 1, 3].map (diffuseAt (mark 2 uniform)) == [0, 1, 3].map (diffuseAt uniform)) == false
#guard room.all (fun i => diffuseAt (mark 2 uniform) i != diffuseAt uniform i)
#guard diffuse (diffuse (mark 2 uniform)) == (mark 2 uniform).map (fun x => 16 * x)
#guard diffuse (diffuse [3, -1, 7, 2]) == [3, -1, 7, 2].map (fun x => 16 * x)

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

def doorFace : Face :=
  ⟨door (List Int) (List Int), Nat, Int × Int, fun d i => (amp (face d) i, amp (met d) i)⟩

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

def charged : door (List Int) (List Int) := atTheDoor field (act 2)

#guard room.map (amp (face charged)) == room.map (amp field)
#guard 2 * amp (face charged) 2 * amp (met charged) 2 == 32
#guard 2 * amp (face charged) 0 * amp (met charged) 0 == -32

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

theorem the_one_query_finds_every_target :
    [0, 1, 2, 3].all (fun t => weight (grover t) t == total (grover t)) = true :=
  by (intros; (repeat' constructor); all_goals (intros; fail))

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

theorem the_scan_needs_three : scanQueries 3 = 3 ∧ scanQueries 2 = 3 :=
  by (intros; (repeat' constructor); all_goals (intros; fail))

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

theorem the_boost_is_the_cross_term :
    weight (grover 2) 2 = weight field 2 + weight (act 2) 2 + 2 * amp field 2 * amp (act 2) 2 :=
  by (intros; (repeat' constructor); all_goals (intros; fail))

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

theorem against_the_grain_costs :
    weight (grover 2) 0 = weight field 0 + weight (act 2) 0 + 2 * amp field 0 * amp (act 2) 0 :=
  by (intros; (repeat' constructor); all_goals (intros; fail))

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

theorem no_grain_no_bonus : weight (diffuse uniform) 2 * 4 = total (diffuse uniform) :=
  by (intros; (repeat' constructor); all_goals (intros; fail))

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

theorem the_diffusion_is_a_seat_over_the_room (i : Nat) (v : Int) :
    Derived ampFace (fun s => diffuseAt s i = v) :=
  a_seat_over_a_seat_is_derived ampFace room (fun (r : List Int) => 2 * r.sum - 4 * amp r i) v

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

theorem a_wall_below_the_diagonal :
    differOnly ampFace uniform (mark 2 uniform) (2 : Nat)
      ∧ reads ampFace ([0, 1, 3] : List Nat) uniform = reads ampFace ([0, 1, 3] : List Nat) (mark 2 uniform) :=
  ⟨fun (q : Nat) hq => match q with
    | 0 => rfl
    | 1 => rfl
    | 2 => absurd rfl hq
    | 3 => rfl
    | _ + 4 => rfl,
   rfl⟩

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

theorem no_wall_at_the_diagonal :
    room.all (fun i => diffuseAt (mark 2 uniform) i != diffuseAt uniform i) = true
      ∧ ([0, 1, 3].map (diffuseAt (mark 2 uniform)) == [0, 1, 3].map (diffuseAt uniform)) = false :=
  by (intros; (repeat' constructor); all_goals (intros; fail))

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

theorem the_diffusion_unwinds_itself :
    diffuse (diffuse (mark 2 uniform)) = (mark 2 uniform).map (fun x => 16 * x) :=
  by (intros; (repeat' constructor); all_goals (intros; fail))

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

theorem the_surplus_is_unheard_at_the_host :
    unheard (host ampFace (List Int)) (fun d => atTheDoor (face d) (act 2)) :=
  the_record_writes_where_the_face_is_blind ampFace (fun _ => act 2)

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

theorem the_surplus_is_read_one_seat_wider (i : Nat) (v : Int) :
    Derived doorFace (fun d => 2 * amp (face d) i * amp (met d) i = v) :=
  fun d d' h => by
    have e1 : amp (face d) i = amp (face d') i := congrArg Prod.fst (h i)
    have e2 : amp (met d) i = amp (met d') i := congrArg Prod.snd (h i)
    show (2 * amp (face d) i * amp (met d) i = v) ↔ (2 * amp (face d') i * amp (met d') i = v)
    rw [e1, e2]

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

end Grover.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 Grover_Treaty["Grover.Treaty"]
    a_wall_below_the_diagonal["a_wall_below_the_diagonal"]
    against_the_grain_costs["against_the_grain_costs"]
    no_grain_no_bonus["no_grain_no_bonus"]
    no_wall_at_the_diagonal["no_wall_at_the_diagonal"]
    the_boost_is_the_cross_term["the_boost_is_the_cross_term"]
    the_diffusion_is_a_seat_over_the_room["the_diffusion_is_a_seat_over_the_room"]
    the_diffusion_unwinds_itself["the_diffusion_unwinds_itself"]
    the_one_query_finds_every_target["the_one_query_finds_every_target"]
    the_scan_needs_three["the_scan_needs_three"]
    the_surplus_is_read_one_seat_wider["the_surplus_is_read_one_seat_wider"]
    the_surplus_is_unheard_at_the_host["the_surplus_is_unheard_at_the_host"]
  end
  subgraph Witness["Witness"]
    Witness_a_seat_over_a_seat_is_derived["a_seat_over_a_seat_is_derived"]
  end
  the_diffusion_is_a_seat_over_the_room --> Witness_a_seat_over_a_seat_is_derived

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


-- doorFace: a face over prod whose probes are names — one reading, of the row and the probe
CREATE FUNCTION prod_as_door_face(prod_id integer, probe integer) RETURNS integer[] LANGUAGE sql STABLE AS $$
  SELECT ⟨unread Prod.mk⟩ FROM prod WHERE id = $1 $$;

-- scanQueries: a function of its arguments alone, derived, never stored
-- described by the_scan_needs_three
CREATE FUNCTION scan_queries(arg1 integer) RETURNS integer LANGUAGE sql IMMUTABLE AS $$
  SELECT (CASE WHEN (3 <= arg1) THEN 3 ELSE (arg1 + 1) END) $$;