locus: Blueprint

6.2. Composition operators on descriptions🔗

Definition6.2.1
uses 0
Used by 5
Reverse dependency previews
Preview
Theorem 6.2.2
Loading preview
Reverse dependency preview content is loaded from the rendered-fragment cache.
✓L∃∀N
Tagsbridgednot audited

Three operators on descriptions, each computed without reference to the library. The parallel product d_1 \parallel_{\mathrm d} d_2 lists the roots, sites and items of d_1 and then those of d_2, renumbered past those of d_1; its outer names are those of d_1 followed by those of d_2 not among them, so that a shared outer name is one name. The merge \mathrm{merge}_{\mathrm d}(d) has one root, which replaces every root of d as a parent. For a list H of names, \mathrm{hid}(H; d) is the list of the outer names of d that occur in H, in the order of d; the closure \mathrm{close}_{\mathrm d}(H; d) appends one edge for each entry of \mathrm{hid}(H; d), sends every link to a hidden name x to the edge

e_{H,d}(x) \;=\; n_d + (\text{the first position of } x \text{ in } \mathrm{hid}(H; d)), \qquad n_d \text{ the number of items of } d ,

and keeps the other outer names.

Class: BD.ppar, BD.merge, BD.close BRIDGED; BD.hidden not audited.

Lean code for Definition6.2.1●4 definitions
  • defdefined in Logic/Compose.lean
    complete
    def ppar {Ctrl : Type} (d₁ d₂ : BD Ctrl) : BD Ctrl
    def ppar {Ctrl : Type} (d₁ d₂ : BD Ctrl) :
  BD Ctrl
    **UNBRIDGED** (no theorem yet relates this to the library's parallel
product; the statement is `PparBridgeStatement`, `Logic/ComposeBridge.lean`).
Intended as the parallel product `d₁ ∥ d₂` (TR-580 Def 9.13): regions of `d₁` then of
`d₂`, sites likewise, supports disjoint, and SHARED OUTER NAMES
IDENTIFIED (that is the linking of ports). Inner names are concatenated;
it is used only where both have none.
  • defdefined in Logic/Compose.lean
    complete
    def merge {Ctrl : Type} (d : BD Ctrl) : BD Ctrl
    def merge {Ctrl : Type} (d : BD Ctrl) :
  BD Ctrl
    **UNBRIDGED** (`MergeBridgeStatement`). Intended as composition with
`merge_m` (TR-580 §10): the regions merged into one.
  • defdefined in Logic/Compose.lean
    complete
    def close {Ctrl : Type} (hide : List Nat) (d : BD Ctrl) : BD Ctrl
    def close {Ctrl : Type} (hide : List Nat)
  (d : BD Ctrl) : BD Ctrl
    **UNBRIDGED** (`CloseBridgeStatement`). Intended as the closure `/hide`
(TR-580 §9): each outer name in `hide` becomes a new edge
(appended to the support); the others stay.
  • defdefined in Logic/Compose.lean
    complete
    def hidden {Ctrl : Type} (hide : List Nat) (d : BD Ctrl) : List Nat
    def hidden {Ctrl : Type} (hide : List Nat)
  (d : BD Ctrl) : List Nat
    The outer names among `hide` that `d` has, in order.
Theorem6.2.2
Statement uses 2
Statement dependency previews
Preview
Definition 6.1.1
Loading preview
Statement dependency preview content is loaded from the rendered-fragment cache.
used by 0✓L∃∀N

The parallel product on descriptions is the library's parallel product \parallel (Definition 4.3.1) up to support equivalence. For every signature, d_1 checked and fitting \varepsilon \to \langle m_1, Y_1 \rangle, d_2 checked and fitting \varepsilon \to \langle m_2, Y_2 \rangle, and every permutation \pi such that no number is a node or an edge of both \llbracket d_1 \rrbracket and \pi \bullet \llbracket d_2 \rrbracket, the description d_1 \parallel_{\mathrm d} d_2 is checked, fits \varepsilon \to \langle m_1 + m_2, Y_1 \cup Y_2 \rangle, and

