w_t_formula_grounded
ILG time-kernel derivation fixes w_t using recognition lag phi to the minus five and alpha equal to (1 minus phi inverse) over two. Galaxy dynamics modelers cite it to obtain the correction term that produces flat rotation curves. The proof is a direct simplification after introducing the two parameter hypotheses.
claimAssuming the recognition lag equals $C_{lag} = varphi^{-5}$ and the fine-structure exponent equals $alpha = (1 - varphi^{-1})/2$, the time kernel satisfies $w_t(T_{dyn}, tau_0) = 1 + varphi^{-5} bigl( max(epsilon_t, T_{dyn}/tau_0)^alpha - 1 bigr)$.
background
In the ILG framework the time kernel w_t modifies the gravitational potential at large scales to account for recognition lags. The recognition lag C_lag is defined as varphi^{-5}, where varphi is the golden ratio fixed point. The fine-structure exponent alpha is set to (1 - varphi^{-1})/2, consistent with the alpha band in Recognition Science. This theorem sits in the Gravity.ILGDerivation module, which derives the ILG correction from the RRF gradient cost. Upstream results include the definition of the constant path in PathSpace and the structure of nuclear densities in NucleosynthesisTiers, though the proof relies only on unfolding w_t and w_t_with. The local setting connects the J-cost from PhiForcingDerived to effective modified gravity.
proof idea
After introducing the hypotheses on the recognition lag and the fine-structure exponent, the proof applies simplification to the definitions of the time kernel w_t and its auxiliary w_t_with.
why it matters in Recognition Science
This declaration grounds the explicit form of the ILG time-kernel, which is required to derive flat galactic rotation curves in the large-radius limit. It fills the step in the ILG derivation chain that links the recognition lag C_lag = phi^{-5} to the effective potential correction, as described in the theorem comment. The result supports the structural theorem on flat rotation curves by providing the exact power-law divergence that cancels the Newtonian 1/r term. It touches the T5 J-uniqueness and T6 phi fixed point from the forcing chain, and the alpha band.
scope and limits
- Does not derive the value of phi or the lag from first principles.
- Does not address quantum corrections or higher-order terms.
- Does not prove stability of the resulting rotation curves.
- Does not incorporate spatial dimensions or the eight-tick octave directly.
formal statement (Lean)
15theorem w_t_formula_grounded (P : Params) (Tdyn τ0 : ℝ) :
16 P.Clag = phi ^ (-(5 : ℝ)) →
17 P.alpha = (1 - 1/phi) / 2 →
18 w_t P Tdyn τ0
19 = 1 + (phi ^ (-(5 : ℝ)))
20 * (Real.rpow (max defaultConfig.eps_t (Tdyn / τ0)) ((1 - 1/phi) / 2) - 1) := by
proof body
Term-mode proof.
21 intro hClag hAlpha
22 simp [w_t, w_t_with, hClag, hAlpha]
23
24/-- **THEOREM: Flat Rotation Curves (Structural)**
25 In the large-r limit where $T_{dyn} \gg \tau_0$, the ILG correction $w_t$
26 diverges as $(T_{dyn})^\alpha$, exactly canceling the $1/r$ decay of the
27 Newtonian potential and forcing a flat velocity $v_{rot} \approx const$. -/