deriv_a_sq
plain-language theorem explainer
For a differentiable scale factor a, the time derivative of a squared equals twice a times ȧ. Cosmologists and GR formalizers cite it when simplifying Christoffel symbols of flat FRW. The proof rewrites the squared map as composition with x ↦ x², applies the chain rule, and finishes by simp.
Claim. Let $a:\mathbb{R}\to\mathbb{R}$ be differentiable. Then for every $t\in\mathbb{R}$, $\frac{d}{dt}\bigl(a(t)^2\bigr)=2\,a(t)\,a'(t)$.
background
The module is a standalone tractability probe for flat FRW geometry (k=0, c=1) encoded componentwise on Fin 4. Every field depends only on cosmic time t, so spatial partials vanish and ∂₀ is ordinary differentiation. The metric is diagonal with g₀₀=-1 and spatial entries a(t)²; the inverse has spatial entries 1/a(t)².
Christoffel symbols are written in the usual second-kind formula Γ^λ_{μν}=½ Σ_σ g^{λσ}(∂μ g{νσ}+∂ν g{μσ}-∂σ g{μν}). Differentiating the spatial metric components therefore produces derivatives of a². The lemma states that identity in the exact lambda form the metric simp lemmas emit, so it chains under simp.
Upstream, the coordinate partial pd and the inverse metric gInv are the local definitions that make the Christoffel sum concrete; off-diagonal metric components are already known to vanish.
proof idea
Rewrite the pointwise square as composition of a with the global map x ↦ x² (definitional equality). Apply the chain rule at t, using differentiability of the power map at a(t) and of a at t. The remaining derivative of x² is 2x; simp closes the arithmetic to 2·a(t)·a'(t).
why it matters
This is the differential-algebra hinge of the FRW componentwise probe. The panel's named first probes are Γ⁰ᵢᵢ=a·ȧ and Γⁱ₀ᵢ=ȧ/a; both simp scripts invoke the lemma when expanding the Christoffel sum against gInv and pd. Downstream it is re-exported into FRWFriedmann and feeds christoffel_0_11, christoffel_0_22, christoffel_0_33, christoffel_1_01, christoffel_2_02, christoffel_3_03, and ultimately ricci_00.
If the probe closes, the full two-layer skeleton (Ricci, Einstein tensor, Friedmann I/II from a named EinsteinEqns Prop) is locked as loop targets. The lemma itself is pure real analysis; its place in Recognition is as the first non-stalling step that shows the Fin-4 encoding is simp-dischargeable before the cosmology chain is committed.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.