RealGeodesic
RealGeodesic encodes a curve in four-dimensional spacetime whose second derivatives satisfy the geodesic equation built from the real Christoffel symbols of a supplied metric tensor. Workers unifying Recognition Science with general relativity cite it when they need the physically correct connection coefficients rather than any scaffold version. The declaration is a direct structure definition that assembles the path map and the explicit differential equation without lemmas or tactics.
claimA curve $x:ℝ→ℝ^4$ is a real geodesic for metric tensor $g$ when, for every parameter value $λ$ and index $μ$, the second derivative satisfies $d²x^μ/dλ² + ∑_{ρ,σ} Γ^μ_{ρσ}(x(λ)) (dx^ρ/dλ)(dx^σ/dλ) = 0$, where the Christoffel symbols $Γ$ are those computed by the curvature module from the components of $g$.
background
The MetricUnification module shows that the Minkowski metric obtained from the Recognition Science forcing chain (RCL → J-uniqueness at T5 → eight-tick octave at T7 → D=3 at T8) is identical to the standard η = diag(−1,+1,+1,+1). MetricTensor supplies the local bilinear form g_μν(x) at each spacetime point; two sibling interfaces appear in Hamiltonian and Gravity.Connection. The Christoffel symbols are taken from the Curvature module (which re-exports the real implementation) rather than the scaffold version in Connection.
proof idea
Structure definition that directly assembles the path function ℝ→(Fin 4→ℝ) together with the predicate stating that the second derivative plus the double sum of christoffel g (path lam) μ ρ σ times the two first derivatives equals zero. No lemmas are applied and the body contains no tactics.
why it matters in Recognition Science
RealGeodesic is the base structure extended by TimelikeGeodesic, SpacelikeGeodesic and RealNullGeodesic, and is invoked by the theorem geodesic_uses_real_christoffel to certify that all downstream trajectories employ the real Christoffel symbols. It thereby completes the bridge from the RS-derived metric to standard GR dynamics, allowing results such as minkowski_straight_line_geodesic to inherit the origin of η from the forcing chain.
scope and limits
- Does not impose any interval signature (timelike, null or spacelike) on the curve.
- Does not guarantee existence or uniqueness of solutions to the geodesic equation.
- Does not restrict the metric tensor to be Minkowski.
- Does not compute explicit solutions for any concrete metric.
formal statement (Lean)
110structure RealGeodesic (g : MetricTensor) where
111 path : ℝ → (Fin 4 → ℝ)
112 geodesic_equation : ∀ lam μ,
113 deriv (deriv (fun lam' => path lam' μ)) lam +
114 Finset.sum Finset.univ (fun ρ =>
115 Finset.sum Finset.univ (fun σ =>
116 christoffel g (path lam) μ ρ σ *
117 (deriv (fun lam' => path lam' ρ) lam) *
118 (deriv (fun lam' => path lam' σ) lam))) = 0
119
120/-- A timelike geodesic: path with negative interval, using real Christoffel. -/