Tier-3: compositional transfer via the abstraction theorem

The per-op BinOpRealization (Bridges/ReprTransfer.lean) transfers a single operation's equation. Real verifier equations are composite — e.g. Groth16's pairing product e(αG1,βG2)·e(L,γG2)·e(C,δG2) is two GT products over three pairings. A parametricity/relational-model translation automates the transfer of each composite.

This module is the internalized relational-model core for a homogeneous operation fragment: an expression algebra over one binary operation, with an abstract and a computational denotation tied by the abstraction theorem (denote_commutes — by induction, the single-op commuting square lifts to whole terms), from which composite equation transfer (expr_eq_transfer) follows. This is the payload a paramcoq/Trocq translation produces; here it is a finite, fully-proved Lean construction for the op-algebra fragment the emit-realization bridges use. A native Expr-level translation that generates this for arbitrary terms (rather than the fixed op-algebra here) is the greenfield "Lean Trocq" — this module is the semantic kernel it targets.

Main definitions

• EndoOpRealization op bop — a homogeneous binary op op : A → A → A realized by bop : α → α → α via an equality-reflecting encoding.
• OpExpr — the expression algebra (leaves + binary nodes).
• OpExpr.denote_commutes — the abstraction theorem.
• OpExpr.expr_eq_transfer — composite equation transfer.

structure ReprTransfer.EndoOpRealization {A α : Type u} (op : A → A → A) (bop : α → α → α) : Type u

A homogeneous binary-op realization: op : A → A → A realized by bop : α → α → α via an equality-reflecting encoding enc. The homogeneous (single-carrier) specialization of BinOpRealization, on which the expression algebra below is built.

• enc : A → α

  The equality-reflecting encoding of abstract values.

• enc_inj : Function.Injective self.enc

  The encoding reflects equality.

• commutes (a b : A) : self.enc (op a b) = bop (self.enc a) (self.enc b)

  The single-op commuting square.

def ReprTransfer.EndoOpRealization.toReprEmbedding {A α : Type u} {op : A → A → A} {bop : α → α → α} (R : EndoOpRealization op bop) : ReprEmbedding A α

The codomain embedding underlying an EndoOpRealization.

Equations

• R.toReprEmbedding = { enc := R.enc, enc_inj := ⋯ }

The operation expression algebra

inductive ReprTransfer.OpExpr (A : Type u) : Type u

Expressions over a single binary operation: abstract leaves and binary nodes. The shape of a pairing-product / field-arithmetic tree.

• leaf {A : Type u} : A → OpExpr A

  An abstract leaf value (e.g. a single pairing output e(P,Q) : GT).

• node {A : Type u} : OpExpr A → OpExpr A → OpExpr A

  A binary node (e.g. a GT product a · b).

def ReprTransfer.OpExpr.denoteAbs {A : Type u} (op : A → A → A) : OpExpr A → A

Abstract denotation: fold the tree with the abstract operation.

Equations

• ReprTransfer.OpExpr.denoteAbs op (ReprTransfer.OpExpr.leaf a) = a
• ReprTransfer.OpExpr.denoteAbs op (l.node r) = op (ReprTransfer.OpExpr.denoteAbs op l) (ReprTransfer.OpExpr.denoteAbs op r)

def ReprTransfer.OpExpr.denoteComp {A α : Type u} {op : A → A → A} {bop : α → α → α} (R : EndoOpRealization op bop) : OpExpr A → α

Computational denotation: encode the leaves and fold with the computational operation bop.

Equations

• ReprTransfer.OpExpr.denoteComp R (ReprTransfer.OpExpr.leaf a) = R.enc a
• ReprTransfer.OpExpr.denoteComp R (l.node r) = bop (ReprTransfer.OpExpr.denoteComp R l) (ReprTransfer.OpExpr.denoteComp R r)

theorem ReprTransfer.OpExpr.denote_commutes {A α : Type u} {op : A → A → A} {bop : α → α → α} (R : EndoOpRealization op bop) (e : OpExpr A) : R.enc (denoteAbs op e) = denoteComp R e

The abstraction theorem. For any composite expression, encoding its abstract value equals its computational denotation. Proved by induction: the single-op commuting square lifts to whole terms. This is the relational-model payload — the reason the transfer composes.

theorem ReprTransfer.OpExpr.expr_eq_transfer {A α : Type u} {op : A → A → A} {bop : α → α → α} (R : EndoOpRealization op bop) (e₁ e₂ : OpExpr A) : denoteAbs op e₁ = denoteAbs op e₂ ↔ denoteComp R e₁ = denoteComp R e₂

