X_var
plain-language theorem explainer
X_var defines the dimensionless ratio X = k τ₀ / a that parametrizes observables in the ILG reciprocity setting. Researchers deriving growth factors or backreaction relations cite this when reducing dependence on separate scale and wave-number parameters to a single variable. The definition is a direct algebraic expression using the fundamental tick duration τ₀ with no lemmas or reductions required.
Claim. The dimensionless variable is defined by $X(k, a, τ_0) := k τ_0 / a$.
background
τ₀ denotes the fundamental tick duration, the basic time unit in RS-native units where c = 1, as supplied by Constants.tau0 and its derivation from ħ, G, and π. The ILG.Reciprocity module imports this constant together with the active edge count A from IntegrationGap to support reciprocity constructions. The LedgerForcing.reciprocity theorem establishes that event cost equals the cost of the reciprocal event via J-symmetry.
proof idea
The declaration is a direct definition. It evaluates the ratio of the product k τ₀ to the scale factor a with no tactic steps or upstream lemma applications.
why it matters
X_var supplies the argument for HasXReciprocity and the derivative identities x_reciprocity_identity and x_reciprocity_log_identity in the same module. It is invoked by growth_x_reciprocity to prove the scale-time derivative relation for the growth factor. This definition implements the reduction to a single variable X that follows from the reciprocity principle and enables the transition between modified and GR regimes.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.