\llbracket d_1 \parallel_{\mathrm d} d_2 \rrbracket \;\bumpeq\; \llbracket d_1 \rrbracket \parallel (\pi \bullet \llbracket d_2 \rrbracket) .

The statement is for every \pi satisfying that disjointness condition, and such a \pi exists for every such d_1, d_2: so there are a \pi, a check and a fit of d_1 \parallel_{\mathrm d} d_2 for which the equivalence holds, with no hypothesis on \pi left. The theorem is applied to a small concrete agent.

Rests on NEW: BD.Fits, Inst.a1, Inst.a2, Perm; not audited: Big, BigH.tr, LiG.Disjoint, Test.T, Test.sig, nset.

Lean code for Theorem6.2.2●5 declarations
  • theoremdefined in Logic/ComposeBridgePar.lean
    complete
    theorem pparBridge {Ctrl : Type} [DecidableEq Ctrl] (S : Sig Ctrl) :
  PparBridgeStatement S
    theorem pparBridge {Ctrl : Type}
  [DecidableEq Ctrl] (S : Sig Ctrl) :
  PparBridgeStatement S
    **B1, PROVED**: for checked ground data `d₁ : ε → J₁`, `d₂ : ε → J₂` and
every `π` with `|⟦d₁⟧| ∩ |π • ⟦d₂⟧| = ∅`,
`⟦ppar d₁ d₂⟧ ≏ ⟦d₁⟧ ‖ π • ⟦d₂⟧`; the witness is
`gluePerm π d₁.n d₂.n • ⟦ppar d₁ d₂⟧ = ⟦d₁⟧ ‖ π • ⟦d₂⟧`.
  • defdefined in Logic/ComposeBridge.lean
    complete
    def PparBridgeStatement {Ctrl : Type} [DecidableEq Ctrl] (S : Sig Ctrl) :
  Prop
    def PparBridgeStatement {Ctrl : Type}
  [DecidableEq Ctrl] (S : Sig Ctrl) : Prop
    **B1, parallel product** (PROVED: `pparBridge`). For checked ground data `d₁ : ε → J₁`,
`d₂ : ε → J₂` and any support translation `π` making `π • ⟦d₂⟧` disjoint
from `⟦d₁⟧`:  `⟦ppar d₁ d₂⟧ ≏ ⟦d₁⟧ ‖ π • ⟦d₂⟧`.
(`ppar` renumbers `d₂` after `d₁`; the library's `‖` needs disjoint
supports, hence a translation, and the result is the same up to `≏`
whichever is chosen.)
  • theoremdefined in Logic/ComposeBridgeCor.lean
    complete
    theorem exists_disjointifying {Ctrl : Type} {S : Sig Ctrl} (d₁ d₂ : BD Ctrl)
  (J₁ J₂ : Face) (h₁ : d₁.check S = true) (f₁ : d₁.Fits Face.origin J₁)
  (h₂ : d₂.check S = true) (f₂ : d₂.Fits Face.origin J₂) :
  ∃ π, ⟦d₁⟧.big.L.Disjoint (BigH.tr π ⟦d₂⟧).big.L
    theorem exists_disjointifying {Ctrl : Type}
  {S : Sig Ctrl} (d₁ d₂ : BD Ctrl)
  (J₁ J₂ : Face) (h₁ : d₁.check S = true)
  (f₁ : d₁.Fits Face.origin J₁)
  (h₂ : d₂.check S = true)
  (f₂ : d₂.Fits Face.origin J₂) :
  ∃ π,
    ⟦d₁⟧.big.L.Disjoint
      (BigH.tr π ⟦d₂⟧).big.L
    **A disjointifying translation exists**: for checked ground data `d₁`,
