X_var
plain-language theorem explainer
X_var defines the dimensionless ILG variable X = k τ₀ / a that marks the transition from modified-gravity to GR regimes in backreaction calculations. Cosmologists working on ILG growth factors and lensing would cite this definition when establishing reciprocity between scale and time derivatives. The definition is a direct algebraic assignment with no computation or lemmas required.
Claim. Define the dimensionless variable by $X(k, τ_0, a) = k τ_0 / a$, where $τ_0$ is the fundamental tick duration, $k$ is wavenumber, and $a$ is scale factor. This $X$ controls the shift between small-$X$ modified regimes and large-$X$ GR recovery.
background
The module formalizes Buchert backreaction and X-reciprocity results from the ILG source-side kernel tests paper. tau0 is the fundamental time unit (duration of one tick) in RS-native units, appearing in multiple constant derivations as sqrt(hbar_codata * G_codata / (π c_codata³)) / c_codata. Upstream reciprocity from LedgerForcing states that event cost equals reciprocal-event cost via J-symmetry. The local setting introduces X to audit backreaction while preserving the potential-flow character of ILG modifications.
proof idea
Direct definition: the body is the single algebraic expression k * tau0 / a. No tactics or lemmas are applied; the declaration simply names the combination that appears in all downstream X-reciprocity statements.
why it matters
X_var supplies the scaling argument for HasXReciprocity and the derivative identities x_reciprocity_identity and x_reciprocity_log_identity in ILG.Reciprocity. These identities feed growth_x_reciprocity in the GrowthODE module, which proves the target-C growth-factor relation. The definition therefore closes the loop between the ledger reciprocity theorem and the eight-tick octave scaling used in backreaction audits; it touches the open question of whether ILG backreaction remains zero once higher-order phi-ladder corrections are restored.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.