SmoothField
plain-language theorem explainer
SmoothField is a predicate requiring that each of the four components of a vector field V along a real affine parameter is differentiable. It is cited in statements of parallel transport preservation and holonomy defects within the Levi-Civita connection on 4D spacetime. The definition is a direct encoding of componentwise differentiability with no lemmas or reductions.
Claim. A map $V : ℝ → ℝ^4$ is smooth if for every component index $μ$, the real function $λ ↦ V(λ)_μ$ is differentiable.
background
The module formalizes parallel transport along curves in 4D spacetime via the Levi-Civita connection (Curvature.christoffel). Parallel transport moves a vector while keeping it as parallel as possible; on curved manifolds the failure around closed loops yields holonomy proportional to the Riemann tensor. In Recognition Science this failure is the geometric signature of non-uniform J-cost defect density that sources gravity.
proof idea
The definition is a direct predicate: it asserts componentwise differentiability over the reals for the four-component vector field. No upstream lemmas are invoked; the body simply quantifies over μ and applies the standard Differentiable predicate from Mathlib.
why it matters
SmoothField supplies the differentiability hypothesis used by HolonomyDefect (which equates the defect to the Riemann contraction over an infinitesimal area) and by ParallelTransportPreservesInnerProduct (which shows the metric inner product is constant along the curve). It therefore supports the module's main results linking curvature to ledger imbalance in the Recognition framework, consistent with the forcing of D=3 and the eight-tick octave.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.