`d₂` there is `π` with `|⟦d₁⟧| ∩ |π • ⟦d₂⟧| = ∅` (`π` sends every number
below `d₂.n` to `d₁.n` or beyond).
  • theoremdefined in Logic/ComposeBridgeCor.lean
    complete
    theorem pparBridge_exists {Ctrl : Type} [DecidableEq Ctrl] (S : Sig Ctrl)
  (d₁ d₂ : BD Ctrl) (J₁ J₂ : Face) (h₁ : d₁.check S = true)
  (f₁ : d₁.Fits Face.origin J₁) (h₂ : d₂.check S = true)
  (f₂ : d₂.Fits Face.origin J₂) :
  ∃ π hd h f,
    SEq S ⟦BD.ppar d₁ d₂⟧ (⟦d₁⟧.par (BigH.tr π ⟦d₂⟧) hd empty_disjoint)
    theorem pparBridge_exists {Ctrl : Type}
  [DecidableEq Ctrl] (S : Sig Ctrl)
  (d₁ d₂ : BD Ctrl) (J₁ J₂ : Face)
  (h₁ : d₁.check S = true)
  (f₁ : d₁.Fits Face.origin J₁)
  (h₂ : d₂.check S = true)
  (f₂ : d₂.Fits Face.origin J₂) :
  ∃ π hd h f,
    SEq S ⟦BD.ppar d₁ d₂⟧
      (⟦d₁⟧.par (BigH.tr π ⟦d₂⟧) hd
        empty_disjoint)
    **B1 with no hypothesis on `π`**: for checked ground data `d₁ : ε → J₁`,
`d₂ : ε → J₂` there is `π` with `|⟦d₁⟧| ∩ |π • ⟦d₂⟧| = ∅` and
`⟦ppar d₁ d₂⟧ ≏ ⟦d₁⟧ ‖ π • ⟦d₂⟧`.
  • theoremdefined in Logic/ComposeBridgeCor.lean
    complete
    theorem pparBridge_a1_a2 :
  ∃ π hd h f,
    SEq Test.sig ⟦BD.ppar Inst.a1 Inst.a2⟧
      (⟦Inst.a1⟧.par (BigH.tr π ⟦Inst.a2⟧) hd empty_disjoint)
    theorem pparBridge_a1_a2 :
  ∃ π hd h f,
    SEq Test.sig ⟦BD.ppar Inst.a1 Inst.a2⟧
      (⟦Inst.a1⟧.par (BigH.tr π ⟦Inst.a2⟧)
        hd empty_disjoint)
    **B1 fires**: `pparBridge` (through `pparBridge_exists`) at `a1`, `a2`:
`∃ π, ⟦ppar a1 a2⟧ ≏ ⟦a1⟧ ‖ π • ⟦a2⟧`, at `ε → ⟨1, {0}⟩ ⊗ ⟨2, {0, 1}⟩`.
Theorem6.2.3
Statement uses 2
Statement dependency previews
Preview
Definition 6.1.1
Loading preview
Statement dependency preview content is loaded from the rendered-fragment cache.
used by 0✓L∃∀N

The merge on descriptions is composition with the library's merge \mathrm{merge}_m^X (Definition 4.3.4). For every signature, every m \ge 1 and every d checked and fitting \varepsilon \to \langle m, X \rangle, the description \mathrm{merge}_{\mathrm d}(d) is checked, fits \varepsilon \to \langle 1, X \rangle, and

\llbracket \mathrm{merge}_{\mathrm d}(d) \rrbracket \;=\; \mathrm{merge}_m^X \circ \llbracket d \rrbracket ,

stated in Lean as the composition relation Comp, as in Theorem 6.1.3. The theorem is applied to a small concrete agent. REFUTED as first stated, without the added hypothesis m \ge 1: for the empty description and m = 0 the one root of \mathrm{merge}_{\mathrm d}(d) has no child, so the description is not checked.

Rests on NEW: BD.Fits, Inst.a2; not audited: BIG, MergeBridgeStatement', Test.T, Test.sig, nset.

Lean code for Theorem6.2.3●5 declarations
  • theoremdefined in Logic/ComposeBridgeProofs.lean
    complete
    theorem mergeBridge' {Ctrl : Type} (S : Sig Ctrl) : MergeBridgeStatement' S
    theorem mergeBridge' {Ctrl : Type}
  (S : Sig Ctrl) : MergeBridgeStatement' S
    **B2′ is PROVED.**
  • defdefined in Logic/ComposeBridge.lean
    complete
    def MergeBridgeStatement' {Ctrl : Type} (S : Sig Ctrl) : Prop
    def MergeBridgeStatement' {Ctrl : Type}
  (S : Sig Ctrl) : Prop
    **B2′, merge** (PROVED: `mergeBridge'`; the restatement forced by `mergeBridge_refuted`).
