minkowski_preserves_inner
plain-language theorem explainer
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.
Claim. In 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
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.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.