Constants Kdisplay Display Ratio Scale Invariant

Scale invariance of the display ratio

A ratio of two lengths is a dimensionless number: it has no units, so it does not change when you multiply both lengths by the same factor. The declaration display_ratio_scale_invariant proves, inside the Recognition Science framework, that one particular ratio has exactly this property. The ratio is the quotient of a kinematic wavelength and a recognition time, both expressed in display units. The theorem states that if you scale both quantities by any positive real number, the quotient is unchanged. This is a formal statement in the framework's machine-checked library of formal theorems, and it is proved for all positive scale factors.

The statement is a theorem in the framework's library, meaning it is derived from the framework's definitions and axioms, not assumed. The proof is short: it relies on the fact that multiplying both numerator and denominator of a fraction by the same nonzero number leaves the fraction's value alone. The theorem's hypotheses are that the recognition time is positive and that the scale factor is positive. Under those conditions, the equality holds. The framework's library also proves a related statement, that the same ratio equals a constant called the speed of light in the framework's units, and another that the ratio satisfies a null condition, meaning its square equals the square of that constant.

What the theorem does not claim is equally important. It does not claim that the ratio is physically measurable, nor that it is invariant under all transformations, only under uniform scaling of both lengths. It does not claim that the ratio is dimensionless in any absolute sense; it is dimensionless because it is a ratio of two quantities with the same units. The theorem does not establish that the ratio is the fine-structure constant or any other specific physical constant. It is a structural fact about the framework's definitions, not an empirical claim about the world.

The practical upshot is that the framework can use this ratio as a stable quantity when comparing different unit systems. If two unit systems are related by a uniform rescaling of their fundamental length and time units, the ratio is the same in both. This makes the ratio a candidate for an observable quantity within the framework, one that does not depend on the arbitrary choice of units. The theorem is a small but necessary step in that direction: it shows the ratio is well-behaved under the transformations that define unit equivalence.

/-- Displays scale uniformly: ratio is scale-invariant -/
theorem display_ratio_scale_invariant (U : RSUnits) (hτ : 0 < U.tau0) (α : ℝ) (hα : 0 < α) :
  let tau' := α * (tau_rec_display U)
  let lambda' := α * (lambda_kin_display U)
  lambda' / tau' = (lambda_kin_display U) / (tau_rec_display U) := by
  intro tau' lambda'
  have hα' : α ≠ 0 := ne_of_gt hα
  have hτ' : tau_rec_display U ≠ 0 := tau_rec_display_ne_zero U hτ
  simp only [tau', lambda']
  rw [mul_div_mul_left _ _ hα']

lemma display_speed_eq_c (U : RSUnits) (h : 0 < U.tau0) :
  (lambda_kin_display U) / (tau_rec_display U) = RSUnits.c U := by
  have hτ : tau_rec_display U ≠ 0 := tau_rec_display_ne_zero U h
  exact display_speed_eq_c_of_nonzero U hτ

/-- Displays scale uniformly: ratio is scale-invariant -/
theorem display_ratio_scale_invariant (U : RSUnits) (hτ : 0 < U.tau0) (α : ℝ) (hα : 0 < α) :
  let tau' := α * (tau_rec_display U)
  let lambda' := α * (lambda_kin_display U)
  lambda' / tau' = (lambda_kin_display U) / (tau_rec_display U) := by
  intro tau' lambda'
  have hα' : α ≠ 0 := ne_of_gt hα
  have hτ' : tau_rec_display U ≠ 0 := tau_rec_display_ne_zero U hτ
  simp only [tau', lambda']
  rw [mul_div_mul_left _ _ hα']

What this page does not claim

The theorem does not claim the ratio is a physically measurable quantity. The theorem does not claim the ratio is invariant under transformations other than uniform scaling of both lengths. The theorem does not identify the ratio with any specific physical constant such as the fine-structure constant.

Verify this page

Every tagged claim above names its theorem. To check one yourself rather than trust this page, elaborate the source module with Lean 4 and audit its axiom basis:

$ lake env lean IndisputableMonolith/Constants/KDisplay.lean
expected axiom basis: [propext, Classical.choice, Quot.sound] (the Lean kernel's standard three; no RS-specific axioms)

A page whose claims cannot be reproduced this way does not ship. In production, every anchor links to the exact declaration in the public source release, and this block carries the build receipt for the page itself.

Derived articles

This page is generated by a question-recursion engine: the questions its answers raise become the next pages. The current agenda, with open targets marked red: