feat(realizability): generalize and pre-upstream the VCVio polytime machine layer

[dtumad]

Adds a generic notion of "this FreeM program can be run by a state machine whose
transition functions satisfy a given predicate", and upstreams the machine-side
helpers that VCVio#500 currently
carries locally with -- upstream candidate for DynComputation comments.

Qualitative only: it constrains which machines are allowed, not how much they cost.

---

Commit 1 — additions to the existing dynamical layer

PolyFun/PFunctor/Dynamical/DynComputation.lean

• ofStep (stepFn : S → β ⊕ p.Obj S) (init : α → S) — @[reducible], with
  ofStep_State, ofStep_init, view_ofStep.
• setInit (M) (g : γ → M.State) — @[reducible], with setInit_State,
  setInit_init, setInit_view, setInit_denote, contramapInput_eq_setInit.

PolyFun/PFunctor/Dynamical/DynComputation/Bounded.lean

• unroll_setInit, unroll_mapResult, unroll_wrap and run_setInit,
  run_mapResult, run_wrap.

PolyFun/PFunctor/Bound.lean

• isTotalRollBound_mapLens.

All additions; no existing declaration changes behaviour. Builds standalone.

---

Commit 2 — new PolyFun/Realizability/ subtree

Entered in the DAG after the ITree block. Nothing under PFunctor/, ITree/ or
Interaction/ depends on it.

File	Contents
StepClass.lean	StepClass; HasProd / HasSum / HasOption / IsDistributive mixins; Distributive bundle; derived combinators; Refines
Machine.lean	head, update?, updateFlat, output, expose, stepD; transport lemmas; seqComp step lemmas; ofStep_step_eq_of_flat_eq
Basic.lean	Boundary (+ withInput, withOut, withInterface, mid, Composable, mapRefines), Realization, IsRealizableBy, IsRealizableWithin
Closure.lean	the closure theorems; Lens.pullHeadIdx, Lens.IsAdmissible
Instances.lean	unconstrained, finite, computable, WordClass

The class of admissible functions

structure PFunctor.StepClass where
  Str : Type u → Type v                                    -- how a type is represented
  Hom : {A B : Type u} → Str A → Str B → (A → B) → Prop    -- which functions are allowed
  id_mem   : ∀ {A} (a : Str A), Hom a a id
  comp_mem : Hom a b f → Hom b d g → Hom a d (g ∘ f)

Str is data, not a proposition: a resource bound only makes sense relative to a
chosen representation. Mixins are separate so each theorem asks for exactly what
it consumes — HasProd, HasSum, HasOption for the core definition,
IsDistributive for seqComp only.

Derived in StepClass.lean: Hom.congr, HasProd.{map_mem, pairRight_mem, pairLeft_mem, diag_mem, withInput_mem, swap_mem, assoc_mem}, HasSum.map_mem,
codistrib_mem, IsDistributive.elimCtx_mem.

The first-order step maps

DynComputation's dynamics live in view : State → β ⊕ p.Obj State, whose second
component is function-valued and dependent — neither shape can be constrained by a
predicate on plain functions. Machine.lean re-presents them as:

def head   (M : DynComputation p α β) : M.State → β ⊕ p.A := M.toDynSystem.expose
def update? [DecidableEq p.A] (M) : M.State × p.Idx → Option M.State
def updateFlat [DecidableEq p.A] (M) (step) : M.State := (M.update? step).getD step.1

head is definitionally the position map of the machine's underlying lens, so
setInit, mapResult and wrap transport it by rfl. updateFlat, output,
expose, stepD are the derived accessors a machine-facing cost model consumes.
ofStep_step_eq_of_flat_eq: a step function is determined by the head and
update? it induces, so these are a presentation rather than a projection.

The predicate

def IsRealizableBy (C) [C.HasProd] [C.HasSum] [C.HasOption] [DecidableEq p.A]
    (bd : Boundary C p α β) (program : α → FreeM p β) : Prop :=
  ∃ R : Realization C bd, R.machine.Implements program

def IsRealizableWithin (C) … (program) (k : ℕ) : Prop :=
  ∃ R : Realization C bd, R.machine.ImplementsWithin program k

A Realization bundles a machine, a representation of its hidden state, and
admissibility of init, head, update?. Constraining init is what forbids
smuggling precomputed advice into the initial state.

Boundary collects the representations at the boundary and is always a
parameter: ∃ bd, IsRealizableBy C bd program would be vacuous, since a
representation is only required to be admissible, not canonical. Only the state
representation is chosen by the realization.

Closure

Theorem	Extra requirement
isRealizableBy_ofFn, isRealizableBy_pure	admissibility of the returning map
IsRealizableBy.precomp, IsRealizableWithin.precomp	admissibility of the reindexing map
IsRealizableBy.mapResult, IsRealizableWithin.mapResult	admissibility of the result map
IsRealizableBy.seqComp, IsRealizableWithin.seqComp	[C.IsDistributive]; budgets add
IsRealizableBy.wrap, IsRealizableWithin.wrap	Lens.IsAdmissible
IsRealizableBy.mono, IsRealizableWithin.mono'	StepClass.Refines

