solution_exists
plain-language theorem explainer
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.
Claim. Let $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
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.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.