IndisputableMonolith.Loom.Grammar

   1import IndisputableMonolith.Loom.Core
   2
   3/-!
   4# The grammar: content in, an utterance out
   5
   6`Expr` is the inductive type of content the language accepts, and `weave` is the total
   7function that turns a piece of content into a configuration of closed walks. Five
   8production rules, each one forced by asking which operation on configurations has the
   9algebraic properties the content operator has:
  10
  11* a relation applied to roles in order is an ordered PRODUCT of letters, opened and
  12  closed by the relation's own letter,
  13* denial is INVERSION, the only involution the group offers,
  14* conjunction is MULTISET UNION, the only unordered idempotent join,
  15* a universal is a BINDER LOOP with the body CONJUGATED BY THAT SAME ORIENTED LOOP,
  16  because "inside" is conjugation and the body sits inside the binder as uttered,
  17* an existential is the same with the binder reversed, which is not a second choice but
  18  a consequence: `not (forall x (not B))` gives back exactly that.
  19
  20Conjugating by the binder's own oriented loop rather than by the bare letter is what makes
  21a quantifier's TYPE visible from inside its scope: an atom's loop then records whether each
  22binder above it was universal or existential, not merely which name it bound. The bare
  23letter loses that, and when two conjuncts bind the same names in the same order it lets
  24atoms be exchanged between a universal and an existential branch without moving the
  25utterance. Measured on 3,800 pieces of irredundant content, the bare letter conflates 860
  26pairs of genuinely different content and this rule conflates 1, which is a pair with no
  27separating model and so is correctly conflated.
  28
  29Two rules make an utterance rather than a fragment. Every utterance carries the FRAME
  30loop, the walk that closes the complete recognition window, because with a single loop
  31there is nothing to be oriented against and denial would be inexpressible. And every
  32loop is freely reduced, because spelling is not content.
  33
  34`Expr` is already in negation normal form: denial rides on the atom. That is not a
  35preprocessing convenience, it is what the algebra does. Inverting a binder loop flips
  36its sign, which turns a denied universal into an existential, so the carrier represents
  37every formula it accepts in this form. The denial of a conjunction is therefore outside
  38the language, since inverting a multiset of loops denies each loop separately, giving
  39"neither" rather than "not both". There is no join on configurations, so the language
  40has no disjunction, and `Expr` cannot express one: the refusal is structural rather
  41than a runtime error.
  42-/
  43
  44namespace IndisputableMonolith
  45namespace Loom
  46
  47/-- Content the language accepts. Names are indices into a shared codebook, so nothing
  48anonymous and nothing per-claim is ever named. -/
  49inductive Expr where
  50  /-- A relation applied to role fillers in role order, denied or not. -/
  51  | atom (pred : Nat) (args : List Nat) (denied : Bool) : Expr
  52  /-- Both, unordered. -/
  53  | conj (a b : Expr) : Expr
  54  /-- A quantifier over a shared name: universal when the flag is true. -/
  55  | quant (universal : Bool) (binder : Nat) (body : Expr) : Expr
  56deriving DecidableEq, Repr
  57
  58/-- Which signed generator each shared name is attached to. This is the whole of what
  59sender and receiver must already share. It is *not* pure gauge, contrary to what this
  60comment said until 2026-07-28: `Loom.Attachment.six_atoms_not_forced` shows the gauge
  61group is too small to act transitively on the labellings, and `fourteen_orbits_insufficient`
  62with `fifteen_orbits_suffice` pin the minimum at fifteen orbits. So a codebook carries a
  63residue of real choice that no relabelling removes. -/
  64abbrev Codebook := List Int
  65
  66def letterOf (cb : Codebook) (n : Nat) : Int := cb.getD n 0
  67
  68/-- The five production rules, as one total function. -/
  69def weaveBody (cb : Codebook) : Expr → Config
  70  | .atom pred args denied =>
  71      let p := letterOf cb pred
  72      let w := reduceWord (p :: (args.map (letterOf cb) ++ [p]))
  73      [if denied then invWord w else w]
  74  | .conj a b => weaveBody cb a ++ weaveBody cb b
  75  | .quant universal binder body =>
  76      let q := letterOf cb binder
  77      let marker : Word := if universal then [q] else [-q]
  78      marker :: (weaveBody cb body).map (conjWord marker)
  79
  80/-- Content to utterance: the body, framed and freely reduced. Total, and every
  81question about its output is answerable in linear time. -/
  82def weave (cb : Codebook) (e : Expr) : Config :=
  83  reduceConfig ([frameGen] :: weaveBody cb e)
  84
  85/-- SOUNDNESS of the weaver against the checker: everything the grammar produces is
  86well formed, so the checker never has to reject an honest utterance. -/
  87theorem wellFormed_weave (cb : Codebook) (e : Expr) : wellFormed (weave cb e) = true :=
  88  wellFormed_reduceConfig_frame _
  89
  90/-- The invariant of a woven utterance does not depend on how its loops are spelled. -/
  91theorem invariant_weave_reduce (T : Table) (hT : Table.ok T = true) (cb : Codebook)
  92    (e : Expr) :
  93    invariant T (weave cb e) = invariant T ([frameGen] :: weaveBody cb e) :=
  94  invariant_reduceConfig T hT _
  95
  96/-- Depth one cannot see nesting. Every loop of a quantified body is a conjugate of the
  97corresponding loop of the body itself, so the loop traces of the two agree pointwise;
  98only the commutators of the loops with each other move. This is the theorem behind the
  99measured fact that loop traces alone fail to separate the witness. -/
 100theorem trN_weaveBody_quant (T : Table) (hT : Table.ok T = true) (cb : Codebook)
 101    (universal : Bool) (binder : Nat) (body : Expr) :
 102    ((weaveBody cb (.quant universal binder body)).tail.map
 103        (fun w => Mat.trN (evalWord T w)))
 104      = (weaveBody cb body).map (fun w => Mat.trN (evalWord T w)) := by
 105  simp only [weaveBody, List.tail_cons, List.map_map]
 106  apply List.map_congr_left
 107  intro w _
 108  simp only [Function.comp_apply, trN_conjWord T hT]
 109
 110#print axioms wellFormed_weave
 111#print axioms trN_weaveBody_quant
 112
 113end Loom
 114end IndisputableMonolith
 115