Plus IsRealizableWithin.{isRealizableBy, isTotalRollBound, mono} and congr in
Basic.lean. bind closure is listed as out of scope in VCVio#500's model.

Distributivity is consumed in exactly two places, both inside the composite
update?: splitting on the state summand, then on the first phase's readout. The
composite head needs no products at all.

Instances

Class	Str / Hom	Notes
unconstrained	PUnit / True	isRealizableBy_unconstrained: realizability collapses to ∃ M, M.Implements program
finite	Fintype / True	IsFiniteStateRealizable abbrev
computable	Primcodable / Computable	works today; exercises every mixin
WordClass	injective encoding into W / an intertwining W → W in the class	bridge from a monomorphic word class, via WordPairing, WordTagging, WordDistrib

---

Two design points a reviewer should check

update? is partial. The total convention (identity on junk) does not compose
across a state coproduct with a handoff:

answer tag	composite updateFlat	Sum.inr (M₂.updateFlat (M₂.init v, i))
matches M₂'s exposed position	Sum.inr (next₂ d)	Sum.inr (next₂ d) ✓
does not match	Sum.inl s₁	Sum.inr (M₂.init v) ✗

Reconciling those junk values needs the class to contain a decidable equality test
on interface positions, which is not derivable from products, coproducts and
distributivity. With none both rows agree, the both-phases-returned case is
subsumed, and update?_seqComp_inl holds unconditionally in the answer index.
updateFlat keeps its name and meaning, so VCVio#500's four-witness cost model is
unaffected.

head rather than an output / expose pair. VCVio#500 splits the readout,
which forces a default at resolved states; that convention breaks
compositionality, since (M.wrap lens).expose ≠ lens.toFunA ∘ M.expose exactly at
resolved states. head has no such wart. output and expose are still provided,
derived.

Naming

With HasProd, HasSum and IsDistributive, a StepClass is a distributive
category (Cockett, MSCS 1993; Carboni–Lack–Walters, JPAA 1993) presented
concretely over Type. The cogap direction of the canonical map is derivable from
products and sums alone and ships as codistrib_mem, so both directions are
admissible and this is the standard axiom rather than a weakening.

Mathlib's CategoryTheory.IsCartesianDistributive cites the same papers, but
MorphismProperty (Type u) cannot type a Hom indexed by representations, so
only the name and axiom are reused. Mathlib states the axiom in the cogap
orientation; our distrib_mem field is the inverse, and says so.

Not included

• The cost-bearing layer — Hom is Prop-valued, so nothing here measures
  running time or description size, which is what makes VCVio#500's model
  quantitative. The successor needs Hom replaced by a Type-valued witness
  carrying measures in an ordered semiring. From the audit of #500, it needs id,
  comp, copy (pointwise-equal transport, 9 call sites there), recode, with
  const/ofFintype as caller obligations — and no product or sum combinators.
• Crypto-specific content (Responder, WiredRun, CoinFold,
  PolyTimeNontrivial, ToMathlib/Computability/) stays in VCVio.
• A terminal/initial representation, hence only binary distributivity.
• Generalizing ImplementsWithin off a uniform ℕ budget.

Validation

• ./scripts/validate.sh --lint --test green: build (2019 jobs), module scopes,
  umbrella imports, docs integrity, lake lint, lake test.
• No sorry; no disabled linters. Axiom footprints of IsRealizableBy.seqComp,
  IsRealizableWithin.seqComp, IsRealizableBy.wrap,
  IsDistributive.elimCtx_mem, ofStep_step_eq_of_flat_eq are all within
  [propext, Classical.choice, Quot.sound]; several are axiom-free.
• PolyFunTest/Realizability/Examples.lean: a concrete two-state machine realizing
  a one-query program, two of them composed under bind at budget 1 + 1, and the
  rfl transport lemmas pinned so a regression to match in a step-map definition
  fails the test build.
• docs/wiki/realizability.md added; DAG block in docs/wiki/repo-map.md;
  AGENTS.md repo map and Further Reading; seven REFERENCES.md entries.

Open items

• Not yet built against VCVio. updateFlat keeps its name and meaning, and
  #500's local output / expose / stepD / ofStep / setInit can be deleted
  in favour of these — wants confirming against a real checkout before merge.
• Lens.IsAdmissible has no .id or .comp: pullHeadIdx compares the incoming
  answer's tag against the position the lens exposes, so even the identity lens's
  pullback performs an equality test on positions. Admissibility of a lens is a
  hypothesis about the class, not derivable from the mixins — which is also why
  wrap needs it and seqComp does not.
• HasOption.none_mem is the one constant map this layer assumes (a machine that
  has returned takes no step). Everything else takes constant-admissibility as a
  per-theorem hypothesis.
• WordClass needs WordDistrib because WordTagging.elim hands each branch only
  the untagged payload, so a tag cannot be moved past a pairing using elim alone.
  Consequence for real clients: complexitylib has the pairing ingredients
  (Complexity.pair, unpair?, delimit) but exposes no class-level closure
  result, and cslib's PolyTimeComputable has id/comp but no pairing or
  projection machines, plus a Monotone side condition on comp whose removal is
  still a TODO upstream. Neither plugs in today without upstream work.

🤖 Generated with Claude Code