gaugeFactsStub
plain-language theorem explainer
This declaration supplies a concrete stub instance of the GaugeConstructionFacts structure for use in relativity fixtures. Auditors of the Recognition Science codebase would cite it when confirming that Newtonian gauge constructions can be realized without unresolved sorries. The definition proceeds by direct construction of the zero gauge vector together with repeated simplification under the Newtonian gauge and gauge_transform rules.
Claim. Define a noncomputable stub realization of the gauge-construction facts structure in which the gauge vector for Newtonian conditions is identically zero, the spatial-trace freedom holds by direct substitution, Newtonian gauge existence is witnessed by the zero vector, matching to the Newtonian gauge is verified by norm_num and simplification, the Riemann tensor remains gauge-invariant under linearised transformations, and the test construction for the Newtonian gauge reduces by simplification.
background
The module supplies fixture instances for hypothesis classes that replace sorries while remaining outside production namespaces. GaugeConstructionFacts is the structure that packages the required properties of gauge transformations in the Newtonian limit: find_gauge_vector_for_newtonian, spatial_trace_freedom, newtonian_gauge_exists, matched_to_newtonian_gauge, gauge_invariant_riemann and test_newtonian_gauge_construction. No upstream lemmas are imported; the stub relies only on the gauge_transform and InNewtonianGauge predicates already present in the surrounding relativity development.
proof idea
Each field of the structure is defined by an intro tactic followed by exact construction of the zero gauge vector and a simp call on the gauge_transform and InNewtonianGauge lemmas. The matched_to_newtonian_gauge field additionally uses norm_num and le_rfl to discharge the ordering constraints. The final instance declaration simply registers the stub as the canonical GaugeConstructionFacts.
why it matters
The stub closes the GaugeConstructionFacts interface so that downstream relativity fixtures (curvatureFactsStub, linearizedPDEStub, weakFieldAlgebraStub) can proceed without open sorries. It directly supports the transition from Newtonian to weak-field relativistic descriptions inside the Recognition Science framework, consistent with the eight-tick octave and the phi-ladder mass formulas. The placement outside production namespaces keeps the trust boundary explicit for any future replacement by a non-stub theorem.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.