ParallelTransportIC
plain-language theorem explainer
ParallelTransportIC records the starting affine parameter and 4-vector for a parallel-transport problem on a spacetime curve. Workers on the Recognition Science account of curvature would cite the record when assembling solutions that satisfy the Levi-Civita transport equation. The declaration is a bare structure definition with two fields and no further content.
Claim. Initial data for parallel transport consist of a real number $λ_0$ together with a vector $V_0 ∈ ℝ^4$.
background
The module formalizes parallel transport along curves in 4D spacetime via the Levi-Civita connection defined in Curvature.christoffel. Key supporting notions include the predicate ParallelTransported, the type SpacetimeCurve, and the metric tensor from Metric. In Recognition Science, curvature arises from non-uniform J-cost defect density; parallel-transport failure around closed loops is the geometric signature of that ledger imbalance.
proof idea
The declaration is a structure definition that introduces exactly two fields: lam0 of type ℝ and V0 of type Fin 4 → ℝ.
why it matters
The record supplies the initial data consumed by ParallelTransportSolution, which builds the transported vector field and its initial-condition proof. It therefore participates in the module's development of holonomy and curvature statements that realize the Recognition Science claim that curvature is forced by J-cost defects. The surrounding development sits inside the T0–T8 forcing chain with D = 3 spatial dimensions and the eight-tick octave.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.