Formal: generalized-coordinate jets are actual derivatives (FORM-S8)

docs/formalism-coverage.json

@@ -1386,7 +1386,7 @@
     },
     {
       "abbreviation_count": 0,
-      "definition_count": 10,
+      "definition_count": 11,
       "formal_dependencies": [],
       "id": "formal-module-predictive-coding",
       "imports": [
@@ -1395,6 +1395,8 @@
         "Mathlib.Analysis.Calculus.Deriv.Add",
         "Mathlib.Analysis.Calculus.Deriv.Mul",
         "Mathlib.Analysis.Calculus.Deriv.Pow",
+        "Mathlib.Analysis.Calculus.IteratedDeriv.Defs",
+        "Mathlib.Analysis.SpecialFunctions.ExpDeriv",
         "Mathlib.Basic.Real.Basic",
         "Mathlib.Order.Filter.Tendsto",
         "Mathlib.Topology.Algebra.Monoid",
@@ -1404,13 +1406,15 @@
       "resource": "predictive_coding.lean",
       "role": "foundation",
       "structure_count": 1,
-      "theorem_count": 30,
+      "theorem_count": 37,
       "theorems": [
         "FEP.PredictiveCoding.doubledPrecision_nontrivial_witness",
+        "FEP.PredictiveCoding.exp_jet_shift_witness",
         "FEP.PredictiveCoding.firstOrderCorrection_witness",
         "FEP.PredictiveCoding.firstOrderJet_shift_boundary",
         "FEP.PredictiveCoding.firstOrderJet_value",
         "FEP.PredictiveCoding.firstOrderJet_velocity",
+        "FEP.PredictiveCoding.functionJet_coefficient_of_le",
         "FEP.PredictiveCoding.generalizedCoordinateEnergy_hasDerivAt",
         "FEP.PredictiveCoding.generalizedFilteringStep_equation",
         "FEP.PredictiveCoding.generalizedFlow_top_boundary",
@@ -1420,6 +1424,7 @@
         "FEP.PredictiveCoding.iteratePredictionEnergy_tendsto_zero",
         "FEP.PredictiveCoding.iteratePredictionError",
         "FEP.PredictiveCoding.iteratePredictionError_tendsto_zero",
+        "FEP.PredictiveCoding.iteratedDeriv_exp_eq",
         "FEP.PredictiveCoding.precisionEnergy_derivative_eq_gradient",
         "FEP.PredictiveCoding.precisionEnergy_eq_zero_iff",
         "FEP.PredictiveCoding.precisionEnergy_hasDerivAt",
@@ -1433,6 +1438,10 @@
         "FEP.PredictiveCoding.predictionError_update",
         "FEP.PredictiveCoding.shift_add",
         "FEP.PredictiveCoding.shift_coefficient",
+        "FEP.PredictiveCoding.shift_functionJet",
+        "FEP.PredictiveCoding.shift_functionJet_succ",
+        "FEP.PredictiveCoding.shift_one_functionJet",
+        "FEP.PredictiveCoding.shift_one_functionJet_top",
         "FEP.PredictiveCoding.shift_top_zero",
         "FEP.PredictiveCoding.shift_zero",
         "FEP.PredictiveCoding.twoLevelEnergy_witness"
@@ -4424,23 +4433,23 @@
     "authored_relation_edges": 146,
     "capability_nodes": 50,
     "composed_theorems": 332,
-    "definitions": 896,
+    "definitions": 897,
     "distinct_mathlib_imports": 70,
     "formal_module_dependency_edges": 162,
-    "formal_module_import_edges": 272,
+    "formal_module_import_edges": 274,
     "formal_modules": 71,
     "formal_pairing_witnesses": 118,
     "formal_relation_witnesses": 20,
     "formal_resource_abbreviations": 31,
-    "formal_resource_definitions": 801,
+    "formal_resource_definitions": 802,
     "formal_resource_structures": 53,
-    "formal_resource_theorems": 1369,
+    "formal_resource_theorems": 1376,
     "foundation_modules": 45,
-    "foundation_theorems": 1037,
+    "foundation_theorems": 1044,
     "open_capabilities": 0,
     "satisfied_capabilities": 50,
     "theorem_witnessed_relations": 138,
-    "theorems": 1953,
+    "theorems": 1960,
     "topic_abbreviations": 7,
     "topic_definitions": 95,
     "topic_import_edges": 225,

docs/formalism-coverage.md

@@ -14,19 +14,19 @@ Counts describe canonical source coverage. Compilation evidence and full externa
 | Maintained formal modules | 71 |
 | Foundation modules | 45 |
 | Topic theorem declarations | 584 |
-| Formal-resource theorem declarations | 1369 |
-| Foundation theorem declarations | 1037 |
-| Total theorem declarations | 1953 |
+| Formal-resource theorem declarations | 1376 |
+| Foundation theorem declarations | 1044 |
+| Total theorem declarations | 1960 |
 | Topic definitions | 95 |
-| Formal-resource definitions | 801 |
-| Total definitions | 896 |
+| Formal-resource definitions | 802 |
+| Total definitions | 897 |
 | Topic abbreviations | 7 |
 | Formal-resource abbreviations | 31 |
 | Total abbreviations | 38 |
 | Formal-resource structures | 53 |
 | Distinct Mathlib imports | 70 |
 | Topic-to-import edges | 225 |
-| Formal-resource import edges | 272 |
+| Formal-resource import edges | 274 |
 | Internal formal-module dependencies | 162 |
 | Authored formalism relations | 146 |
 | Derivational formal relations | 20 |
@@ -245,7 +245,7 @@ These packaged modules are a distinct proof surface from the generated topic ske
 | `FepSketches.temporal_inference` | `foundation` | 34 | 18 | 1 | `FepSketches.controlled_markov` |
 | `FepSketches.finite_markov_dynamics` | `foundation` | 17 | 6 | 0 | `FepSketches.finite_probability` |
 | `FepSketches.causal_dynamics` | `foundation` | 34 | 18 | 2 | `FepSketches.markov_blanket` |
-| `FepSketches.predictive_coding` | `foundation` | 30 | 10 | 1 | — |
+| `FepSketches.predictive_coding` | `foundation` | 37 | 11 | 1 | — |
 | `FepSketches.ness_flow` | `foundation` | 9 | 6 | 0 | — |
 | `FepSketches.path_thermodynamics` | `foundation` | 25 | 12 | 1 | `FepSketches.finite_markov_dynamics`, `FepSketches.variational_duality` |
 | `FepSketches.geometric_optimization` | `foundation` | 25 | 17 | 3 | `FepSketches.information_geometry` |