Constants Kdisplay

The K display bridge

In physics, a measurement is only meaningful relative to a unit. Change the unit, and the number changes. Recognition Science is a framework that begins from a discrete record of events, called a ledger, and it has a way of writing down its basic quantities so that this unit dependence becomes a feature, not a nuisance. The module KDisplay defines the bridge: a dimensionless ratio, called K, that compares a time interval to a length interval in a way that survives any rescaling of the units.

The core object is a set of units, written RSUnits, that carries a time scale tau0, a length scale ell0, and a speed c with the relation ell0 = c * tau0. Two unit systems are equivalent if they share the same speed and one is just a rescaling of the other by a nonzero factor. The module proves that the display ratio, the quotient of a displayed kinetic length by a displayed recognition time, equals the speed c exactly. That is the null condition: the ratio squared equals c squared, which is the statement that the display speed is the speed of light in the framework's own units.

The important theorem is that K itself is invariant under rescaling. If you multiply both tau0 and ell0 by the same nonzero factor, the ratio tau_rec_display / tau0 does not change. The proof is short and the statement is exact: the quotient factors through the equivalence relation on units. A second theorem, observable_factors_through_quotient, states the general principle: any observable that respects rescaling takes the same value on equivalent unit systems. That is the mathematical content of the phrase "unit independent".

The module also includes a measurement protocol. A K gate measurement records two estimates of K, one from a time measurement and one from a length measurement, and validates them if they agree within a tolerance derived from error propagation. The tolerance is the combined uncertainty: K times the square root of the sum of the squared relative errors. A falsifier, falsifier_K_gate_mismatch, is defined as the negation of that validation. This turns the unit invariance into a testable prediction: if the two estimates disagree beyond tolerance, the framework's claim is falsified.

What this establishes in plain language is that the framework's basic quantities are not arbitrary. The ratio K is a genuine invariant, the same number regardless of how you scale your units, and the speed that appears in the display is exactly the framework's c. The module does not derive the value of c; it proves the structural fact that the display is consistent and unit independent. The practical consequence is that any experiment that measures K from time and from length must agree, and the tolerance for that agreement is computable from the measurement errors.

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τ

/-- K-gate is independent of units rescaling -/
theorem K_gate_units_invariant (U : RSUnits) (α : ℝ) (hα : 0 < α) (hτ : 0 < U.tau0) :
  let U' : RSUnits := { tau0 := α * U.tau0, ell0 := α * U.ell0, c := U.c,
                        c_ell0_tau0 := by calc U.c * (α * U.tau0) = α * (U.c * U.tau0) := by ring
                                              _ = α * U.ell0 := by rw [U.c_ell0_tau0] }
  (tau_rec_display U') / U'.tau0 = (tau_rec_display U) / U.tau0 := by
  intro U'
  have hα' : α ≠ 0 := ne_of_gt hα
  have hτ' : U.tau0 ≠ 0 := ne_of_gt hτ
  rw [tau_rec_display_ratio U hτ', tau_rec_display_ratio U' (mul_ne_zero hα' hτ')]

/-- Observable displays factor through units quotient (sketch) -/
theorem observable_factors_through_quotient (O : RSUnits → ℝ)
    (hQuot : ∀ U α, α ≠ 0 → O {tau0 := α * U.tau0, ell0 := α * U.ell0, c := U.c,
                               c_ell0_tau0 := by calc U.c * (α * U.tau0) = α * (U.c * U.tau0) := by ring
                                                     _ = α * U.ell0 := by rw [U.c_ell0_tau0]} = O U) :
    ∀ U1 U2, UnitsEquivalent U1 U2 → O U1 = O U2 := by
  intro U1 U2 h
  obtain ⟨hc, α, hα, hτ, hℓ⟩ := h
  -- U2 = scaled version of U1
  have h1 := hQuot U1 α hα
  -- Need to show the scaled U1 equals U2
  have hU2_eq : U2 = {tau0 := α * U1.tau0, ell0 := α * U1.ell0, c := U1.c,
                       c_ell0_tau0 := by calc U1.c * (α * U1.tau0) = α * (U1.c * U1.tau0) := by ring
                                             _ = α * U1.ell0 := by rw [U1.c_ell0_tau0]} := by
    cases U2
    simp only [RSUnits.mk.injEq]
    exact ⟨hτ, hℓ, hc.symm⟩
  rw [hU2_eq]
  exact h1.symm

/-- Falsifier: K-gate mismatch beyond tolerance -/
noncomputable def falsifier_K_gate_mismatch (meas : KGateMeasurement) : Prop :=
  ¬validateKGate meas

What this page does not claim

This module does not derive the numerical value of the speed c. This module does not prove that the K gate measurement protocol is physically realizable. This module does not establish that the framework's units match any particular conventional unit system.

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: