linearizedPDEStub
This definition supplies a concrete stub instance for LinearizedPDEFacts in the relativity fixtures module. It asserts existence of a trivial zero-perturbation solution to the linearized equation together with an explicit O(ε) remainder bound. Researchers developing weak-field approximations would cite the stub to keep proofs moving while the full derivation from the Recognition action remains open. The construction is a direct term-mode record build that applies norm_num and simp to discharge the required properties.
claimDefine a noncomputable stub instance of the facts class for linearized partial differential equations that, for any gauge ng, density ρ and mass-squared parameter, returns a solution record with vanishing perturbation field δψ satisfying the linearized equation to first order and supplies a remainder function bounded by |ε|.
background
The module supplies stub instances for hypothesis classes that replace sorries during development; these live outside production namespaces to keep the trust boundary explicit. LinearizedPDEFacts is the structure containing solution_exists (which must produce a record with δψ, smallness proof and equation satisfaction) and remainder_order (which must produce an order-ε bound with the appropriate norm and multiplication properties). The two upstream solution_exists theorems establish existence of rotation-velocity solutions in the ILG fixed-point equation and of static spherical metrics via the Schwarzschild section, providing the pattern this stub emulates in the linearized setting.
proof idea
The definition is a direct term-mode construction of the LinearizedPDEFacts record. For solution_exists it introduces the parameters, refines a record with constant-zero δψ, discharges smallness by norm_num, verifies the equation by simp on Linearized00Equation, and supplies a trivial gauge record. For remainder_order it builds a function returning |ε|, proves the order properties by norm_num and simp on IsOrderEpsilonSquared and abs_mul, then registers the whole object as the typeclass instance.
why it matters in Recognition Science
The stub closes a temporary gap that would otherwise block weak-field calculations in the Recognition framework while the full linearized PDE is derived from the action. It mirrors the existence pattern already proved for ILG rotation and static spherical solutions, allowing downstream relativity lemmas to proceed without sorries. Because the used_by count is currently zero, the declaration functions as a placeholder whose replacement by a derived theorem would complete the bridge from the Recognition Composition Law to the weak-field limit.
scope and limits
- Does not derive the linearized PDE from the Recognition Science action.
- Does not produce non-trivial solutions or numerical field profiles.
- Does not incorporate boundary conditions or gauge fixing beyond the trivial case.
- Does not address higher-order terms or back-reaction on the metric.
formal statement (Lean)
61noncomputable def linearizedPDEStub : LinearizedPDEFacts where
62 solution_exists := by
proof body
Definition body.
63 intro ng ρ m_squared
64 refine ⟨{ δψ := fun _ => 0, small := by intro _ _; norm_num }, ?_, ?_⟩
65 · intro x; simp [Linearized00Equation]
66 · refine ⟨⟨fun _ => 1, by intro; simp⟩, fun _ => rfl, rfl⟩
67 remainder_order := by
68 intro ng δψ ρ ε
69 refine ⟨fun _ => |ε|, ?_, ?_⟩
70 · intro; exact ⟨by norm_num, by intro; norm_num⟩
71 · intro x; simp [IsOrderEpsilonSquared, abs_mul]
72
73instance : LinearizedPDEFacts := linearizedPDEStub
74