IndisputableMonolith.Loom.Separation

   1import IndisputableMonolith.Loom.Grammar
   2import IndisputableMonolith.Loom.Readings
   3import IndisputableMonolith.Loom.Semantics
   4import IndisputableMonolith.Loom.CertificateData
   5
   6/-!
   7# The separation witness, checked by the kernel
   8
   9Two pieces of content:
  10
  11* A. every door has some key that opens it, and one master key locks every door,
  12* B. every door has some key that locks it, and one master key opens every door.
  13
  14The second is a security hole and the first is not. They assert the same two relations
  15under the same two quantifier patterns and differ only in which relation gets the
  16universal power, so a multiset of ground facts holds the same entries for both, and the
  17codebook was chosen by exhaustive search so that both cost the same number of one bit
  18acts with the same per loop length multiset. Counting cannot tell them apart.
  19
  20What this module proves, with no hypothesis left dangling and nothing taken on trust
  21except the provenance of the automorphism action:
  22
  23* `weave_witnessA`, `weave_witnessB`: the Lean weaver reproduces the two utterances the
  24  Python encoder emitted, letter for letter. Everything below is therefore about the
  25  grammar in `Grammar.lean` and not about opaque data.
  26* `depth_one_is_blind`, `abelianised_is_blind`: the loop by loop reading and the
  27  abelianised reading are IDENTICAL on the pair. Every carrier that stops at depth one
  28  conflates them, and this is what makes the separation nontrivial rather than a
  29  restatement of a length difference.
  30* `depth_two_separates`: the commutator reading differs.
  31* `no_gauge_image_of_A_is_B`: for every one of the forty eight automorphisms of the
  32  recognition window, every basepoint move, a simultaneous reversal or not, any
  33  respelling and any reordering of the loops, the image of A is not B. So the two are
  34  different meanings and not two spellings of one.
  35
  36The strength of the separation, stated in the terms the institute requires: the gauge
  37group quotiented over has order 96 times the free choice of basepoint word, the check
  38covers all 48 automorphism images exactly (`autSubst_length`), and the two invariants
  39differ in one coordinate of twenty one, which is the smallest possible margin and is
  40exact rather than within a tolerance, because the invariant lands in a finite set.
  41-/
  42
  43namespace IndisputableMonolith
  44namespace Loom
  45namespace Certificate
  46
  47-- ---------------------------------------------------------------------------
  48-- the content, as content
  49-- ---------------------------------------------------------------------------
  50
  51/-- The four shared names, as codebook indices. -/
  52def door : Nat := 0
  53def key : Nat := 1
  54def opens : Nat := 2
  55def locks : Nat := 3
  56
  57/-- The codebook the search chose: it is the one under which no length statistic can
  58separate the pair, which makes the test harder rather than easier. Which codebook is
  59used is a free convention, and `invariant_substConfig` is why. Taken from the emitted
  60certificate rather than written out here, because the search rechooses it whenever the
  61encoder changes. -/
  62def cb : Codebook := cbData
  63
  64def opensKeyDoor : Expr := .atom opens [key, door] false
  65def locksKeyDoor : Expr := .atom locks [key, door] false
  66
  67/-- Every door has some key that opens it. -/
  68def everyDoorSomeKeyOpens : Expr := .quant true door (.quant false key opensKeyDoor)
  69/-- One master key opens every door. -/
  70def someKeyEveryDoorOpens : Expr := .quant false key (.quant true door opensKeyDoor)
  71/-- Every door has some key that locks it. -/
  72def everyDoorSomeKeyLocks : Expr := .quant true door (.quant false key locksKeyDoor)
  73/-- One master key locks every door. -/
  74def someKeyEveryDoorLocks : Expr := .quant false key (.quant true door locksKeyDoor)
  75
  76/-- Safe: keys open doors one at a time, and one master key locks up. -/
  77def witnessA : Expr := .conj everyDoorSomeKeyOpens someKeyEveryDoorLocks
  78/-- Unsafe: one master key opens every door. -/
  79def witnessB : Expr := .conj everyDoorSomeKeyLocks someKeyEveryDoorOpens
  80
  81/-- The weaver in `Grammar.lean` produces exactly the utterance the Python encoder
  82produced, so the certificate below is about the grammar and not about a coincidence of
  83transcription. -/
  84theorem weave_witnessA : weave cb witnessA = cfgA := by decide
  85theorem weave_witnessB : weave cb witnessB = cfgB := by decide
  86
  87/-- Both utterances pass the checker. -/
  88theorem wellFormed_A : wellFormed cfgA = true := by
  89  rw [← weave_witnessA]; exact wellFormed_weave cb witnessA
  90theorem wellFormed_B : wellFormed cfgB = true := by
  91  rw [← weave_witnessB]; exact wellFormed_weave cb witnessB
  92
  93-- ---------------------------------------------------------------------------
  94-- the homomorphism is a homomorphism
  95-- ---------------------------------------------------------------------------
  96
  97/-- The five generator images really are inverse pairs of determinant one, so `base` is
  98a homomorphism from the free group of rank five into `SL(2, ZMod 3)`. Decided, not
  99assumed. -/
 100theorem base_ok : Table.ok base = true := by decide
 101
 102/-- And so is every one of its forty eight relabellings, for free, from
 103`ok_tableOfSubst`. No table beyond `base` is trusted data: Lean computes each
 104composite itself from the automorphism's action on the generators. -/
 105theorem tableOfSubst_ok (σ : Subst) : Table.ok (tableOfSubst base σ) = true :=
 106  ok_tableOfSubst base base_ok σ
 107
 108/-- All forty eight automorphisms of the window are covered. -/
 109theorem autSubst_length : autSubst.length = 48 := by decide
 110
 111/-- The composite tables the Python search reported agree, matrix for matrix, with the
 112ones Lean computes from the substitution words. Two independent routes to the same
 113forty eight homomorphisms. -/
 114theorem autTables_eq : autTables = autSubst.map (tableOfSubst base) := by decide
 115
 116-- ---------------------------------------------------------------------------
 117-- what the shallow readings see, and what they do not
 118-- ---------------------------------------------------------------------------
 119
 120/-- The loop by loop reading is BLIND: identical on the pair. Any carrier whose reading
 121of an utterance is a multiset of per loop quantities conflates A with B. -/
 122theorem depth_one_is_blind : (invariant base cfgA).1 = (invariant base cfgB).1 := by
 123  decide
 124
 125/-- The abelianised reading is blind too. This is the unique canonical quotient a bag of
 126relations performs, so the conflation is not an artifact of one implementation. -/
 127theorem abelianised_is_blind : abelBag cfgA = abelBag cfgB := by decide
 128
 129/-- Depth two separates. One coordinate of twenty one, exactly, in a finite set. -/
 130theorem depth_two_separates : (invariant base cfgA).2 ≠ (invariant base cfgB).2 := by
 131  decide
 132
 133theorem invariant_separates : invariant base cfgA ≠ invariant base cfgB := by
 134  intro h
 135  exact depth_two_separates (congrArg Prod.snd h)
 136
 137-- ---------------------------------------------------------------------------
 138-- the gauge group, and the theorem
 139-- ---------------------------------------------------------------------------
 140
 141/-- A gauge image of an utterance: relabel the generators by an automorphism of the
 142window, optionally reverse every loop at once, move the shared basepoint by one word,
 143and respell everything freely. Reordering the loops is handled by the permutation
 144hypothesis of the theorem below, because an utterance is a multiset. -/
 145def gaugeImage (σ : Subst) (flip : Bool) (g : Word) (c : Config) : Config :=
 146  reduceConfig
 147    ((if flip then (substConfig σ c).map invWord else substConfig σ c).map (conjWord g))
 148
 149theorem invariant_gaugeImage (σ : Subst) (flip : Bool) (g : Word) (c : Config) :
 150    invariant base (gaugeImage σ flip g c) = invariant (tableOfSubst base σ) c := by
 151  rw [gaugeImage, invariant_reduceConfig base base_ok,
 152    invariant_conjWord base base_ok]
 153  cases flip with
 154  | false => rw [if_neg (by simp), invariant_substConfig]
 155  | true =>
 156    rw [if_pos rfl, invariant_map_invWord base base_ok, invariant_substConfig]
 157
 158/-- The check: under every one of the forty eight relabellings, the invariant of A stays
 159different from the invariant of B. -/
 160def separatesEverywhere : Bool :=
 161  autSubst.all fun σ => invariant (tableOfSubst base σ) cfgA != invariant base cfgB
 162
 163theorem separates_everywhere : separatesEverywhere = true := by decide
 164
 165/-- THE SEPARATION THEOREM. No gauge transformation of A is B: not a relabelling by any
 166automorphism of the recognition window, not a reversal of every loop, not a move of the
 167shared basepoint, not a respelling, and not a reordering. So A and B are two meanings
 168and not two spellings of one, while every depth one reading of them is identical. -/
 169theorem no_gauge_image_of_A_is_B (σ : Subst) (hσ : σ ∈ autSubst) (flip : Bool)
 170    (g : Word) (c : Config) (hc : List.Perm c (gaugeImage σ flip g cfgA)) :
 171    invariant base c ≠ invariant base cfgB := by
 172  rw [invariant_perm base hc, invariant_gaugeImage]
 173  have h := List.all_eq_true.mp separates_everywhere σ hσ
 174  simpa only [bne_iff_ne, ne_eq] using h
 175
 176/-- The same statement about the utterances themselves. -/
 177theorem gauge_image_ne_B (σ : Subst) (hσ : σ ∈ autSubst) (flip : Bool) (g : Word)
 178    (c : Config) (hc : List.Perm c (gaugeImage σ flip g cfgA)) : c ≠ cfgB := by
 179  intro h
 180  exact no_gauge_image_of_A_is_B σ hσ flip g c hc (by rw [h])
 181
 182/-- And the whole thing as one statement about CONTENT: the two formulas receive
 183utterances that no gauge transformation identifies, though every depth one reading of
 184them agrees. -/
 185theorem witnesses_separated (σ : Subst) (hσ : σ ∈ autSubst) (flip : Bool) (g : Word)
 186    (c : Config) (hc : List.Perm c (gaugeImage σ flip g (weave cb witnessA))) :
 187    c ≠ weave cb witnessB := by
 188  rw [weave_witnessA] at hc
 189  rw [weave_witnessB]
 190  exact gauge_image_ne_B σ hσ flip g c hc
 191
 192-- ---------------------------------------------------------------------------
 193-- the second witness: the rival readings are defined here and proved blind
 194-- ---------------------------------------------------------------------------
 195
 196/-! The flagship above is conflated by a multiset of ground facts, which is the honest
 197shape of a relational message, but it IS seen by a stronger rival that also carries every
 198parent to child label of the parse tree. So the flagship does not settle the question
 199against that rival, and this second pair does.
 200
 201The pair, with `door` and `key` as the two bound names:
 202
 203* C. some door locks every key, and every door opens every key,
 204* D. some door opens every key, and every door locks every key.
 205
 206Which relation is asserted of everything and which only of one thing: the same question the
 207flagship asks, put so that a labelled tree cannot answer it either. The atom in each branch
 208hangs off a `forall key` node, so the multiset of parent to child label pairs is identical
 209and the two atoms are exchangeable between the branches.
 210
 211Unlike the flagship, this pair is separated under EVERY one of the 384 codebooks, while act
 212count and the amplitude reading separate it under NONE of them. The codebook below is the
 213one that also equalises the per loop length multiset, so both utterances cost 88 acts with
 214the same multiset of loop lengths. -/
 215
 216def cb2 : Codebook := cbData2
 217
 218def opensDoorKey : Expr := .atom opens [door, key] false
 219def locksDoorKey : Expr := .atom locks [door, key] false
 220
 221/-- Some door locks every key. -/
 222def someDoorLocksEveryKey : Expr := .quant false door (.quant true key locksDoorKey)
 223/-- Some door opens every key. -/
 224def someDoorOpensEveryKey : Expr := .quant false door (.quant true key opensDoorKey)
 225/-- Every door opens every key. -/
 226def everyDoorOpensEveryKey : Expr := .quant true door (.quant true key opensDoorKey)
 227/-- Every door locks every key. -/
 228def everyDoorLocksEveryKey : Expr := .quant true door (.quant true key locksDoorKey)
 229
 230def witnessC : Expr := .conj someDoorLocksEveryKey everyDoorOpensEveryKey
 231def witnessD : Expr := .conj someDoorOpensEveryKey everyDoorLocksEveryKey
 232
 233theorem weave_witnessC : weave cb2 witnessC = cfgC := by decide
 234theorem weave_witnessD : weave cb2 witnessD = cfgD := by decide
 235
 236/-- The two differ as trees. Necessary and nowhere near sufficient, since two formulas can
 237differ as trees and agree as claims; the model below is what settles it. -/
 238theorem witnessC_ne_witnessD : witnessC ≠ witnessD := by decide
 239
 240/-- THE TWO ARE DIFFERENT CLAIMS, and on the plainest reading there is: one universe of
 241two elements shared by both bound names, `opens` holding of every pair, `locks` holding of
 242`(0,0)` and `(0,1)`. Then C holds, because door 0 locks both keys and everything opens
 243everything, and D fails, because it needs door 1 to lock key 0 and it does not.
 244
 245This is the theorem that keeps the separation from being an embarrassment. Had the two been
 246logically equivalent, separating them would show the language drawing a distinction the
 247logic does not, which is a defect and not a witness. Note what is NOT assumed: the two
 248names range over the same universe, so nothing here rests on doors and keys being different
 249kinds of thing. -/
 250def witnessModel : Model 2 where
 251  holds p args :=
 252    if p = opens then true
 253    else if p = locks then
 254      match args with
 255      | [x, _] => x = 0
 256      | _ => false
 257    else false
 258
 259theorem witnessC_and_D_are_different_claims :
 260    SeparatedBy witnessModel (fun _ => 0) witnessC witnessD := by decide
 261
 262/-- Spelled out: the first holds and the second fails. -/
 263theorem witnessC_holds : evalExpr witnessModel (fun _ => 0) witnessC = true := by decide
 264theorem witnessD_fails : evalExpr witnessModel (fun _ => 0) witnessD = false := by decide
 265
 266/-- RIVAL ONE IS BLIND. The multiset of ground facts and binder occurrences is the same
 267for both. Stated as a permutation, which is equality of multisets. -/
 268theorem groundBag_blind : List.Perm (groundBag witnessC) (groundBag witnessD) := by decide
 269
 270/-- RIVAL TWO IS BLIND, and this is the one the flagship failed against. Every parent to
 271child label pair of the parse tree, with denial folded into the atom labels, is the same
 272for both. So no reading of this content as a collection of locally labelled facts can tell
 273the two apart. -/
 274theorem adjacencyBag_blind :
 275    List.Perm (adjacencyBag witnessC) (adjacencyBag witnessD) := by decide
 276
 277/-- And the depth one reading of the two utterances is blind as well, so nothing that
 278reads loop by loop separates them either. -/
 279theorem depth_one_is_blind2 : (invariant base cfgC).1 = (invariant base cfgD).1 := by
 280  decide
 281
 282theorem abelianised_is_blind2 : abelBag cfgC = abelBag cfgD := by decide
 283
 284/-- Depth two separates, under the same single homomorphism that certifies the flagship. -/
 285theorem depth_two_separates2 : (invariant base cfgC).2 ≠ (invariant base cfgD).2 := by
 286  decide
 287
 288theorem wellFormed_C : wellFormed cfgC = true := by
 289  rw [← weave_witnessC]; exact wellFormed_weave cb2 witnessC
 290theorem wellFormed_D : wellFormed cfgD = true := by
 291  rw [← weave_witnessD]; exact wellFormed_weave cb2 witnessD
 292
 293def separatesEverywhere2 : Bool :=
 294  autSubst.all fun σ => invariant (tableOfSubst base σ) cfgC != invariant base cfgD
 295
 296theorem separates_everywhere2 : separatesEverywhere2 = true := by decide
 297
 298/-- THE SECOND SEPARATION THEOREM, and the strongest statement in this file. Two pieces of
 299content that every reading of content as locally labelled facts identifies, and that no
 300gauge transformation of the utterance identifies. -/
 301theorem no_gauge_image_of_C_is_D (σ : Subst) (hσ : σ ∈ autSubst) (flip : Bool)
 302    (g : Word) (c : Config) (hc : List.Perm c (gaugeImage σ flip g cfgC)) :
 303    invariant base c ≠ invariant base cfgD := by
 304  rw [invariant_perm base hc, invariant_gaugeImage]
 305  have h := List.all_eq_true.mp separates_everywhere2 σ hσ
 306  simpa only [bne_iff_ne, ne_eq] using h
 307
 308theorem gauge_image_ne_D (σ : Subst) (hσ : σ ∈ autSubst) (flip : Bool) (g : Word)
 309    (c : Config) (hc : List.Perm c (gaugeImage σ flip g cfgC)) : c ≠ cfgD := by
 310  intro h
 311  exact no_gauge_image_of_C_is_D σ hσ flip g c hc (by rw [h])
 312
 313theorem witnesses2_separated (σ : Subst) (hσ : σ ∈ autSubst) (flip : Bool) (g : Word)
 314    (c : Config) (hc : List.Perm c (gaugeImage σ flip g (weave cb2 witnessC))) :
 315    c ≠ weave cb2 witnessD := by
 316  rw [weave_witnessC] at hc
 317  rw [weave_witnessD]
 318  exact gauge_image_ne_D σ hσ flip g c hc
 319
 320/-!
 321## A conjecture, tagged as one
 322
 323Ken's ninth judgment `recognize_ne_defeq` is held open. The loop language suggests a
 324witness: a trivial loop, one that freely reduces to the empty word, is a walk that
 325returns without distinguishing anything, and that is exactly the shape of definitional
 326equality, while a nontrivial loop is a closed walk that cannot be contracted and so
 327records a distinction that had to be made. If that reading is right then
 328`reduceWord w = []` is the decidable side of `defeq` and any `w` with
 329`reduceWord w ≠ []` witnesses `recognize_ne_defeq`. CONJECTURE: not proved here, and
 330the gap is that nothing in this module connects the free group to Ken's judgment types.
 331-/
 332
 333#print axioms weave_witnessA
 334#print axioms weave_witnessB
 335#print axioms base_ok
 336#print axioms autTables_eq
 337#print axioms depth_one_is_blind
 338#print axioms abelianised_is_blind
 339#print axioms depth_two_separates
 340#print axioms separates_everywhere
 341#print axioms no_gauge_image_of_A_is_B
 342#print axioms witnesses_separated
 343#print axioms weave_witnessC
 344#print axioms witnessC_ne_witnessD
 345#print axioms witnessC_and_D_are_different_claims
 346#print axioms witnessC_holds
 347#print axioms witnessD_fails
 348#print axioms groundBag_blind
 349#print axioms adjacencyBag_blind
 350#print axioms depth_one_is_blind2
 351#print axioms depth_two_separates2
 352#print axioms separates_everywhere2
 353#print axioms no_gauge_image_of_C_is_D
 354#print axioms witnesses2_separated
 355
 356end Certificate
 357end Loom
 358end IndisputableMonolith
 359