Constants Kdisplay Displays Invariant Under Equivalence

The unit-free display

In physics, a measurement is only trustworthy if it does not depend on the units you happen to use. The Recognition Science framework encodes this idea in a machine-checked theorem called displays_invariant_under_equivalence. It states that if two unit systems are equivalent, meaning they differ only by a common rescaling of their base length and time units, then the ratio of the displayed recognition time to the base time unit is identical in both systems. In plain terms: change the ruler and the clock by the same factor, and the dimensionless number that the framework calls the display, the value shown by its measurement protocol, does not change.

This is a theorem, not a definition or a hope. The framework's library, a machine-checked collection of formal theorems, proves it from the definition of unit equivalence and the structure of the display functions. The proof is short: it shows that the display ratio is a pure number, built from the base units in such a way that a common rescaling cancels out. The theorem also covers the speed of light: the same ratio, squared, equals the framework's constant c, and that equality is invariant under the same rescaling. The result is one of a family of invariance theorems, including the symmetry, transitivity, and reflexivity of unit equivalence, which together guarantee that any observable defined through the quotient of unit systems is well-defined.

What the theorem does not claim is just as important. It does not say that any particular measurement is correct, or that the framework's constants match experiment. It only says that the display ratio is a well-defined function of the unit system, not of the arbitrary choice of scale. It also does not claim that the display ratio is invariant under a change that alters the speed of light c, or that rescales only one of the two base units. The theorem's scope is precisely the common rescaling of length and time, with c held fixed. A separate, unformalized protocol in the same file, the K-gate measurement, uses a tolerance based on error propagation, but its validation is a definition, not a proved theorem.

The practical consequence is that the framework's displays are genuine observables. A reader who sees a display value in one unit system can be confident it would be the same in any equivalent system, which is the minimum requirement for a number to be a property of the world rather than of the measuring apparatus. This invariance is what lets the framework talk about a single, unit-free recognition rate, and it is the foundation on which any comparison to measured physical constants must rest.

/-- Displays are invariant under units equivalence -/
theorem displays_invariant_under_equivalence {U1 U2 : RSUnits}
    (h : UnitsEquivalent U1 U2) (hτ1 : U1.tau0 ≠ 0) (hℓ1 : U1.ell0 ≠ 0) :
    (tau_rec_display U1) / U1.tau0 = (tau_rec_display U2) / U2.tau0 := by
  obtain ⟨_, α, hα, hτ2, _⟩ := h
  have hτ2' : U2.tau0 ≠ 0 := by simp [hτ2, hα, hτ1]
  rw [tau_rec_display_ratio U1 hτ1, tau_rec_display_ratio U2 hτ2']

/-- Display-level Lorentz structure: (λ/τ)² - c² = 0 (null) -/
theorem display_null_condition (U : RSUnits) (h : 0 < U.tau0) :
  ((lambda_kin_display U) / (tau_rec_display U))^2 = U.c^2 := by
  simp only [display_speed_eq_c 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α']

/-- Units equivalence class: two units packs are equivalent if they have same c -/
def UnitsEquivalent (U1 U2 : RSUnits) : Prop :=
  U1.c = U2.c ∧ ∃ α : ℝ, α ≠ 0 ∧ U2.tau0 = α * U1.tau0 ∧ U2.ell0 = α * U1.ell0

What this page does not claim

The theorem does not prove that any particular display value matches a measured physical constant. The theorem does not claim invariance under a rescaling that changes the speed of light c. The theorem does not validate the K-gate measurement protocol, which is defined by a tolerance, not proved.

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: