K_gate_units_invariant
plain-language theorem explainer
The theorem shows that the ratio of the recognition display function to the fundamental time unit remains unchanged when time and length units are scaled by a positive factor while speed is held fixed. Researchers deriving unit-independent constants in Recognition Science would cite this to confirm that the K-gate yields a true dimensionless quantity. The proof constructs the rescaled unit structure, verifies the light-cone constraint by algebraic simplification, and reduces both sides to the known ratio formula.
Claim. Let $U$ be an RS unit system with fundamental time $τ_0 > 0$, length $ℓ_0$, and speed $c$ satisfying $c τ_0 = ℓ_0$. For any $α > 0$, define the rescaled system $U'$ by $τ_0' = α τ_0$, $ℓ_0' = α ℓ_0$, and $c' = c$. Then the ratio of the recognition display function to the time unit is invariant: $τ_{rec}(U') / τ_0' = τ_{rec}(U) / τ_0$.
background
The RSUnits structure packages the minimal constants needed for the framework: fundamental tick duration $τ_0$, voxel length $ℓ_0$, and speed $c$, together with the light-cone identity $c τ_0 = ℓ_0$. The module establishes display equalities that render the dimensionless bridge ratio $K = φ^{1/2}$ independent of unit choice. Upstream lemmas supply the definition of $τ_0$ as the base tick, the identity $ℓ_0 = c τ_0$, and the ratio formula for the recognition display function.
proof idea
The tactic proof first builds the rescaled structure $U'$ explicitly and confirms its light-cone constraint via ring simplification followed by rewriting with the original identity. It then invokes the ratio lemma on both the original and rescaled units, using the supplied positivity hypotheses to obtain the required non-zero conditions for division.
why it matters
The result establishes units invariance for the K-gate, ensuring the derived dimensionless ratio is a genuine constant rather than an artifact of unit selection. It supports the module's goal of producing display equalities that feed into the broader constants derivation and aligns with the framework's emphasis on unit-independent quantities derived from the forcing chain. No downstream theorems are yet recorded, leaving its precise placement in the constants pipeline open for later use.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.