SmoothField
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.
claimA 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 in Recognition Science
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.
scope and limits
- Does not specify the connection or the underlying metric tensor.
- Does not guarantee existence or uniqueness of parallel transport solutions.
- Does not incorporate J-cost, phi-ladder, or recognition composition law.
- Does not address global topology or closed-loop integrability.
formal statement (Lean)
65def SmoothField (V : ℝ → (Fin 4 → ℝ)) : Prop :=
proof body
Definition body.
66 ∀ μ, Differentiable ℝ (fun l => V l μ)
67
68/-- Initial conditions for parallel transport: a vector at parameter λ₀. -/