The Baby Bear field as a first-class transfer domain (stack fusion)

The other Param-engine domains are small: the diagonal Eq and the Num ↦ ℕ change-of-representation (Transfer.Param.instTransferDomNumNat). This module promotes a crypto carrier — the computational Baby Bear field operations (bbFieldMul/bbFieldAdd, proved equal to the abstract */+ via bbFieldMul_eq/bbFieldAdd_eq) — into first-class transfer data, and fuses the two transfer stacks over the same field:

• Stack B (Related). Related.lean registers the field ops as RelatedBinOp instances (bbMulRelated/bbAddRelated) and composes a transfer of a closed op-tree by instance resolution (composeBinOp), extracted by transferRel/.rel. Driven by rcongr/param_solve.
• Stack A (Param). ParamDB resolves @[param]-registered RArrow PA PB c c' witnesses for the term-level translation ⟦·⟧ (#transfer/translateAll); Transfer.Param.TransferDom resolves the domain for the ∀-rule (param_transfer/forallTransferAuto).

Without this file these two stacks share a field but not a registry: the Baby Bear ops live only in Stack B. This file registers the same operations into Stack A as @[param] RArrow witnesses and adds a Baby Bear TransferDom, so a single field operation is usable by both engines.

What is registered

1. @[param] field witnesses (Stack A). bbMulParam/bbAddParam prove RArrow Eq (RArrow Eq Eq) (· * ·) bbFieldMul (resp. +/bbFieldAdd) from bbFieldMul_eq/bbFieldAdd_eq. @[param] keys them under the abstract operator heads (HMul.hMul/HAdd.hAdd), so getParamDB/translateAll resolve the field ops by the same witness that proves Stack B's square.
2. A Baby Bear TransferDom. instTransferDomBabyBear : TransferDom F F so param_transfer transfers ∀ (x : F), P x-style statements over the field. It is the diagonal domain (graph Eq on F) — see the non-diagonal case below for why a field↔limb domain needs more than the TransferDom shape expresses.

The non-diagonal case

TransferDom A A' carries a Param .map0 .map2a A A': a backward section A' → A with map_in_R. The Baby Bear representation change is F ↔ BitVec-style limbs through bbEncode/bbToF; a non-diagonal TransferDom F BitVec-style domain would need that backward decoder packaged at map2a (it exists — bbToF_bbEncode is the round-trip), but the ∀-rule then delivers a pointwise obligation phrased against the limb predicate P', which the caller must supply by hand. Inferring that limb predicate requires the annotation inference described in the ParamTransferTac module docstring (the full ⟦t⟧ over arbitrary terms with per-subterm levels). This file therefore registers the diagonal field domain (complete for same-representation field transfer) and the op-level representation change lives in the @[param]/RelatedBinOp op witnesses, which carry the F ↔ bbField* change.

Stack-A registration: the field ops as @[param] RArrow witnesses

These are the same field realizations that Stack B carries as RelatedBinOp (bbMulRelated/bbAddRelated). Rather than a second proof, the Stack-A RArrow witnesses are derived from those squares by the single source of truth paramWitnessOfRelatedBinOp (Integrations/ParamRelatedBridge.lean): register the RelatedBinOp once, and the @[param] witness is a one-liner citing it — the bbFieldMul_eq/bbFieldAdd_eq proof lives in exactly one place.

theorem Transfer.bbMulParam : Param.RArrow Eq (Param.RArrow Eq Eq) HMul.hMul ExampleField.bbFieldMul

Baby Bear multiply, Stack-A witness. RArrow Eq (RArrow Eq Eq) is the curried function relation for a binary op: on Eq-related arguments the abstract * and the emitted bbFieldMul agree. Registered with @[param] (keyed under HMul.hMul). Derived from the RelatedBinOp square bbMulRelated — one registration, both engines.

theorem Transfer.bbAddParam : Param.RArrow Eq (Param.RArrow Eq Eq) HAdd.hAdd ExampleField.bbFieldAdd

Baby Bear add, Stack-A witness. As bbMulParam, for +/bbFieldAdd, keyed under HAdd.hAdd. Derived from the RelatedBinOp square bbAddRelated.

Stack-A domain: the Baby Bear field as a TransferDom

A TransferDom F F (the diagonal field domain) so param_transfer / forallTransferAuto transfer ∀ (x : F), P x-style statements over the field with the domain Param resolved by instance — the field plays the role Num played, but as a crypto carrier.

@[instance_reducible]

instance Transfer.instTransferDomBabyBear : Param.TransferDom ExampleField.F ExampleField.F

Baby Bear TransferDom. Resolves the domain Param .map0 .map2a F F (the diagonal, graph Eq on the field) for param_transfer. Definitionally paramDiag, so the pointwise obligation on related pairs (x, x') is x = x'. This is the same-representation field domain; the op-level representation change is carried by bbMulParam/bbAddParam and the RelatedBinOp squares.

Equations

• Transfer.instTransferDomBabyBear = { dom := Transfer.Param.paramDiag }

Doc-tests: both stacks close Baby Bear field goals

These pinned examples back the README's prose snippets. They exercise, on the same field operations: Stack B (Related/transferRel), Stack A @[param] witnesses, and the param_transfer ∀-rule over the field TransferDom.

Next domains (documented)

Two further representations in the repo would slot in as additional @[param]/TransferDom registrations, both diagonal-only under the current TransferDom shape (the same non-diagonal limitation as above):

• ZMod p ↔ canonical-Natlimbs.bbEncode/bbToFalready give the `F ↔ BitVecround-trip; aTransferDom F BitVec-style domain needs the decoder at map2a(have it:bbToF_bbEncode`) and the caller-supplied limb predicate — blocked on the annotation-inference gap, not on a missing primitive.
• group ↔ bytes. Any ReprEmbeddingClass A α is already a Param .map3 .map0 (Param.paramOfEmbedding); registering it as a TransferDom needs a backward section, which an embedding lacks by construction (it is map0 backward) — so this stays a forward-only op witness, not a ∀-domain, until a decoder is registered.

No new primitives are introduced here: only the already-proven Baby Bear field realizations are registered.

Pinned fusion doc-test: the field ops live in the Param-engine registry

This #guard_msgs-checked probe materialises the ambient @[param] registry (getParamDB, the database the term-level translator translate/translateAll consumes) and confirms the abstract field operators HMul.hMul/HAdd.hAdd resolve to the emitted Baby Bear kernels via the same witnesses that back Stack B's RelatedBinOp squares — i.e. the two stacks share one registry.