solution_exists
The theorem proves that for any rotation system S, valid ILG parameters P, positive tick duration tau0, radius r and enclosed mass, a positive velocity v exists satisfying the ILG rotation fixed-point equation. Galactic dynamics modelers working inside Recognition Science cite it to guarantee solution existence before fitting observed rotation curves. The proof applies the intermediate value theorem to an auxiliary function f(v) = v^2 - w_t(P, 2 pi r / v, tau0) * K after verifying continuity on (0, inf) and a sign change.
claimLet $S$ be a rotation system, $P$ a set of ILG parameters obeying the parameter properties, and let $r>0$, $M>0$ be radius and enclosed mass with $0<tau_0$. Then there exists $v>0$ such that $v$ satisfies the ILG rotation-velocity fixed-point condition.
background
The RotationILG module augments Newtonian gravity with the ILG weight function w_t derived from the Recognition Composition Law. w_t(P, T, tau0) = 1 + P.Clag * ((max(eps_t, T/tau0))^alpha - 1), where tau0 is the fundamental tick duration supplied by Compat.Constants.tau0 and K is the dimensionless bridge ratio phi^{1/2} from Constants.K. Upstream CostAlgebra.comp supplies the multiplicative J-automorphism composition that justifies the algebraic properties of w_t used in the continuity argument. The local setting is galactic rotation curves, with supporting structure from ClassicalBridge.Fluids.CPM2D.model and Astrophysics.NucleosynthesisTiers.of.
proof idea
The proof defines K = S.G * S.Menc(r)/r > 0 and the auxiliary f(v) = v^2 - ILG.w_t(P, 2 pi r / v, tau0) * K. Continuity of f on (0, inf) follows by composing the continuous w_t with the continuous map v |-> 2 pi r / v. A small positive v_try is exhibited where f(v_try) < 0 by using w_t >= 1 together with v_try^2 <= K/2. The remaining steps locate a large v where f(v) > 0 and invoke the intermediate value theorem.
why it matters in Recognition Science
This existence result is invoked by Relativity.Compact.StaticSpherical.solution_exists to construct stationary Schwarzschild sections and by Relativity.NewFixtures.linearizedPDEStub to close the linearized PDE facts. It supplies the rotation-curve existence step required by the gravity sector of the framework, consistent with the eight-tick octave and D = 3. The theorem is fully proved with no remaining scaffolding.
scope and limits
- Does not prove uniqueness of the velocity solution.
- Does not supply an explicit closed-form expression for v.
- Does not address dynamical stability under small perturbations.
- Does not extend the existence claim to non-spherical or time-dependent mass distributions.
formal statement (Lean)
36theorem solution_exists (S : RotSys) (P : ILG.Params) (HP : ParamProps P) (tau0 : ℝ) (htau : 0 < tau0)
37 (r : ℝ) (hr : 0 < r) (hM : 0 < S.Menc r) :
38 ∃ v : ℝ, v > 0 ∧ is_ilg_vrot S P tau0 r v := by
proof body
Tactic-mode proof.
39 -- We use the Intermediate Value Theorem on the function f(v) = v^2 - w_t(r,v) * K
40 -- where K = G * Menc / r > 0.
41 let K := S.G * S.Menc r / r
42 have hK : 0 < K := by
43 apply div_pos
44 · exact mul_pos S.posG hM
45 · exact hr
46
47 let f : ℝ → ℝ := fun v => v^2 - ILG.w_t P (2 * Real.pi * r / v) tau0 * K
48
49 -- 1. Continuity of f on (0, inf)
50 have h_cont : ContinuousOn f (Set.Ioi 0) := by
51 apply ContinuousOn.sub
52 · exact continuousOn_pow 2
53 · apply ContinuousOn.mul
54 · -- w_t is continuous. w_t(T, tau0) = 1 + Clag * ((max eps_t (T/tau0))^alpha - 1)
55 -- T(v) = 2*pi*r / v is continuous on (0, inf)
56 have hT : ContinuousOn (fun v => 2 * Real.pi * r / v) (Set.Ioi 0) := by
57 apply ContinuousOn.div
58 · exact continuousOn_const
59 · exact continuousOn_id
60 · intro v hv; exact ne_of_gt hv
61
62 -- Now compose with w_t
63 -- w_t_with defaultConfig P T tau0
64 -- = 1 + P.Clag * (Real.rpow (max defaultConfig.eps_t (T / tau0)) P.alpha - 1)
65 refine ContinuousOn.comp (f := fun T => ILG.w_t P T tau0) (g := fun v => 2 * Real.pi * r / v) ?_ hT (Set.mapsTo_image _ _)
66
67 -- w_t is continuous everywhere
68 apply Continuous.continuousOn
69 unfold ILG.w_t ILG.w_t_with
70 refine continuous_const.add ?_
71 apply Continuous.mul continuous_const
72 refine Continuous.sub ?_ continuous_const
73
74 -- rpow is continuous for positive base
75 -- base is max eps_t (T/tau0) >= eps_t = 0.01 > 0
76 apply Continuous.rpow
77 · refine continuous_max continuous_const ?_
78 exact continuous_id.div_const _
79 · exact continuous_const
80 · intro T; apply lt_max_of_lt_left; norm_num
81 · exact continuousOn_const
82
83 -- 2. Existence of v_small such that f(v_small) < 0
84 have hf_small_exists : ∃ v_small, 0 < v_small ∧ f v_small < 0 := by
85 let v_bound := 2 * Real.pi * r / tau0
86 let v_try := min (Real.sqrt (K / 2)) v_bound
87 have hv_pos : 0 < v_try := by
88 apply lt_min
89 · exact Real.sqrt_pos.mpr (half_pos hK)
90 · apply div_pos
91 · exact mul_pos (mul_pos (by norm_num) Real.pi_pos) hr
92 · exact htau
93 use v_try
94 constructor
95 · exact hv_pos
96 · have h_wt_ge_one : 1 ≤ ILG.w_t P (2 * Real.pi * r / v_try) tau0 := by
97 apply ILG.w_t_ge_one P HP (2 * Real.pi * r / v_try) tau0 htau
98 -- T >= tau0 <=> 2pi*r/v >= tau0 <=> 2pi*r/tau0 >= v
99 rw [ge_iff_le]
100 exact min_le_right _ _
101
102 unfold f
103 -- f(v) = v^2 - w_t * K
104 -- Since w_t >= 1, f(v) <= v^2 - K
105 -- v^2 <= (sqrt(K/2))^2 = K/2
106 have hv_sq : v_try^2 ≤ K / 2 := by
107 have : v_try ≤ Real.sqrt (K / 2) := min_le_left _ _
108 exact sq_le_sq_of_nonneg (le_of_lt (Real.sqrt_pos.mpr (half_pos hK))) this
109
110 have hfk : f v_try ≤ v_try^2 - K := by
111 simp only [f, sub_le_sub_iff_left]
112 exact (le_mul_iff_one_le_left hK).mpr h_wt_ge_one
113
114 calc f v_try ≤ v_try^2 - K := hfk
115 _ ≤ K / 2 - K := sub_le_sub_right hv_sq K
116 _ = -K / 2 := by ring
117 _ < 0 := by linarith
118
119-- ... 75 more lines elided ...