HasXReciprocity
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.
claimA 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 in Recognition Science
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.
scope and limits
- Does not derive the differential form a ∂Q/∂a = -k ∂Q/∂k.
- Does not restrict the domain of Q beyond real numbers.
- Does not identify Q with any concrete physical density or flux.
- Does not invoke the phi-ladder or J-cost structure.
formal statement (Lean)
14def HasXReciprocity (Q : ℝ → ℝ → ℝ) (tau0 : ℝ) : Prop :=
proof body
Definition body.
15 ∃ Q_tilde : ℝ → ℝ, ∀ a k, Q a k = Q_tilde (X_var k a tau0)
16
17/-- The X-reciprocity identity: if Q depends only on X = k*tau0/a,
18 then a * ∂Q/∂a = - k * ∂Q/∂k.
19
20 This is the derivative form of ∂lnQ/∂lna = -∂lnQ/∂lnk. -/