curvatureFactsStub
plain-language theorem explainer
The curvatureFactsStub supplies a placeholder instance of CurvatureExpansionFacts inside the relativity fixtures module. It would be cited by any proof that needs temporary access to first-order curvature expansions while full derivations remain pending. The definition is realized directly by assigning norm_num reductions to the three required fields for the Riemann, Ricci, and scalar expansions.
Claim. Let $CurvatureExpansionFacts$ be the structure whose fields are the first-order expansions of the Riemann tensor $R^ρ{}_{σμν}(g_0 + h)$, the Ricci tensor $R_{μν}(g_0 + h)$, and the Ricci scalar $R(g_0 + h)$. The stub instance sets each expansion map to the zero function.
background
The module Relativity.NewFixtures supplies stub instances for hypothesis classes introduced to replace sorries, keeping the trust boundary explicit. CurvatureExpansionFacts is the structure that packages the three expansion identities needed for weak-field curvature calculations in a perturbed metric. No upstream lemmas are referenced; the declaration stands alone with zero dependencies.
proof idea
The definition constructs the instance by providing three separate proof terms, each obtained by introducing the metric, perturbation, and index variables and then applying the norm_num tactic. This reduces every required identity to a trivial numerical equality.
why it matters
It belongs to the fixture collection that includes gaugeFactsStub, matrixBridgeFactsStub, and the remaining relativity stubs, allowing modular progress on weak-field results. The stub supports downstream work on linearized PDEs and modified Poisson equations without introducing sorries. It touches the weak-field sector of the Recognition framework but carries no direct connection to the T0-T8 chain or the Recognition Composition Law.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.