As `MergeBridgeStatement`, for `1 ≤ m`: for checked ground data
`d : ε → ⟨m, X⟩` with at least one region,
`⟦merge d⟧ = (merge_m ⊗ id_X) ∘ ⟦d⟧`.
  • theoremdefined in Logic/ComposeBridge.lean
    complete
    theorem mergeBridge_refuted {Ctrl : Type} (S : Sig Ctrl) :
  ¬MergeBridgeStatement S
    theorem mergeBridge_refuted {Ctrl : Type}
  (S : Sig Ctrl) : ¬MergeBridgeStatement S
    **B2 is REFUTED as stated.** Countermodel: `d = emptyBD`, `m = 0`,
`X = ∅`. `d` is checked and fits `ε → ⟨0, ∅⟩`; `BD.merge d` has width 1
and no node, so its root has no child and `check` is `false`.
  • defdefined in Logic/ComposeBridge.lean
    complete
    def MergeBridgeStatement {Ctrl : Type} (S : Sig Ctrl) : Prop
    def MergeBridgeStatement {Ctrl : Type}
  (S : Sig Ctrl) : Prop
    **B2, merge** (REFUTED AS STATED, 2026-10-10: `mergeBridge_refuted`; for
`m = 0` the data `merge d` has one root with no child, so it fails
`check` and the `∃ h'` is false. Restatement: `MergeBridgeStatement'`).
For checked ground data `d : ε → ⟨m, X⟩`:
`⟦merge d⟧ = (merge_m ⊗ id_X) ∘ ⟦d⟧`, as an equation of the library's
composition (`merge_m` has no nodes or edges, so the supports are
disjoint and no translation is needed).
  • theoremdefined in Logic/ComposeBridgeCor.lean
    complete
    theorem mergeBridge_a2 :
  ∃ h' f',
    Big.mergeN 2 (nset [0, 1]) ◦ ⟦Inst.a2⟧.big ≃ ⟦BD.merge Inst.a2⟧.big
    theorem mergeBridge_a2 :
  ∃ h' f',
    Big.mergeN 2 (nset [0, 1]) ◦
      ⟦Inst.a2⟧.big ≃
      ⟦BD.merge Inst.a2⟧.big
    **B2′ fires**: `mergeBridge'` at `a2` (`m = 2`, `X = {0, 1}`):
`⟦merge a2⟧ = (merge₂ ⊗ id_{0,1}) ∘ ⟦a2⟧`.
Definition6.2.4
Statement uses 2
Statement dependency previews
Preview
Definition 6.1.1
Loading preview
Statement dependency preview content is loaded from the rendered-fragment cache.
Used by 2
Reverse dependency previews
Preview
Theorem 6.2.5
Loading preview
Reverse dependency preview content is loaded from the rendered-fragment cache.
✓L∃∀N
Tagsnewnot audited

The check \mathrm{ok}(d) of Definition 6.1.1 does not ask that the names of d be listed once. The decidable predicate \mathrm{faceOk}(d), which is separate from \mathrm{ok}(d) and not part of it, holds when no outer name is listed twice and no inner name is listed twice. It gives, for every list H,

\mathrm{faceOk}(d) \;\Longrightarrow\; \text{the outer names of } d \text{ are listed once} \;\wedge\; \mathrm{hid}(H; d) \text{ has no repetition} .

OPEN, and TESTED by a compiled example only: the check o \checkmark_F a of Definition 6.3.1 accepts an occurrence whose list of names X is doubled, whose R \otimes \mathrm{id}_X then repeats outer names; the checker is unchanged.

Class: BD.faceOk NEW; BD.faceOk_outer, hidden_nodup not audited.

Lean code for Definition6.2.4●3 declarations
  • defdefined in Logic/FaceOk.lean
    complete
    def faceOk {Ctrl : Type} (d : BD Ctrl) : Bool
    def faceOk {Ctrl : Type} (d : BD Ctrl) : Bool
    **The faces of `d` are sets**: no outer name and no inner name is
