Transpose Duality

A structural symmetry of the 4QX square: the pair‑of‑teloi view (2×3) and the triple‑of‑edges view (3×2) are the same object seen from opposite sides, related by an involutive transpose.

Formal setting

Vertices: Vtx={TL,TR,BL,BR}Vtx=\{TL,TR,BL,BR\}.
Edges: unordered pairs of vertices; write s:=ETL ⁣− ⁣TR,ℓL:=ETL ⁣− ⁣BL,ℓR:=ETR ⁣− ⁣BR.s:=E_{TL\!-\!TR},\quad \ell_L:=E_{TL\!-\!BL},\quad \ell_R:=E_{TR\!-\!BR}.
Policies (4QX constraints):
- (P1) Seam‑only coupling: teloi may share only ss.
- (P2) No back‑channel: bottom edge EBL ⁣− ⁣BRE_{BL\!-\!BR} is forbidden.
- (P3) Locality: a left‑apex telos’s private leg ends in BLBL; a right‑apex telos’s private leg ends in BRBR (diagonals excluded).

Data

Telos (the “3”): a triple (apex, s, ℓ)(\text{apex},\, s,\, \ell) with ℓ\ell a private leg incident to the apex.
(The apex is derivable from s∩ℓs\cap\ell, so extensionally a telos ≅\cong a dual‑edge {s,ℓ}\{s,\ell\}.)
Pair of teloi (the “2”): two teloi (TL,s,ℓL)(TL,s,\ell_L) and (TR,s,ℓR)(TR,s,\ell_R) satisfying (P1–P3).
Incidence matrix (telos‑centric, 2×3):

M = sℓLℓRTL110TR101M \;=\; \begin{array}{c|ccc} & s & \ell_L & \ell_R\\\hline T_L & 1 & 1 & 0\\ T_R & 1 & 0 & 1 \end{array}

Transpose (edge‑centric, 3×2):

M⊤ = TLTRs11ℓL10ℓR01M^\top \;=\; \begin{array}{c|cc} & T_L & T_R\\\hline s & 1 & 1\\ \ell_L& 1 & 0\\ \ell_R& 0 & 1 \end{array}

Definition (Transpose Duality).
Transpose duality is the equivalence T:(2×3)⇄(3×2)\mathcal{T} : (2\times 3)\rightleftarrows (3\times 2) given by M↦M⊤M \mapsto M^\top. It swaps the telos‑centric and edge‑centric factorizations while preserving all 4QX policies and derived structure. The map is an involution: T(T(M))=M\mathcal{T}(\mathcal{T}(M))=M.

Classification / “Inevitability”

Under (P1–P3), there is (up to left–right symmetry) exactly one admissible incidence pattern: { s, ℓL, ℓR }.\{\,s,\ \ell_L,\ \ell_R\,\}.

All other 3‑edge choices violate a policy:

include EBL ⁣− ⁣BRE_{BL\!-\!BR} ⇒ violates (P2);
include a diagonal ⇒ violates (P3);
share more than ss ⇒ violates (P1).

This uniqueness is the precise sense in which 2×3 and 3×2 “can co‑exist only one way.”

Derived structure and invariants

Vertices generated: endpoints of {s,ℓL,ℓR}\{s,\ell_L,\ell_R\} are exactly {TL,TR,BL,BR}\{TL,TR,BL,BR\}.
Forbidden edge absent: EBL ⁣− ⁣BR∉{s,ℓL,ℓR}E_{BL\!-\!BR}\notin\{s,\ell_L,\ell_R\} by construction.
Apex determinacy: TL=s∩ℓL, TR=s∩ℓRTL=s\cap\ell_L,\ TR=s\cap\ell_R. A telos’s “third” component is derived data.
Uniqueness up to symmetry: swapping left/right conjugates MM by column/row swap and preserves policies.

Why it matters

Normal form: proofs can toggle between rows (teloi) and columns (edges) without changing the object.
Safety by generators: seam‑only coupling and no BL–BR channel are enforced at the generator level, not as after‑the‑fact constraints.
Process grammar fit: the backbone “two teloi × three roles” (or “three edges × two teloi”) underlies the six canonical actions [\Pow,\Sep,\Pair,\Un,\Emp,\Repl][\Pow,\Sep,\Pair,\Un,\Emp,\Repl].
Compositionality: replacement‑naturality (paths compose up to ≈\approx) is indifferent to the side chosen; transpose duality keeps the calculus symmetric.

Minimal formalization (set‑theoretic)

Let Telos:={(TL,s,ℓL),(TR,s,ℓR)}Telos := \{(TL,s,\ell_L), (TR,s,\ell_R)\}.
Define Edges(Telos):={s,ℓL,ℓR},Teloi(Edges):={(s∩ℓL, s, ℓL), (s∩ℓR, s, ℓR)}.Edges(Telos) := \{s,\ell_L,\ell_R\},\qquad Teloi(Edges) := \big\{(s\cap \ell_L,\ s,\ \ell_L),\ (s\cap \ell_R,\ s,\ \ell_R)\big\}.

Then, under (P1–P3): Teloi(Edges(Telos))=Telos,Edges(Teloi(Edges))=Edges.Teloi(Edges(Telos)) = Telos,\qquad Edges(Teloi(Edges)) = Edges.

This pair of maps is the object‑level form of M↦M⊤M \mapsto M^\top.

Lean sketch (names match your HF layer)

/-- Edges in the admissible 3-edge skeleton. -/
inductive EdgeRole | seam | leftVert | rightVert

structure Telos :=
  (apex : Vertex)         -- TL or TR
  (seam : Edge)           -- E_TLTR
  (leg  : Edge)           -- E_TLBL or E_TRBR
  (policies : satisfies_P1_P3 apex seam leg)

structure PairOfTeloi := (left right : Telos) (share_only_seam : ...) (disjoint_legs : ...)

def edgesOf (P : PairOfTeloi) : Finset EdgeRole := {seam, leftVert, rightVert}

def teloiOf (E : Finset EdgeRole) (ok : E = {seam,leftVert,rightVert}) : PairOfTeloi := ...

theorem transpose_duality_involutive :
  teloiOf (edgesOf P) = P ∧ edgesOf (teloiOf E ok) = E := ...

(The proof is by case analysis on allowed legs under (P1–P3).)

Edge cases & variants

Relaxed locality (drop P3): a second admissible skeleton appears: {s,ETL ⁣− ⁣BR,ETR ⁣− ⁣BL}\{s, E_{TL\!-\!BR}, E_{TR\!-\!BL}\}. Transpose duality still holds, but safety properties change (cross‑silo reach).
Add bottom edge: violates (P2); transpose duality becomes trivial but no longer enforces seam‑only coupling.

Do / Don’t

Do use the transpose to switch perspectives when a proof or diagram is simpler in telos‑centric vs edge‑centric form.
Don’t treat the apex as independent data in algebraic manipulations; it is determined by ss and the leg.