christoffelStub
plain-language theorem explainer
This stub definition supplies a placeholder instance for the ChristoffelExpansionFacts structure in the weak-field limit of general relativity. It would be referenced by maintainers of the relativity fixtures to eliminate sorries while preserving a clear trust boundary. The implementation proceeds via a nonnegativity argument establishing the Minkowski bound followed by simplification for the Newtonian component.
Claim. Let $Γ^λ_{μν}$ denote the Christoffel symbols. The stub asserts that $|Γ^λ_{μν}| ≤ 40ε²$ holds in the Minkowski background under weak-field conditions with small parameter $ε$, and that the 00-component reduces to the Newtonian gravitational expression.
background
The NewFixtures module supplies stub instances for hypothesis classes introduced to replace sorries. These live outside production namespaces to keep the trust boundary clear, as stated in the module documentation. ChristoffelExpansionFacts is the structure that packages the Minkowski expansion bound together with the Newtonian 00-component formula.
proof idea
The Minkowski bound proof introduces the weak-field hypothesis, establishes nonnegativity of 40ε² via sq_nonneg and nlinarith, then applies simpa. The Newtonian 00 formula is discharged by a direct simp tactic on the structure definition.
why it matters
This declaration populates one of the stub fixtures in the relativity module and immediately supplies the following instance declaration. It supports progress on sibling stubs such as linearizedPDEStub and ppnInverseStub. In the Recognition framework it touches the weak-field approximations needed to connect gravity to the phi-ladder and eight-tick octave, though no explicit link is forged here.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.