weakFieldAlgebraStub
plain-language theorem explainer
The declaration supplies a stub instance for WeakFieldAlgebraFacts in the relativity fixtures module, allowing downstream proofs on linearized gravity to compile without sorries. Researchers working on post-Newtonian expansions or weak-field limits within Recognition Science would cite it to maintain proof continuity. The implementation reduces to a short tactic sequence that verifies a trivial non-negativity bound on the error term.
Claim. Let WeakFieldAlgebraFacts be the structure whose field inverse_first_order_identity_minkowski asserts that the first-order inverse metric identity holds in Minkowski space with error bounded by $8e + 4e^2$ whenever $e > 0$. The definition weakFieldAlgebraStub realizes this structure by exhibiting a proof of the bound $|0| ≤ 8e + 4e^2$.
background
The Relativity.NewFixtures module collects stub instances for hypothesis classes that temporarily replace sorries, keeping them outside production namespaces to preserve a clear trust boundary. WeakFieldAlgebraFacts encodes algebraic identities required for the inverse metric in the weak-field regime around flat space. The supplied proof body uses only elementary real-number facts on non-negativity and linear arithmetic.
proof idea
The proof is a short tactic sequence: introduce the hypotheses, establish non-negativity of the right-hand side via le_of_lt on eps_pos followed by nlinarith, then apply simpa to conclude the target inequality.
why it matters
This stub closes a temporary gap in the weak-field algebra layer and permits the surrounding chain of fixtures (gaugeFactsStub through radialPoissonStub) to compile. It supports the larger program of recovering general-relativity features from the Recognition Science forcing chain without blocking on algebraic details. The declaration touches the open question of whether the full weak-field limit follows rigorously from J-uniqueness and the phi-ladder.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.