minkowski_preserves_inner
Minkowski spacetime preserves the inner product of any two parallel-transported vector fields along an arbitrary curve. Researchers checking metric compatibility in the flat-space limit of general relativity or confirming the trivial holonomy case would cite the result. The tactic proof invokes parallel_transport_flat to obtain constant components, expands the inner product into four independent products, and verifies that each product has vanishing derivative.
claimIn Minkowski spacetime with metric tensor $η$, for any smooth curve $γ:ℝ→ℝ^4$, if vector fields $V$ and $W$ are parallel transported along $γ$, then the inner product $η(V,W)$ is constant along $γ$.
background
SpacetimeCurve is a smooth map from the real line to 4-dimensional spacetime together with its tangent vector field. ParallelTransportPreservesInnerProduct is the predicate asserting that the metric inner product of two vector fields remains constant whenever both fields satisfy the parallel-transport ODE with respect to the Levi-Civita connection of the given metric. The module works in the setting of 4D spacetime equipped with the Levi-Civita connection derived from Curvature.christoffel; parallel transport is defined by the first-order ODE that keeps the vector “as parallel as possible.” Upstream, parallel_transport_flat establishes that every parallel-transported vector field on Minkowski space is literally constant, which is the key algebraic simplification used here.
proof idea
The tactic proof begins by introducing the two vector fields and the parameter value. It applies parallel_transport_flat twice to replace the parallel-transport conditions with the statement that both fields are constant. Four auxiliary real-valued functions are defined as the component-wise products of the two fields. Differentiability of each product follows from the product rule on the given smoothness hypotheses. Each product’s derivative is shown to vanish by substituting the constancy statements into the product rule for derivatives. The inner-product sum is rewritten, via the explicit components of the Minkowski metric, as the linear combination −t0 + t1 + t2 + t3. The derivative of this combination is therefore the same linear combination of the four zero derivatives and hence zero.
why it matters in Recognition Science
The theorem supplies the inner_product_preserved field required by parallel_transport_cert_minkowski, thereby completing the ParallelTransportCert instance for the Minkowski metric. In the Recognition Science framework this confirms that a uniform J-cost defect density produces a flat geometry with no holonomy, consistent with the forcing chain that yields D = 3 and the position-independent Minkowski tensor. It closes the flat-space case before the module proceeds to HolonomyDefect and the curvature-holonomy correspondence.
scope and limits
- Does not prove inner-product preservation for any non-Minkowski metric.
- Does not compute finite holonomy around closed loops.
- Does not treat non-smooth or non-differentiable curves.
- Does not derive the Minkowski metric from the J-cost functional.
Lean usage
theorem parallel_transport_cert_minkowski : ParallelTransportCert minkowski_tensor where flat_trivial := fun γ V h_eq h_pt => by simpa [h_eq] using parallel_transport_flat γ V h_pt inner_product_preserved := minkowski_preserves_innerformal statement (Lean)
119theorem minkowski_preserves_inner (γ : SpacetimeCurve) :
120 ParallelTransportPreservesInnerProduct minkowski_tensor γ := by
proof body
Tactic-mode proof.
121 intro V W h_diffV h_diffW hV hW lam
122 have hV_const := parallel_transport_flat γ V hV
123 have hW_const := parallel_transport_flat γ W hW
124 let t0 : ℝ → ℝ := fun l => V l 0 * W l 0
125 let t1 : ℝ → ℝ := fun l => V l 1 * W l 1
126 let t2 : ℝ → ℝ := fun l => V l 2 * W l 2
127 let t3 : ℝ → ℝ := fun l => V l 3 * W l 3
128 have ht0_diff : DifferentiableAt ℝ t0 lam := by
129 unfold t0
130 exact (h_diffV 0 lam).mul (h_diffW 0 lam)
131 have ht1_diff : DifferentiableAt ℝ t1 lam := by
132 unfold t1
133 exact (h_diffV 1 lam).mul (h_diffW 1 lam)
134 have ht2_diff : DifferentiableAt ℝ t2 lam := by
135 unfold t2
136 exact (h_diffV 2 lam).mul (h_diffW 2 lam)
137 have ht3_diff : DifferentiableAt ℝ t3 lam := by
138 unfold t3
139 exact (h_diffV 3 lam).mul (h_diffW 3 lam)
140 have ht0_zero : deriv t0 lam = 0 := by
141 unfold t0
142 simpa [hV_const lam 0, hW_const lam 0] using
143 (((h_diffV 0 lam).hasDerivAt).mul ((h_diffW 0 lam).hasDerivAt)).deriv
144 have ht1_zero : deriv t1 lam = 0 := by
145 unfold t1
146 simpa [hV_const lam 1, hW_const lam 1] using
147 (((h_diffV 1 lam).hasDerivAt).mul ((h_diffW 1 lam).hasDerivAt)).deriv
148 have ht2_zero : deriv t2 lam = 0 := by
149 unfold t2
150 simpa [hV_const lam 2, hW_const lam 2] using
151 (((h_diffV 2 lam).hasDerivAt).mul ((h_diffW 2 lam).hasDerivAt)).deriv
152 have ht3_zero : deriv t3 lam = 0 := by
153 unfold t3
154 simpa [hV_const lam 3, hW_const lam 3] using
155 (((h_diffV 3 lam).hasDerivAt).mul ((h_diffW 3 lam).hasDerivAt)).deriv
156 have h_expand :
157 (fun l =>
158 Finset.univ.sum (fun μ =>
159 Finset.univ.sum (fun ν =>
160 minkowski_tensor.g (γ.path l) (fun _ => 0) (fun i => if i.val = 0 then μ else ν) *
161 V l μ * W l ν))) =
162 fun l => -t0 l + t1 l + t2 l + t3 l := by
163 funext l
164 unfold t0 t1 t2 t3
165 rw [finset_sum_fin_4]
166 simp [minkowski_tensor, eta]
167 rw [h_expand]
168 calc
169 deriv (fun l => -t0 l + t1 l + t2 l + t3 l) lam
170 = -(deriv t0 lam) + deriv t1 lam + deriv t2 lam + deriv t3 lam := by
171 simp [ht0_diff, ht1_diff, ht2_diff, ht3_diff]
172 _ = 0 := by rw [ht0_zero, ht1_zero, ht2_zero, ht3_zero]; ring
173
174/-! ## §4 Holonomy: Curvature as Parallel Transport Failure -/
175
176/-- A closed loop in spacetime, parameterized by λ ∈ [0, 1] with γ(0) = γ(1). -/