listed twice.
  • theoremdefined in Logic/FaceOk.lean
    complete
    theorem faceOk_outer {Ctrl : Type} {d : BD Ctrl} (h : BD.faceOk d = true) :
  d.outer.Nodup
    theorem faceOk_outer {Ctrl : Type} {d : BD Ctrl}
  (h : BD.faceOk d = true) : d.outer.Nodup
  • theoremdefined in Logic/FaceOk.lean
    complete
    theorem hidden_nodup {Ctrl : Type} {d : BD Ctrl} (h : BD.faceOk d = true)
  (hide : List Nat) : (BD.hidden hide d).Nodup
    theorem hidden_nodup {Ctrl : Type} {d : BD Ctrl}
  (h : BD.faceOk d = true)
  (hide : List Nat) :
  (BD.hidden hide d).Nodup
    Under `faceOk` the hidden names are listed once: the hypothesis of B3′.
Theorem6.2.5
Statement uses 2
Statement dependency previews
Preview
Definition 6.2.1
Loading preview
Statement dependency preview content is loaded from the rendered-fragment cache.
used by 0✓L∃∀N

The closure on descriptions is composition with the library's closure \mathrm{cl}^m_e(X; Y) (Definition 4.3.4). For every signature, every list H and every checked d of width m, let X be the set of entries of \mathrm{hid}(H; d), Y the set of outer names of d not in H, and e = e_{H,d}; then X \cap Y = \emptyset and e is injective on X, and a ground d (no sites, no inner names) fits \varepsilon \to \langle m, X \cup Y \rangle. If d fits \varepsilon \to \langle m, X \cup Y \rangle and \mathrm{hid}(H; d) has no repetition, then \mathrm{close}_{\mathrm d}(H; d) is checked, fits \varepsilon \to \langle m, Y \rangle, and

\llbracket \mathrm{close}_{\mathrm d}(H; d) \rrbracket \;=\; \mathrm{cl}^m_e(X; Y) \circ \llbracket d \rrbracket ,

stated in Lean as the composition relation Comp. The same holds, for d fitting that face (so ground), with \mathrm{faceOk}(d) in place of the hypothesis that \mathrm{hid}(H; d) has no repetition. In the form with no other hypothesis: for d checked, ground, and with \mathrm{faceOk}(d) (or with \mathrm{hid}(H; d) without repetition), and every H, the description \mathrm{close}_{\mathrm d}(H; d) is checked, fits \varepsilon \to \langle m, Y \rangle and satisfies the displayed equation. The theorem is applied to a small concrete agent. REFUTED as first stated, without that hypothesis: for the description with no root, no item and the outer name 5 listed twice, and H = [5], the description \mathrm{close}_{\mathrm d}(H; d) has two edges and the library's composite has one.

Rests on NEW: BD.Fits, BD.faceOk, Inst.a2, Item, Par; not audited: BD.hidden, BD.n, BIG, CloseBridgeStatement', NSet.Disjoint, Test.T, Test.sig, nset.

Lean code for Theorem6.2.5●12 declarations
  • theoremdefined in Logic/ComposeBridgeProofs.lean
    complete
    theorem closeBridge' {Ctrl : Type} (S : Sig Ctrl) : CloseBridgeStatement' S
    theorem closeBridge' {Ctrl : Type}
  (S : Sig Ctrl) : CloseBridgeStatement' S
    **B3′ is PROVED.**
  • defdefined in Logic/ComposeBridge.lean
    complete
    def CloseBridgeStatement' {Ctrl : Type} (S : Sig Ctrl) : Prop
    def CloseBridgeStatement' {Ctrl : Type}
  (S : Sig Ctrl) : Prop
    **B3′, closure** (PROVED: `closeBridge'`; the restatement forced by `closeBridge_refuted`).
