units_quotient_preserves_K
The theorem shows that the dimensionless K-gate ratio equals tau_rec_display(U) divided by U.tau0 for any RSUnits structure with nonzero fundamental units, and remains unchanged under uniform rescaling by nonzero alpha. Researchers verifying scale invariance of derived constants in Recognition Science would cite it when confirming unit-independent quantities. The proof is a one-line wrapper applying the tau_rec_display_ratio lemma after introducing the scaling parameter.
claimLet $U$ be an RSUnits structure with nonzero fundamental time unit $U.τ_0$ and length unit $U.ℓ_0$. For any nonzero real scalar $α$, the ratio of the recursive display time quantity for $U$ to $U.τ_0$ equals the K-gate ratio.
background
The module centers on dimensionless bridge ratios K and associated display equalities that connect fundamental units to observable quantities without dimensional dependence. The RSUnits structure packages the minimal data: fundamental tick duration τ₀, voxel length ℓ₀, and speed c satisfying the relation c τ₀ = ℓ₀. Upstream results supply the concrete definitions of tau0 as the tick duration (from tick) and ell0 as the fundamental length (from c_codata * tau0), together with the K_gate_ratio and K_gate_eqK lemmas from KDisplayCore that encode the invariant ratio and the equality between display routes.
proof idea
The proof is a one-line wrapper: introduce the scaling parameter α (discarding its nonzeroness hypothesis) and apply the lemma tau_rec_display_ratio directly to U and the nonzeroness of τ₀.
why it matters in Recognition Science
This declaration establishes functoriality of the K-gate under units transformations, confirming that the dimensionless bridge ratio K is preserved when the base units τ₀ and ℓ₀ are rescaled together. It supports the framework goal of unit-independent constants (aligning with the derivation of ell0 and tau0 from ħ, G, and c) and closes a potential invariance gap for K-display quantities, even though no immediate downstream theorems are listed.
scope and limits
- Does not compute or bound the numerical value of K_gate_ratio.
- Does not address cases where τ₀ or ℓ₀ vanishes.
- Does not treat non-uniform or nonlinear transformations of the units.
- Does not derive the ratio equality from the Recognition Composition Law or forcing chain.
formal statement (Lean)
64theorem units_quotient_preserves_K (U : RSUnits) (hτ : U.tau0 ≠ 0) (hℓ : U.ell0 ≠ 0) :
65 ∀ (α : ℝ), α ≠ 0 →
66 -- Under rescaling (τ0, ℓ0) → (α·τ0, α·ℓ0), K_gate_ratio remains invariant
67 (tau_rec_display U) / U.tau0 = K_gate_ratio := by
proof body
Term-mode proof.
68 intro α _hα
69 exact tau_rec_display_ratio U hτ
70
71/-- Single-inequality audit: checking one route inequality suffices (routes equal).
72
73 Since `(tau_rec_display U)/τ0 = (lambda_kin_display U)/ℓ0` by `K_gate_eqK`,
74 the inequality direction is immediate. -/