The flat FRW metric is encoded componentwise on Fin 4 with g_{00} = -1 and g_{ii} = a(t)^2 (i ≠ 0), all fields depending only on cosmic time t so that spatial partials vanish and ∂_0 = deriv.
The Christoffel symbol of the second kind is Γ^λ_{μν} = ½ Σ_σ g^{λσ} (∂μ g{νσ} + ∂ν g{μσ} − ∂σ g{μν}).
Probe 1 requires Γ^0_{11} = a · ȧ.
Γ_0_11 states: for differentiable a : ℝ → ℝ and any t : ℝ, Γ a 0 1 1 t = a t * deriv a t.
The proof applies simp to the definitions of Γ, gInv, pd and Fin.sum_univ_four together with the auxiliary lemma deriv_a_sq (which expands deriv((a t)^2) = 2 a t deriv a t) followed by ring normalization. The same encoding yields the companion result Γ_1_01 for the second probe goal, confirming the componentwise differential algebra is tractable.