Repository navigation
[FORM-S6] Entropy production for Markov-chain path laws (fep-094, 098, 099) #89
Description
Scope ID: FORM-S6. Size: Medium. Scoped on 2026-10-08 in SCOPE-2026-10-08.md; acceptance remains open.
Owner: path-space thermodynamics foundation.
Dependencies: FORM-D3
Work
FinitePathProtocol is an arbitrary law pair; nothing builds a path law from a kernel, and fep-094's primary equality is a definition. Build forward/reverse path laws from (π₀, K, n) on Fin (n+1) → State; prove path KL = stage log-ratios + boundary entropy, and the stationary rate equals the Schnakenberg form.
Acceptance
Chain-rule identity; reduction to fep-099 at n = 1; zero under detailed balance (fep-098); positive rate on the existing three-cycle witness.
Failure controls and claim boundary
No disposition promotion from compilation, import or numerical agreement; the maturity record changes only after independent semantic review. No duplicate topics and no automatic sealed-roster expansion.
Canonical references
Closure requires actual exact-source commands, results and retained receipts, with independent review where specified. Remove its open TODO row only after acceptance; retain delivery facts in changelog/history. Size describes implementation scope, not a semantic-version promise.
Activity
docxology commentedon Oct 9, 2026
Status update (2026-10-09). Delivered in #163 (via #164), merged to
main: General-n Markov path laws with normalisation, the path-KL decomposition, reversed-kernel duality (zero entropy production), the Schnakenberg form tied to the fep-098localAffinity, the stationary and reversible reductions, and an irreversible witness with exact rate log 2 / 4. Detailed-balance zero for general n is not stated separately; it follows from the duality. This unblocks FORM-S5 (#88).Evidence:
lake --wfail build FepSketchespasses at the pin (Lean v4.34.1, Mathlibd13f23b7), every new declaration depends only onpropext/Classical.choice/Quot.sound, and all generator--checks plus hosted CI pass.Remaining for closure: independent semantic review of the delivered statements against the topic's theorem proxy. Per this issue's claim boundary, no disposition in
config/theorem_maturity.yamlwas changed, and none may change without that review.docxology commentedon Oct 11, 2026
Delivered on
maininFEP.PathThermodynamics: general-horizonmarkovPathLawandmarkovReversePathLaw, the Schnakenberg form, reversed-kernel duality, the zero under detailed balance at n = 1, and the positive three-cycle rate (biasedCycle_entropyProduction_pos). Still open: the path-KL chain rule is proved only at n = 1, and no declaration tiesmarkovPathProtocol … 1to fep-099. TheTODO.mdrow is narrowed in #171 to the remaining clause.