Formalize Libkind–Spivak “Pattern Runs on Matter” (polynomial free/cofree constructions and module action)

[quangvdao]

Goal

Track a comprehensive formalization in PolyFun of Nelson Niu, David I. Spivak, and Sophie Libkind's “Pattern Runs on Matter: The Free Monad Monad as a Module Over the Cofree Comonad Comonad” (arXiv:2404.16321).

The target is the paper's polynomial/categorical result, not merely the fact that the existing type-level FreeM is a lawful monad and CofreeC is a lawful comonad. In the paper one constructs:

• the free substitution monoid 𝔪 p on a polynomial p;
• the cofree substitution comonoid 𝔠 q on a polynomial q;
• the action Ξ_{p,q} : 𝔪 p ⊗ 𝔠 q → 𝔪 (p ⊗ q);
• naturality and the unit/associativity laws making 𝔪 a left module over the lax monoidal functor 𝔠.

This is not a FreeM ⊣ CofreeC adjunction. The relevant adjunctions are separately the free-monoid and cofree-comonoid adjunctions over polynomials.

Repository snapshot

This assessment records the repository as it existed at:

• Time: 2026-07-12 18:58:55 +05:30
• Default branch: main
• Commit: 42fff61e197cce4a634bfb5e416be7b8edb154e9
• Commit subject: feat(pfunctor): Spivak–Niu monoidal & lens algebra (⊗-hom, factorization, cartesian closure, machines) (#15)

All statements below about what PolyFun “currently” contains refer to this snapshot. Future contributors should compare the then-current branch and PR graph against this commit and update the checklist rather than assuming the inventory remains current.

At posting time there were eleven open PRs, forming this stack:

main
└─ #16 PointedMachine fuel semantics / Handler
   └─ #17 fuel-exact seqComp
      └─ #18 seqComp notation
         └─ #19 DynSystem-as-lens refactor
            └─ #20 game wiring
               └─ #21 FreeM.mapM universal property
                  └─ #22 seqComp_State simp lemma
                     └─ #23 citation and FreeM/Cofree documentation corrections
                        └─ #24 simulation/naming cleanup
                           └─ #25 tests and documentation
                              └─ #27 bisimulation and UC bridge

Relevant links: #16, #17, #18, #19, #20, #21, #22, #23, #24, #25, #27.

What exists at the snapshot

PolyFun already has much of the computational substrate:

Free side

• PFunctor/Free/Basic.lean defines type-level FreeM P α, its monad structure, maps along lenses, and handlers.
• PFunctor/Free/Path.lean defines root-to-leaf paths, tree grafting, path append/split, and inverse laws.
• #21 proposes uniqueness and naturality results for FreeM.mapM/mapMHom. This is a useful type-level shadow of the free universal property.

The path/grafting API is close to the hard fiberwise data needed to bundle the paper's polynomial 𝔪 p, but that bundled polynomial, its substitution-monoid structure, and its categorical universal property are not yet present.

Cofree side

• PFunctor/Cofree.lean defines the standard type-level CofreeC and its lawful comonad structure.
• PFunctor/M.lean supplies terminal-coalgebra corecursion, uniqueness, and bisimulation.
• PFunctor/Dynamical/Trajectory.lean defines behavior/trajectory semantics and a uniqueness theorem.
• PFunctor/Comonoid.lean defines concrete substitution-comonoid data and laws.

The missing low-level ingredient is a general finite-vertex/rooted-path calculus for M p. The paper's polynomial 𝔠 p has behavior trees as positions and finite vertices of each tree as directions. PolyFun has the positions but not this dependent direction family.

Tensor/duoidal side

• PFunctor/InternalHom.lean supplies the tensor internal hom, evaluation, and curry/uncurry.
• PFunctor/Lens/Duoidal.lean supplies ordering/interchange maps.
• Full duoidal coherence is not yet proved or packaged.
• There is no generic substitution-monoid object/homomorphism category, no substitution-comonoid homomorphism category, and no implementation of the paper's two adjunctions or Ξ.

In short: the repository is substrate-rich but paper-theorem-incomplete.

Proposed formalization

1. Polynomial free monoid

Define a bundled polynomial along the lines of

FreeP p :=
  PFunctor.mk
    (FreeM p PUnit) -- positions: finite p-trees
    FreeM.Path      -- directions: dangling leaves

and prove an extension equivalence

(FreeP p).Obj X ≃ FreeM p X

Then provide:

• unit lens;
• substitution/multiplication lens using tree grafting;
• direction maps using Path.append/Path.split;
• monoid laws;
• functoriality on polynomial morphisms;
• substitution-monoid homomorphisms;
• free universal property and adjunction 𝔪₋ ⊣ U;
• compatibility with the type-level universal property from feat(pfunctor): FreeM.mapM universal property & naturality along a monad morphism (B6) #21.

2. Finite vertices of M-types

Develop a reusable dependent finite-path API for behavior trees:

• M.Vertex or M.Path;
• root vertex;
• child extension;
• following a path;
• subtree rooted at a vertex;
• path concatenation;
• splitting and inverse laws;
• mapping/transport along polynomial morphisms;
• simp and extensionality API suitable for later proofs.

This infrastructure should be designed for reuse in transcripts, finite observations, query paths, reachable sub-behaviors, and categorical/comonoid constructions.

3. Polynomial cofree comonoid

Define

CofreeP p :=
  PFunctor.mk
    (M p)       -- positions: p-behavior trees
    M.Vertex    -- directions: finite rooted vertices

and prove the expected extension equivalence

(CofreeP p).Obj X ≃ CofreeC p X

Then provide:

• counit selecting the root;
• comultiplication via rooted subtrees and path concatenation;
• comonoid laws;
• functoriality;
• substitution-comonoid homomorphisms and their category;
• cofree universal property and adjunction U ⊣ 𝔠₋;
• theorem identifying DynSystem.behavior with the adjunction mate;
• compatibility with existing trajectory and behavior uniqueness results.

4. Lax monoidality and duoidal coherence

• finish/package the required duoidal naturality and coherence laws;
• define y → CofreeP y;
• define CofreeP p ⊗ CofreeP q → CofreeP (p ⊗ q);
• prove lax-monoidal unit, associativity, and naturality;
• decide how much should initially be concrete “à-la-carte” structure versus Mathlib's generic MonoidalCategory/Mon_/Comon_ hierarchy.

A practical approach is to validate concrete structures and homomorphisms first, then bridge them to the generic categorical hierarchy after the universe and coherence APIs stabilize.

5. Pattern runs on matter

Construct

Ξ_{p,q} : FreeP p ⊗ CofreeP q ⟶ FreeP (p ⊗ q)

using internal hom, duoidality, and the free universal property. Prove:

• naturality in p;
• naturality in q;
• module unit law;
• module associativity law;
• compatibility with free-tree grafting/substitution;
• operational characterization;
• compatibility with game wiring, handlers, and PointedMachine.runWith;
• behavior/bisimulation compatibility;
• at least representative executable examples from the paper.

The operational theorems should explain/generalize existing machinery rather than duplicate it. In particular, #20's one-step game wiring and Ξ's whole finite-pattern semantics should be related by explicit compatibility theorems.

Scope and completeness

Primary milestone: theorem-complete, Lean-native construction

The initial goal should prove the paper's principal objects and theorems using PolyFun's existing inductive/coinductive W/M-type infrastructure:

• bundled polynomial FreeP and CofreeP;
• their substitution monoid/comonoid structures;
• both universal properties/adjunctions;
• lax monoidality of CofreeP;
• Ξ, naturality, and module coherence;
• representative applications and operational bridges.

This can be mathematically theorem-complete even though the proof presentation differs from the paper.

Optional later milestone: literal transfinite reconstruction

The paper presents the free construction through ordinal stages, κ-small polynomials, filtered colimits, and distribution of substitution over those colimits. Reproducing this proof method would require a separate substantial development:

• cardinal bounds on polynomial fibers;
• transfinite chains/stages;
• relevant colimits of polynomials;
• filtered-colimit/substitution distribution;
• independence of the chosen regular cardinal;
• comparison theorem with the direct FreeP construction.

This is valuable category-theoretic work but should not block the primary milestone or its VCV/game-semantics applications.

Universe considerations

The direct position type FreeM p PUnit naturally lives in a maximum of the position and direction universes. The simplest first theorem-complete development may therefore restrict to PFunctor.{u,u}.

Before cementing the public API, decide whether to:

• initially support a shared universe and generalize later; or
• incorporate ULift/resizing from the start.

The tensor internal-hom code also has shared-universe limitations, so the universe policy should be resolved coherently rather than independently in each construction.

Relationship to the open PR stack

At the snapshot above:

• feat(pfunctor): FreeM.mapM universal property & naturality along a monad morphism (B6) #21 is a direct precursor and should preferably be extracted/retargeted to merge earlier rather than remaining behind refactor(pfunctor): DynSystem is an abbrev of lenses from the self monomial #19/feat(dynamical): game wiring — responders, eval-games, Kleisli runs #20.
• docs: fix Spivak–Niu citations, honest FreeM/Cofree wording, DAG sync #23 contains an important documentation correction and should merge independently of this larger project.
• The foundational FreeP, M.Vertex, and CofreeP work is mostly orthogonal to refactor(pfunctor): query-exact PointedMachine fuel semantics; promote Handler #16–Standard LTS bisimulation and activation-delay coherence #27 and should not be placed behind the entire stack.
• The DynSystem.behavior mate theorem should account for the representation change in refactor(pfunctor): DynSystem is an abbrev of lenses from the self monomial #19.
• Operational compatibility with games/runWith should be developed against feat(dynamical): game wiring — responders, eval-games, Kleisli runs #20 and feat(pfunctor): FreeM.mapM universal property & naturality along a monad morphism (B6) #21.
• feat(pfunctor): fuel-exact seqComp run law (ResolvesIn, runWith_seqComp) #17's operational sequential composition should be related to, but not conflated with, the paper's module action.
• Standard LTS bisimulation and activation-delay coherence #27 is not a prerequisite, but its bisimulation API should later prove that Ξ-induced execution respects behavioral/observational equivalence.

Suggested PR decomposition

1. FreeP and the extension equivalence with FreeM.
2. Free substitution monoid and universal property, incorporating/depending on feat(pfunctor): FreeM.mapM universal property & naturality along a monad morphism (B6) #21.
3. M.Vertex finite-path calculus.
4. CofreeP, its comonoid, and the extension equivalence with CofreeC.
5. Cofree universal property and the DynSystem.behavior mate.
6. Remaining duoidal coherence and lax monoidality of CofreeP.
7. Ξ, naturality, and module laws.
8. Operational bridges, examples, and VCV/game/bisimulation consequences.
9. Optional transfinite/κ-small reconstruction in a separate stack.

Reusable payoff

This project should leave behind general infrastructure rather than a theorem narrowly specialized to one paper:

• finite vertices/paths through terminal-coalgebra behavior trees;
• generic handler/interpreter fusion from the free universal property;
• canonical behavior semantics from the cofree universal property;
• categories of substitution monoids and comonoids;
• reusable duoidal coherence;
• denotational semantics for running finite interaction patterns against behaviors;
• laws for sequential/parallel protocol and game composition;
• foundations for later polynomial bicomodule/prafunctor work and UC composition.

Definition of done for the primary milestone

• The paper's 𝔪 p, 𝔠 p, and Ξ have bundled PolyFun definitions.
• Their extensions are related to the existing FreeM and CofreeC APIs by explicit equivalences.
• Both free/cofree universal properties are stated at the polynomial level and proved.
• Naturality, lax-monoidal coherence, and module unit/associativity are proved.
• The development has a documented universe policy.
• Existing game/dynamical-system semantics are connected by compatibility theorems.
• At least one nontrivial worked example executes and is covered by tests.
• Documentation clearly distinguishes type-level free/cofree structures from the polynomial categorical constructions.