HasXReciprocity
plain-language theorem explainer
HasXReciprocity defines the property that a function Q(a,k) depends only on the single dimensionless ratio X = k tau0 / a. ILG modelers cite it to collapse two-variable expressions into functions of one scaled argument. The definition is an existential statement that introduces a reduced function Q_tilde and requires equality after substitution of the ratio.
Claim. A function $Q:ℝ→ℝ→ℝ$ satisfies X-reciprocity for fixed $τ_0$ when there exists a function $Q̃:ℝ→ℝ$ such that $Q(a,k)=Q̃(k τ_0/a)$ holds for all real $a,k$.
background
The ILG module centers on the dimensionless variable X = k τ₀ / a, with τ₀ the fundamental tick duration taken from Constants. X_var implements this ratio as (k * τ₀) / a. Upstream results supply the reciprocity theorem from LedgerForcing, which states that the cost of an event equals the cost of its reciprocal, together with multiple definitions of τ₀ as the base time unit in RS-native units.
proof idea
This is a direct definition. It asserts existence of a reduced function Q_tilde such that Q equals Q_tilde composed with the X_var ratio for every pair (a,k). No lemmas or tactics are invoked; the body is the plain existential quantification.
why it matters
The definition supplies the functional form underlying the X-reciprocity identity, whose derivative version reads a ∂Q/∂a = -k ∂Q/∂k. It aligns with the reciprocity principle established in LedgerForcing and supports reduction of ILG quantities to the single scaled variable X. No downstream theorems are recorded, leaving its use in concrete ILG derivations open.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.