voice — a product as an assay, on Witness

27 receipts inline · 197 lines · pinned 8328df9a5ea3c4bc — shasum -a 256 of this file, cut to 16, as pins has it · lake env lean voice.lean prints nothing when every receipt passes

import Witness
open Room Face Witness
set_option autoImplicit false

-- the voice as a tower of faces (isaac at the table, 2026-09-08: "if things get less interesting,
-- some W got dropped"). a field is where a voice has grain: the contexts it has heard. the face at
-- width k reads a context only up to k bytes long; wider is a wider face, and the tower is exact
-- (Face.the_widening_is_exact). two voices alike at width k and distinct are parted one width up
-- (a_wider_seat_reads_the_remainder), and two fields that cover every context up to k are alike at
-- k whatever they are (the saturation counter's voice met at twenty million charges). the
-- instrument is not the reading at one width but the PARTING WIDTH: the least k at which the faces
-- part two voices on what they have heard. below it the identification is licensed; at it the
-- remainder is real; the number is the reading.

namespace Voice.Treaty

structure Field where
  grain : List (List Nat)

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

def ctxBeq : List Nat → List Nat → Bool
  | [], [] => true
  | [], _ :: _ => false
  | _ :: _, [] => false
  | a :: as, b :: bs => Nat.beq a b && ctxBeq as bs

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

def has (f : Field) (c : List Nat) : Bool := enrolled ctxBeq f.grain c

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

def voiceFace (k : Nat) : Face :=
  ⟨Field, List Nat, Bool, fun f c => cond (Nat.ble c.length k) (has f c) false⟩

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

def agreeTo (k : Nat) (f g : Field) : Prop := ∀ c : List Nat, Nat.ble c.length k = true → has f c = has g c

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

def heard (f g : Field) : List (List Nat) := f.grain ++ g.grain

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

def partsAt (k : Nat) (f g : Field) : Bool :=
  (heard f g).any (fun c => Nat.ble c.length k && !(has f c == has g c))

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

def widest (f g : Field) : Nat := longest (heard f g)

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

def partingFrom (f g : Field) : Nat → Nat → Nat
  | _, 0 => widest f g + 1
  | k, fuel + 1 => cond (partsAt k f g) k (partingFrom f g (k + 1) fuel)

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

def partingWidth (f g : Field) : Nat := partingFrom f g 0 (widest f g + 1)

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

def full (k : Nat) (f : Field) : Prop := ∀ c : List Nat, Nat.ble c.length k = true → has f c = true

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

def isaacVoice : Field := ⟨[[1], [2], [1, 2], [2, 3], [1, 2, 3], [1, 2, 3, 4, 5]]⟩

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

def fableVoice : Field := ⟨[[1], [2], [1, 2], [2, 3], [1, 2, 3], [2, 3, 4, 5, 6]]⟩

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

def quoted : Field := ⟨[[1], [2], [1, 2], [2, 3], [1, 2, 3], [1, 2, 3, 4, 5], [2, 3, 4, 5, 6]]⟩

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

def atThree : Bool := partsAt 3 isaacVoice fableVoice

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

def atFive : Bool := partsAt 5 isaacVoice fableVoice

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

def theWidth : Nat := partingWidth isaacVoice fableVoice

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

def quotedWidth : Nat := partingWidth quoted quoted

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

def readThree : Bool := (voiceFace 3).obs isaacVoice [1, 2, 3, 4, 5]

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

def readFive : Bool := (voiceFace 5).obs isaacVoice [1, 2, 3, 4, 5]

#guard atThree == false
#guard atFive == true
#guard theWidth == 5
#guard quotedWidth == 6
#guard readThree == false
#guard readFive == true
#guard widest isaacVoice fableVoice == 5

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

theorem the_face_at_a_width_reads_agreement (k : Nat) (f g : Field) :
    alike (voiceFace k) f g ↔ agreeTo k f g :=
  ⟨fun h c hc => by
      have hf : cond (Nat.ble c.length k) (has f c) false = cond (Nat.ble c.length k) (has g c) false := h c
      rw [hc] at hf
      exact hf,
   fun h c => by
      show cond (Nat.ble c.length k) (has f c) false = cond (Nat.ble c.length k) (has g c) false
      cases hc : Nat.ble c.length k with
      | true => exact h c hc
      | false => rfl⟩

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

theorem a_wider_agreement_is_a_narrower_one (k : Nat) (f g : Field) (h : agreeTo (k + 1) f g) :
    agreeTo k f g :=
  fun c hc => h c (ble_trans c.length k (k + 1) hc (ble_le_succ k))

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

theorem a_context_that_parts_parts_the_face (k : Nat) (f g : Field) (c : List Nat)
    (hc : Nat.ble c.length k = true) (hd : has f c ≠ has g c) : ¬ agreeTo k f g :=
  fun ha => hd (ha c hc)

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

theorem full_fields_are_alike (k : Nat) (f g : Field) (hf : full k f) (hg : full k g) :
    agreeTo k f g :=
  fun c hc => (hf c hc).trans (hg c hc).symm

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

theorem no_context_parts_a_voice_from_itself (k : Nat) (f : Field) :
    ∀ l : List (List Nat), l.any (fun c => Nat.ble c.length k && !(has f c == has f c)) = false
  | [] => rfl
  | c :: cs => by
      show ((Nat.ble c.length k && !(has f c == has f c))
        || List.any cs (fun c => Nat.ble c.length k && !(has f c == has f c))) = false
      have hp : (Nat.ble c.length k && !(has f c == has f c)) = false := by
        cases has f c <;> cases Nat.ble c.length k <;> rfl
      rw [hp]
      exact no_context_parts_a_voice_from_itself k f cs

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

theorem nothing_is_heard_beyond_the_widest (f g : Field) (c : List Nat) (hc : c ∈ heard f g) :
    Nat.ble c.length (widest f g) = true :=
  (by (apply Room.the_longest_reaches_each <;> assumption))

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

theorem a_voice_never_parts_itself (k : Nat) (f : Field) : partsAt k f f = false :=
  (by (apply no_context_parts_a_voice_from_itself <;> fail))

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

end Voice.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 Voice_Treaty["Voice.Treaty"]
    a_context_that_parts_parts_the_face["a_context_that_parts_parts_the_face"]
    a_voice_never_parts_itself["a_voice_never_parts_itself"]
    a_wider_agreement_is_a_narrower_one["a_wider_agreement_is_a_narrower_one"]
    full_fields_are_alike["full_fields_are_alike"]
    no_context_parts_a_voice_from_itself["no_context_parts_a_voice_from_itself"]
    nothing_is_heard_beyond_the_widest["nothing_is_heard_beyond_the_widest"]
    the_face_at_a_width_reads_agreement["the_face_at_a_width_reads_agreement"]
  end
  a_voice_never_parts_itself --> no_context_parts_a_voice_from_itself

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/voice.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 field (
  id serial PRIMARY KEY
);
CREATE TABLE field_grain (
  field_id integer NOT NULL REFERENCES field(id),
  position integer NOT NULL,
  c0 integer NOT NULL
);

-- partingFrom: derived, not yet drawn (data over Voice.Treaty.Field)

-- parting_width: derived, not yet drawn (calls parting_from, widest, beyond the fragment)

-- widest: derived, not yet drawn (data over Voice.Treaty.Field)

-- heard: derived, not yet drawn (a list of lists — the shadow holds no jagged array)

-- has: a check, derived, never stored
-- described by a_context_that_parts_parts_the_face, no_context_parts_a_voice_from_itself
CREATE FUNCTION has(field_id integer, arg2 integer[]) RETURNS boolean LANGUAGE sql STABLE AS $$
  SELECT (arg2 = ANY(SELECT unnest((SELECT array_agg(c ORDER BY position) FROM field_grain c WHERE c.field_id = field.id)))) FROM field WHERE id = $1 $$;

-- ctxBeq: derived, not yet drawn (a function over List Nat)