partialDeriv
plain-language theorem explainer
partialDeriv supplies a coordinate partial derivative for scalar functions on the manifold by reducing it to an ordinary derivative along a line that perturbs only one coordinate. Geodesic modules cite it when expressing directional changes along basis vectors in uniqueness and straight-line constructions. The implementation is a direct one-line definition that applies the standard real derivative to a coordinate-shifted family evaluated at zero.
Claim. Let $M$ be a manifold, $f$ a scalar function from points of $M$ to reals, and $x$ a point with coordinates in Fin $M.dim$. For index $mu$, the partial derivative is defined as the ordinary derivative at zero of $f$ composed with the path that adds $t$ only to the $mu$-th coordinate of $x$ while leaving all other coordinates unchanged.
background
Manifold is a structure carrying a natural-number dimension; Point M is the type of maps from Fin M.dim to reals that represent coordinate tuples. This module is labeled a scaffold whose definitions are structural placeholders to let downstream relativity code type-check; the module documentation states explicitly that it is not part of the verified certificate chain and should not be cited as rigorous mathematics. Upstream, the dimension value is supplied by the dim definition in TauStepDerivation (which sets it to D) and by the recognition structures M appearing in the core Recognition and Cycle3 modules.
proof idea
The definition is a one-line wrapper that applies the standard real derivative operator to the auxiliary function obtained by shifting only the selected coordinate index by the real parameter t, then evaluates the result at t = 0.
why it matters
It is referenced by the geodesic_unique theorem and the straight_null_geodesic definition inside the NullGeodesic module, supplying the directional derivative needed for coordinate-based path comparisons. As part of the relativity geometry scaffold it enables typing of manifold constructions without contributing to the core Recognition Science certificate chain. The module documentation flags the open question of embedding a full, verified differential geometry into the framework built from the J-uniqueness and forcing-chain steps.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.