Integrate the Lean formalism wave: #156–#163 with one regeneration and one CI run

[docxology]

Merges the eight open Lean PRs in a single step. Each one passed its own build and checks, but they all regenerate the same projections and pins, so merging them one at a time would have taken eight serial CI cycles with a conflict in each. When this lands, GitHub marks each PR merged, because its head commit is in main.

PR	Issue	Content
#157	FORM-S8 #91	Generalized-coordinate jets are derivatives
#156	LEAN-1 #99	One shared finite-matrix kit
#158	FORM-S2 #85	General finite MaxEnt and the constrained Gibbs maximiser
#159	LEAN-6/8 #104 #106	Pairing review; derivational edges for 4 isolated topics
#160	FORM-S9 #92	Precision as inference; predictive-coding energy = −log joint
#161	FORM-S3 #86	Helmholtz free energy as the variational minimum, with dF/dT = −H
#162	FORM-S13 #96	Optimal linear/log pooling; Dobrushin consensus
#163	FORM-S6 #89	Markov path laws, Schnakenberg form, reversed-kernel duality

Integration: the Lean sources merged cleanly except for two appended sections in variational_duality.lean (MaxEnt from #158, Helmholtz from #161), and both are kept. Their definitions don't clash: energyGibbsLaw and helmholtzGibbsLaw use different parameterisations, β versus T. Projections were regenerated once by their owners. Pins are set to the measured totals, which match the additive expectation exactly: lexical declarations 2,053 = 1,946 + 107, predictive_coding 47, variational_duality 74.

Evidence on the integrated tree

• lake --wfail build FepSketches: 8,997 jobs, zero warnings.
• Every generator --check and methods check pass.
• check_render_log --verify-receipt, theorem_ref_audit, check_orphan_compiles, citation_audit and xref_audit pass.
• 204 formal, relation and methods tests pass, as do ruff, format, mypy, links and hygiene.

Formalism issues stay open pending independent semantic review, per their claim boundaries. No disposition was promoted.