the modified market's computability is discharged, via an additive upstream export

ComputableMarket is no longer a premise of the traderized-deduction chain, and the object that replaced it is constructed rather than assumed. The blocker was module visibility: marketMakerSearchUpToTradeList_prim, tradingFirmTradesFromStageTradeLists_prim and efAbsBound_prim are private in the pinned dependency's LIACompiler.lean, and that file carries 398 private declarations, so re-deriving them downstream would have meant re-deriving the file.

The resolution is an upstream section that re-exports those ingredients publicly and changes nothing else — no definition, statement or proof above it is touched, so nothing that built before can break. The recurrence itself is deliberately not exported: a downstream construction states and proves its own, which is where its soundness obligation belongs.

Statements of record: Workspace.Normativity.Contrib.EnforcedCompiler.computableMarket, .isLogicalInductor, .ProjectionSchedule.end_to_end_effective. The one standing hypothesis, Primrec₂ E.trades (EffectiveEnforcerComputation), is the definition of an effective enforcer and sits where DeductiveProcessComputation sits upstream.