Formal: entropy production for Markov-chain path laws, Schnakenberg form, reversed-kernel duality (FORM-S6)

[docxology]

Refs #89 (FORM-S6). Not closing: fep-094/098/099 dispositions change only after independent review. This unblocks FORM-S5 (#88), the Landauer bound for biased bits.

FinitePathProtocol was an arbitrary pair of laws, and fep-094's primary equality was a definition. New in path_thermodynamics.lean (existing declarations unchanged):

1. Markov path laws for general n. markovPathLaw K π₀ n on Fin (n+1) → S has mass π₀(x₀)∏K(xₜ,xₜ₊₁), proved normalised by Fin.snoc induction. markovPathProtocol wraps it as a FinitePathProtocol, so the existing entropyProduction now applies to a concrete construction.
2. Path-KL decomposition for general n. entropyProduction_markov_decomposition gives path KL as the expected boundary term plus the sum of expected stage log-ratios. The one-step forms are explicit.
3. Reversed-kernel duality.
   • reversedKernel is K†_ab = π_b K_ba / π_a.
   • It satisfies detailed balance against K, and equals K under reversibility.
   • markovReverseMass_reversedKernel: for every n, the reverse-driven chain under K† reproduces the forward path law, by telescoping. So that protocol has zero entropy production.
4. Schnakenberg form.
   • entropyProduction_markov_schnakenberg: ∑ πᵢKᵢⱼ log(πᵢKᵢⱼ/(πⱼKⱼᵢ)).
   • It is restated through the existing fep-098 localAffinity.
   • The stationary reduction removes the boundary term.
   • Under IsReversible it is exactly zero (fep-098), with no support hypothesis.
5. Positive-rate witness. The existing three-cycle has zero reverse rates, so it violates full support. Instead, a full-support biased 3-cycle has a uniform stationary law, is not reversible, and has entropy production exactly log 2 / 4 > 0.

Not covered: detailed-balance zero for general n is not stated separately; it follows from item 3. Schnakenberg needs full support, and a zero edge is the totalized-log boundary already documented in the module.

Evidence:

• lake --wfail build FepSketches passes, and every axiom set is the standard three.
• Projections were regenerated by their owners, and every --check passes, as do the receipt, theorem_ref_audit and orphan checks.
• Pins: path_thermodynamics 25 → 56, lexical 1,953 → 1,984.
• Tests and ruff pass.