grLimitRegularityStub
plain-language theorem explainer
This definition supplies a trivial stub instance of GRLimitRegularityFacts inside the relativity fixtures module. It would be cited by any downstream relativity derivation that needs a placeholder for limit regularity until a constructive proof replaces the stub. The body constructs the instance by feeding g, ψ, vol into a pair of trivial assertions for the zero_nonsingular field.
Claim. Define a noncomputable instance of the general relativity limit regularity facts such that, for any metric $g$, field $ψ$, and volume $vol$, the zero-nonsingular condition holds by triviality.
background
The module supplies stub instances for hypothesis classes that replace sorries in relativity arguments. These stubs sit outside production namespaces so the trust boundary remains explicit. GRLimitRegularityFacts is the structure that packages regularity statements for the general relativity limit, here instantiated only with the zero_nonsingular property.
proof idea
One-line wrapper that applies the trivial tactic twice: the intro g ψ vol line is followed by exact ⟨by trivial, by intro x; trivial⟩ to populate the zero_nonsingular field.
why it matters
The stub closes a temporary gap in the relativity fixture layer so that the rest of the Recognition Science derivation chain can continue without unresolved sorries. It belongs to the same family as gaugeFactsStub and curvatureFactsStub and will be discharged once a full regularity theorem from the forcing chain (T5–T8) is available.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.