grLimitRegularityStub
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.
claimDefine 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 in Recognition Science
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.
scope and limits
- Does not derive any nontrivial regularity estimate from the J-cost or phi-ladder.
- Does not connect the metric g to the eight-tick octave or spatial dimension D=3.
- Does not replace the stub with a theorem that would satisfy a referee.
- Does not interact with the Recognition Composition Law or Berry threshold.
formal statement (Lean)
169noncomputable def grLimitRegularityStub : GRLimitRegularityFacts where
170 zero_nonsingular := by
proof body
Definition body.
171 intro g ψ vol
172 exact ⟨by trivial, by intro x; trivial⟩
173
174instance : GRLimitRegularityFacts := grLimitRegularityStub