Repository navigation
[FORM-S8] Tie generalized-coordinate jets to actual derivatives (fep-089, 090) #91
Description
Scope ID: FORM-S8. Size: Minor. Scoped on 2026-10-08 in SCOPE-2026-10-08.md; acceptance remains open.
Owner: predictive-coding foundation and generalized-coordinate bodies.
Dependencies: FORM-D3
Work
FiniteJet (predictive_coding.lean:136) is a coefficient list with a combinatorial shift; nothing links it to a trajectory. Define jet f t k := iteratedDeriv k f t and prove shift 1 (jet f t) = jet (deriv f) t below the order, so generalized-coordinate D is differentiation.
Acceptance
A nonzero exp/polynomial witness where shift matches deriv in every coordinate, plus the truncation-boundary statement.
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 #157 (via #164), merged to
main:functionJetwith coordinate k equal toiteratedDeriv k f t,shift_one_functionJetandshift_functionJet(shift is differentiation below the truncation order), the truncation-boundary theorem, and theReal.expwitness.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,functionJetcoordinates are iterated derivatives, andshift_functionJetmatchesderivin every coordinate.shift_one_functionJet_topgives the truncation boundary, andexp_jet_shift_witnessis the nonzero witness. Row retired.