Composite equation transfer. An equation between two abstract composite expressions holds iff their computational denotations agree. The whole (multi-op) verifier equation transfers from the single-op realization R.

Two-sorted: a whole pairing-product verifier tree

The homogeneous OpExpr handles a single op. A pairing-product verifier (Groth16 LHS) mixes two operations of different sorts: the pairing e : A → B → C (heterogeneous) and the C-product mul (homogeneous). PExpr is the two-sorted tree — pairing leaves and product nodes — so the entire verifier LHS is one term, and PExpr.expr_eq_transfer transfers the whole verifier equation from a single abstraction theorem. Here the pairings are nodes of the same tree the transfer ranges over, rather than opaque leaf-values supplied by hand.

structure ReprTransfer.PairingRealization {A B C α β γ : Type u} (e : A → B → C) (mul : C → C → C) (bpair : α → β → γ) (bmul : γ → γ → γ) : Type u

A bilinear-operation realization: an abstract pairing e : A → B → C and an abstract C-product mul, realized by computational bpair/bmul via domain maps encA/encB, a C-embedding encC, and two commuting squares. The data a whole pairing-product verifier tree needs (the KZG ByteGroupRealization is an instance).

• encA : A → α

  Encoding of A (first pairing operand).

• encB : B → β

  Encoding of B (second pairing operand).

• encC : C → γ

  Equality-reflecting encoding of C (the target group).

• encC_inj : Function.Injective self.encC

  C-equality reflection.

• pair_commutes (a : A) (b : B) : self.encC (e a b) = bpair (self.encA a) (self.encB b)

  The pairing commuting square.

• mul_commutes (x y : C) : self.encC (mul x y) = bmul (self.encC x) (self.encC y)

  The C-product commuting square.

inductive ReprTransfer.PExpr (A B : Type u) : Type u

A two-sorted pairing-product expression: pairing leaves e(a,b) and product nodes. One PExpr captures a whole pairing-product verifier LHS.

• pair {A B : Type u} : A → B → PExpr A B

  A pairing leaf e(a, b).

• node {A B : Type u} : PExpr A B → PExpr A B → PExpr A B

  A product node combining two sub-expressions.

def ReprTransfer.PExpr.denoteAbs {A B C : Type u} (e : A → B → C) (mul : C → C → C) : PExpr A B → C

Abstract denotation of a pairing-product tree (pairings via e, nodes via mul).

Equations

• ReprTransfer.PExpr.denoteAbs e mul (ReprTransfer.PExpr.pair a b) = e a b
• ReprTransfer.PExpr.denoteAbs e mul (l.node r) = mul (ReprTransfer.PExpr.denoteAbs e mul l) (ReprTransfer.PExpr.denoteAbs e mul r)

def ReprTransfer.PExpr.denoteComp {A B C α β γ : Type u} {e : A → B → C} {mul : C → C → C} {bpair : α → β → γ} {bmul : γ → γ → γ} (R : PairingRealization e mul bpair bmul) : PExpr A B → γ

Computational denotation: pairing leaves via bpair on encoded operands, nodes via bmul.

Equations

• ReprTransfer.PExpr.denoteComp R (ReprTransfer.PExpr.pair a b) = bpair (R.encA a) (R.encB b)
• ReprTransfer.PExpr.denoteComp R (l.node r) = bmul (ReprTransfer.PExpr.denoteComp R l) (ReprTransfer.PExpr.denoteComp R r)

theorem ReprTransfer.PExpr.denote_commutes {A B C α β γ : Type u} {e : A → B → C} {mul : C → C → C} {bpair : α → β → γ} {bmul : γ → γ → γ} (R : PairingRealization e mul bpair bmul) (x : PExpr A B) : R.encC (denoteAbs e mul x) = denoteComp R x

Abstraction theorem (two-sorted). Encoding the abstract value of a whole pairing-product tree equals its computational denotation — by induction, both commuting squares lifting through the tree.

theorem ReprTransfer.PExpr.expr_eq_transfer {A B C α β γ : Type u} {e : A → B → C} {mul : C → C → C} {bpair : α → β → γ} {bmul : γ → γ → γ} (R : PairingRealization e mul bpair bmul) (x y : PExpr A B) : denoteAbs e mul x = denoteAbs e mul y ↔ denoteComp R x = denoteComp R y

Whole-verifier equation transfer. An equation between two abstract pairing-product trees holds iff their computational denotations agree — the entire pairing-product verifier equation, transferred from the per-op commuting squares with no bespoke composite proof.