solution_exists
For any real mass M, static spherical metric functions f and g together with a scalar field psi exist satisfying the asymptotic flatness conditions at infinity. Researchers recovering classical vacuum solutions within the Recognition Science action would cite this result. The proof proceeds by direct construction of the Schwarzschild metric with vanishing scalar field, followed by separate epsilon-delta arguments that bound the deviations of f and g from unity.
claimFor any real number $M$, there exist functions $f,g : (0,∞) → ℝ$ with $f(r)>0$, $g(r)>0$ for all $r>0$ and a scalar field $ψ : ℝ → ℝ$ such that $|f(r)-1|→0$ and $|g(r)-1|→0$ as $r→∞$.
background
The module treats compact static spherical configurations in the Recognition Science framework. A StaticSphericalMetric is a pair of positive real functions f and g on positive radii that encode the metric components. A StaticScalarField is simply a real-valued function psi on the radial coordinate. BoundaryConditions is the conjunction of two statements: for every ε>0 there exists R such that |f(r)-1|<ε and |g(r)-1|<ε whenever r>R. The construction rests on upstream ledger-factorization and phi-forcing structures that calibrate the underlying J-cost action.
proof idea
The tactic proof instantiates the existential with the explicit SchwarzschildMetric M (f(r)=1-2M/r, g(r)=1/(1-2M/r)) and the zero scalar field. It unfolds BoundaryConditions, splits into the two limit conjuncts, and for each ε>0 supplies an explicit R (linear in |M|/ε) followed by algebraic rewriting, positivity lemmas, and repeated application of div_lt_of_lt_mul together with linarith to close the inequalities.
why it matters in Recognition Science
The declaration supplies the vacuum exterior solution that feeds the rotation-velocity existence theorem in Gravity.RotationILG and the linearized-PDE stub in NewFixtures. It demonstrates that the Recognition Science action admits the classical Schwarzschild geometry as a stationary section outside a mass M, consistent with the forcing-chain recovery of D=3 and the eight-tick octave. No open scaffolding remains inside the module.
scope and limits
- Does not prove uniqueness of the metric for given M.
- Does not construct or match an interior solution.
- Does not incorporate non-vacuum matter sources.
- Does not address linear stability or perturbations.
Lean usage
theorem rotation_use (M : ℝ) : ∃ v, v > 0 ∧ is_ilg_vrot S P tau0 r v := by exact (solution_exists M).1formal statement (Lean)
66theorem solution_exists (M : ℝ) :
67 ∃ (metric : StaticSphericalMetric) (scalar : StaticScalarField),
68 BoundaryConditions metric := by
proof body
Tactic-mode proof.
69 use SchwarzschildMetric M, { psi := fun _ => 0 }
70 unfold BoundaryConditions SchwarzschildMetric
71 constructor
72 · -- Limit of 1 - 2M/r as r -> inf is 1
73 intro ε hε
74 use 2 * |M| / ε + 1
75 intro r hr
76 have : r > 0 := by linarith [abs_nonneg M]
77 simp
78 -- |(1 - 2M/r) - 1| = |2M/r| = 2|M|/r < ε
79 rw [abs_div, abs_of_pos this]
80 apply div_lt_of_lt_mul
81 · linarith
82 · linarith
83 · -- Limit of 1 / (1 - 2M/r) as r -> inf is 1
84 intro ε hε
85 -- Choose R such that 2M/r < 1/2 and (1/(1-x) - 1) < ε
86 use 4 * |M| * (1 + 1/ε) + 1
87 intro r hr
88 have hr_pos : r > 0 := by
89 have : 4 * |M| * (1 + 1/ε) ≥ 0 := by positivity
90 linarith
91 have h_ratio : |2 * M / r| < 1 / 2 := by
92 rw [abs_div, abs_of_pos hr_pos, div_lt_iff hr_pos]
93 have : 4 * |M| * (1 + 1/ε) + 1 > 4 * |M| := by
94 have : 4 * |M| / ε ≥ 0 := by positivity
95 linarith
96 have : r > 4 * |M| := by linarith
97 linarith [abs_of_pos hr_pos]
98
99 simp only [sub_add_cancel, abs_sub_comm]
100 -- |1 / (1 - 2M/r) - 1| = |(2M/r) / (1 - 2M/r)|
101 have h_denom_pos : 1 - 2 * M / r > 1 / 2 := by
102 have : 2 * M / r ≤ |2 * M / r| := le_abs_self _
103 linarith
104
105 have h_eq : 1 / (1 - 2 * M / r) - 1 = (2 * M / r) / (1 - 2 * M / r) := by
106 field_simp [hr_pos.ne', h_denom_pos.ne']
107
108 rw [h_eq, abs_div, abs_of_pos h_denom_pos]
109 apply div_lt_of_lt_mul h_denom_pos
110 -- We want |2M/r| < ε * (1 - 2M/r)
111 -- |2M/r| + ε * (2M/r) < ε
112 -- (2M/r) * (1 + ε) < ε if M > 0
113 -- |2M/r| * (1 + ε) < ε
114 -- 2|M|/r * (1 + ε) < ε
115 -- 2|M|(1 + ε) / ε < r
116 -- 2|M|(1/ε + 1) < r
117 have h_r_bound : r > 2 * |M| * (1 / ε + 1) := by
118 have : 4 * |M| * (1 + 1/ε) + 1 > 2 * |M| * (1 + 1/ε) := by
119 have : 2 * |M| * (1 + 1/ε) + 1 > 0 := by positivity
120 linarith
121 linarith
122
123 rw [abs_div, abs_of_pos hr_pos]
124 have h_goal : 2 * |M| < r * ε * (1 - 2 * M / r) := by
125 have : r * ε * (1 - 2 * M / r) = ε * r - ε * 2 * M := by ring
126 rw [this]
127 -- We need 2|M| < ε*r - 2εM
128 -- 2|M| + 2εM < ε*r
129 -- 2|M|(1+ε) < ε*r
130 -- 2|M|(1+ε)/ε < r
131 -- 2|M|(1/ε + 1) < r
132 have h_M_le : 2 * M ≤ 2 * |M| := by linarith [le_abs_self M]
133 have : ε * 2 * M ≤ ε * 2 * |M| := (mul_le_mul_left hε).mpr h_M_le
134 have : 2 * |M| * (1 + ε) < ε * r := by
135 rw [mul_comm ε r, ← div_lt_iff hε]
136 field_simp [hε.ne']
137 linarith
138 linarith
139 exact h_goal
140