As `CloseBridgeStatement`, for data in which no hidden name is listed
twice: `(BD.hidden hide d).Nodup`. (`hinj` is derivable, as it is in
general: `hidden_inj`; it is kept so that the statement's shape is
unchanged.)
  • theoremdefined in Logic/ComposeBridgeProofs.lean
    complete
    theorem closeBridge_faceOk {Ctrl : Type} (S : Sig Ctrl) (d : BD Ctrl)
  (hide : List Nat) (h : d.check S = true) (hf : BD.faceOk d = true) :
  have X := nset (BD.hidden hide d);
  have Y := nset (List.filter (fun y => !hide.contains y) d.outer);
  have ed := fun x => d.n + List.idxOf x (BD.hidden hide d);
  ∀ (hXY : X.Disjoint Y)
    (hinj :
      ∀ (x x' : Nat),
        X.mem x = true → X.mem x' = true → ed x = ed x' → x = x')
    (f : d.Fits Face.origin { width := d.width, names := X.union Y }),
    ∃ h' f',
      Big.closure d.width X Y ed hXY hinj ◦ ⟦d⟧.big ≃
        ⟦BD.close hide d⟧.big
    theorem closeBridge_faceOk {Ctrl : Type}
  (S : Sig Ctrl) (d : BD Ctrl)
  (hide : List Nat) (h : d.check S = true)
  (hf : BD.faceOk d = true) :
  have X := nset (BD.hidden hide d);
  have Y :=
    nset
      (List.filter
        (fun y => !hide.contains y)
        d.outer);
  have ed := fun x =>
    d.n + List.idxOf x (BD.hidden hide d);
  ∀ (hXY : X.Disjoint Y)
    (hinj :
      ∀ (x x' : Nat),
        X.mem x = true →
          X.mem x' = true →
            ed x = ed x' → x = x')
    (f :
      d.Fits Face.origin
        { width := d.width,
          names := X.union Y }),
    ∃ h' f',
      Big.closure d.width X Y ed hXY
          hinj ◦
        ⟦d⟧.big ≃ ⟦BD.close hide d⟧.big
    **B3 for descriptions whose faces are sets** (`BD.faceOk`): the bridge
for `BD.close` as ORIGINALLY stated, with `faceOk` in place of the
hypothesis of `CloseBridgeStatement'`.
  • theoremdefined in Logic/ComposeBridgeCor.lean
    complete
    theorem closeBridge_ground {Ctrl : Type} (S : Sig Ctrl) (d : BD Ctrl)
  (hide : List Nat) (h : d.check S = true) (hs : d.sites = [])
  (hi : d.inner = []) (hf : BD.faceOk d = true) :
  let X := nset (BD.hidden hide d);
  let Y := nset (List.filter (fun y => !hide.contains y) d.outer);
  let ed := fun x => d.n + List.idxOf x (BD.hidden hide d);
  ∃ h' f',
    Big.closure d.width X Y ed ⋯ ⋯ ◦ ⟦d⟧.big ≃ ⟦BD.close hide d⟧.big
    theorem closeBridge_ground {Ctrl : Type}
  (S : Sig Ctrl) (d : BD Ctrl)
  (hide : List Nat) (h : d.check S = true)
  (hs : d.sites = []) (hi : d.inner = [])
  (hf : BD.faceOk d = true) :
  let X := nset (BD.hidden hide d);
  let Y :=
    nset
      (List.filter
        (fun y => !hide.contains y)
        d.outer);
  let ed := fun x =>
    d.n + List.idxOf x (BD.hidden hide d);
  ∃ h' f',
    Big.closure d.width X Y ed ⋯ ⋯ ◦
      ⟦d⟧.big ≃ ⟦BD.close hide d⟧.big
    **B3′ for ground data whose faces are sets** (`BD.faceOk`): as
`closeBridge_ground_nodup`, for every `hide`.
  • theoremdefined in Logic/ComposeBridgeCor.lean
    complete
    theorem closeBridge_ground_nodup {Ctrl : Type} (S : Sig Ctrl) (d : BD Ctrl)
  (hide : List Nat) (h : d.check S = true) (hs : d.sites = [])
  (hi : d.inner = []) (hnd : (BD.hidden hide d).Nodup) :
  let X := nset (BD.hidden hide d);
  let Y := nset (List.filter (fun y => !hide.contains y) d.outer);
  let ed := fun x => d.n + List.idxOf x (BD.hidden hide d);
  ∃ h' f',
    Big.closure d.width X Y ed ⋯ ⋯ ◦ ⟦d⟧.big ≃ ⟦BD.close hide d⟧.big
    theorem closeBridge_ground_nodup {Ctrl : Type}
  (S : Sig Ctrl) (d : BD Ctrl)
  (hide : List Nat) (h : d.check S = true)
  (hs : d.sites = []) (hi : d.inner = [])
  (hnd : (BD.hidden hide d).Nodup) :
  let X := nset (BD.hidden hide d);
  let Y :=
    nset
      (List.filter
        (fun y => !hide.contains y)
        d.outer);
  let ed := fun x =>
    d.n + List.idxOf x (BD.hidden hide d);
  ∃ h' f',
    Big.closure d.width X Y ed ⋯ ⋯ ◦
      ⟦d⟧.big ≃ ⟦BD.close hide d⟧.big
    **B3′ for ground data, hidden names listed once**: for checked `d` with
no site and no inner name and `(BD.hidden hide d).Nodup`,
`⟦close hide d⟧ = (id_m ⊗ /X ⊗ id_Y) ∘ ⟦d⟧`, with `X` the hidden names,
`Y` the kept ones, and the edge of the `i`-th hidden name `d.n + i`.
  • theoremdefined in Logic/ComposeBridge.lean
    complete
    theorem hidden_disjoint {Ctrl : Type} (hide : List Nat) (d : BD Ctrl) :
  (nset (BD.hidden hide d)).Disjoint
    (nset (List.filter (fun y => !hide.contains y) d.outer))
    theorem hidden_disjoint {Ctrl : Type}
  (hide : List Nat) (d : BD Ctrl) :
  (nset (BD.hidden hide d)).Disjoint
    (nset
      (List.filter
        (fun y => !hide.contains y)
        d.outer))
    `hXY`: the hidden names and the kept names are disjoint.
  • theoremdefined in Logic/ComposeBridge.lean
    complete
    theorem hidden_inj {Ctrl : Type} (hide : List Nat) (d : BD Ctrl) (n x x' : Nat)
  (hx : (nset (BD.hidden hide d)).mem x = true)
  (hx' : (nset (BD.hidden hide d)).mem x' = true)
  (e :
    n + List.idxOf x (BD.hidden hide d) =
      n + List.idxOf x' (BD.hidden hide d)) :
  x = x'
    theorem hidden_inj {Ctrl : Type} (hide : List Nat)
  (d : BD Ctrl) (n x x' : Nat)
  (hx :
    (nset (BD.hidden hide d)).mem x =
      true)
  (hx' :
    (nset (BD.hidden hide d)).mem x' =
      true)
  (e :
    n + List.idxOf x (BD.hidden hide d) =
      n +
        List.idxOf x'
          (BD.hidden hide d)) :
  x = x'
    `hinj`: distinct hidden names get distinct edge numbers (whatever the
offset `n`, and whether or not a name is listed twice).
  • theoremdefined in Logic/ComposeBridge.lean
    complete
    theorem close_fits {Ctrl : Type} (hide : List Nat) (d : BD Ctrl)
  (hs : d.sites = []) (hi : d.inner = []) :
  d.Fits Face.origin
    { width := d.width,
      names :=
        (nset (BD.hidden hide d)).union
          (nset (List.filter (fun y => !hide.contains y) d.outer)) }
    theorem close_fits {Ctrl : Type} (hide : List Nat)
  (d : BD Ctrl) (hs : d.sites = [])
  (hi : d.inner = []) :
  d.Fits Face.origin
    { width := d.width,
      names :=
        (nset (BD.hidden hide d)).union
          (nset
            (List.filter
              (fun y => !hide.contains y)
              d.outer)) }
    `f`: ground data fits `ε → ⟨width, X ∪ Y⟩`, `X` the hidden names and `Y`
the kept ones.
  • theoremdefined in Logic/ComposeBridge.lean
    complete
    theorem closeBridge_refuted {Ctrl : Type} (S : Sig Ctrl) :
  ¬CloseBridgeStatement S
    theorem closeBridge_refuted {Ctrl : Type}
  (S : Sig Ctrl) : ¬CloseBridgeStatement S
    **B3 is REFUTED as stated.** Countermodel: `d = dupBD` (checked: `check`
does not look at repetitions in `outer`), `hide = [5]`. Then
`X = {5}`, `Y = ∅`, `ed 5 = 0`; the library's composite has the one
edge `0`; `BD.close [5] d` has the two edges `0` and `1`. They differ at
the edge test of `1`.
  • defdefined in Logic/ComposeBridge.lean
    complete
    def CloseBridgeStatement {Ctrl : Type} (S : Sig Ctrl) : Prop
    def CloseBridgeStatement {Ctrl : Type}
  (S : Sig Ctrl) : Prop
    **B3, closure** (REFUTED AS STATED, 2026-10-10: `closeBridge_refuted`;
`BD.check` does not ask that `d.outer` has no repetition, and
`BD.close` appends one edge for each ENTRY of `BD.hidden hide d`, so a
hidden name listed twice gives an edge that the library's composite
does not have. Restatement: `CloseBridgeStatement'`).
For checked ground data `d : ε → ⟨m, X ∪ Y⟩`
with `X` the names of `hide` that `d` has and `Y` its other outer names:
`⟦close hide d⟧ = (id_m ⊗ /X ⊗ id_Y) ∘ ⟦d⟧`, the closure's edge for the
`i`-th hidden name being `d.n + i` (the number `BD.close` gives it).
  • theoremdefined in Logic/ComposeBridgeCor.lean
    complete
    theorem closeBridge_a2 :
  ∃ h' f',
    Big.closure Inst.a2.width (nset (BD.hidden [0] Inst.a2))
        (nset (List.filter (fun y => ![0].contains y) Inst.a2.outer))
        (fun x => Inst.a2.n + List.idxOf x (BD.hidden [0] Inst.a2)) ⋯
        ⋯ ◦
      ⟦Inst.a2⟧.big ≃ ⟦BD.close [0] Inst.a2⟧.big
    theorem closeBridge_a2 :
  ∃ h' f',
    Big.closure Inst.a2.width
        (nset (BD.hidden [0] Inst.a2))
        (nset
          (List.filter
            (fun y => ![0].contains y)
            Inst.a2.outer))
        (fun x =>
          Inst.a2.n +
            List.idxOf x
              (BD.hidden [0] Inst.a2))
        ⋯ ⋯ ◦
      ⟦Inst.a2⟧.big ≃
      ⟦BD.close [0] Inst.a2⟧.big
    **B3′ fires**: `closeBridge'` at `a2`, `hide = [0]` (`X = {0}`,
`Y = {1}`, the closing edge `3 = a2.n`):
`⟦close [0] a2⟧ = (id₂ ⊗ /{0} ⊗ id_{1}) ∘ ⟦a2⟧`.
  • theoremdefined in Logic/ComposeBridgeCor.lean
    complete
    theorem closeBridge_ground_a2 :
  ∃ h' f',
    Big.closure Inst.a2.width (nset (BD.hidden [0] Inst.a2))
        (nset (List.filter (fun y => ![0].contains y) Inst.a2.outer))
        (fun x => Inst.a2.n + List.idxOf x (BD.hidden [0] Inst.a2)) ⋯
        ⋯ ◦
      ⟦Inst.a2⟧.big ≃ ⟦BD.close [0] Inst.a2⟧.big
    theorem closeBridge_ground_a2 :
  ∃ h' f',
    Big.closure Inst.a2.width
        (nset (BD.hidden [0] Inst.a2))
        (nset
          (List.filter
            (fun y => ![0].contains y)
            Inst.a2.outer))
        (fun x =>
          Inst.a2.n +
            List.idxOf x
              (BD.hidden [0] Inst.a2))
        ⋯ ⋯ ◦
      ⟦Inst.a2⟧.big ≃
      ⟦BD.close [0] Inst.a2⟧.big
    The same through the clean corollary: `a2` has `faceOk`.