Repository navigation
[FORM-S9] Predictive-coding energy as a negative log joint, with precision inferred #92
Description
Scope ID: FORM-S9. Size: Minor. Scoped on 2026-10-08 in SCOPE-2026-10-08.md; acceptance remains open.
Owner: predictive-coding and Gaussian information-geometry foundations.
Dependencies: FORM-D3
Work
hierarchicalEnergy sums weighted squared errors over arbitrary variables; fep-091's primary theorem is monotonicity in a fixed weight. Prove (a) the linear-Gaussian chain energy equals the negative log native density up to a constant, and (b) ½πε² − ½ log π has the unique minimiser π* = 1/ε².
Acceptance
Both statements, plus a two-level witness tied to fep087_twoLevel_decomposition_nonvacuity.
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 #160 (via #164), merged to
main: Precision as inference: the unique minimiser π* = 1/ε², the derivative, strict convexity, and the ε = 0 unboundedness boundary. Also the linear-Gaussian chain energy as exactly −log ∏ N up tocard/2·log(2π)via Mathlib'sgaussianPDFReal, and a two-level witness.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
Accepted on
mainvia #171. InFEP.PredictiveCoding:gaussianChainEnergy_eq_neg_log_prod(energy is a negative log joint),precisionFreeEnergy_eq_iff(unique optimum1/ε²) andtwoLevel_chain_energy_witness, tied to the fep-087 two-level data. Any maturity change still needs independent semantic review. Row retired.