Constants Kdisplay Display Rate Matches Structural Rate

The display rate identity

The Recognition Science framework models physical reality as a ledger, a discrete record of recognition events. In this account, a system's units of length and time are not arbitrary; they are tied to a fundamental constant, the speed of light, through the relation ell0 = tau0 times c. The framework's machine-checked library of formal theorems proves a statement called display_rate_matches_structural_rate. In plain language, it says that the ratio of a displayed kinetic wavelength to a displayed recognition time equals the ratio of the structural length unit to the structural time unit. This is not an approximation; it is an exact equality that holds for any valid choice of units in the framework.

The theorem is a consequence of how the framework defines its display quantities. The displayed recognition time is built from the structural time unit and the golden ratio, while the displayed kinetic wavelength is defined as the speed of light times that displayed time. Because the structural length unit is itself the speed of light times the structural time unit, the two ratios collapse to the same value. The proof is a short chain of algebraic rewrites, all checked by the machine. The identity also survives rescaling: if you multiply both the structural time and length units by the same positive factor, the display ratio does not change. This scale invariance is itself a proved theorem in the same file.

What the declaration does not claim is just as important. It does not assert that any particular measured value of a wavelength or a time matches a prediction. It is a statement about the internal consistency of the framework's definitions, not an empirical check. The theorem also does not say that the display rate equals the speed of light; that separate result, called display_speed_eq_c, is proved elsewhere and requires the structural time unit to be positive. The identity here is more basic: it connects two ways of forming a ratio and shows they agree.

/-- Display derivatives (for rate transformations) -/
theorem display_rate_matches_structural_rate (U : RSUnits) :
  (lambda_kin_display U) / (tau_rec_display U) = U.ell0 / U.tau0 := by
  -- λ_kin / τ_rec = (2π·ℓ₀/(8 log φ)) / (2π·τ₀/(8 log φ)) = ℓ₀/τ₀
  simp only [lambda_kin_display, tau_rec_display]
  have hlog : 0 < Real.log phi := Real.log_pos one_lt_phi
  have h8log : 8 * Real.log phi ≠ 0 := by linarith
  have hpi : 2 * Real.pi ≠ 0 := by linarith [Real.pi_pos]
  have h2pi_ell : 2 * Real.pi * U.ell0 / (8 * Real.log phi) =
                  U.ell0 * (2 * Real.pi / (8 * Real.log phi)) := by ring
  have h2pi_tau : 2 * Real.pi * U.tau0 / (8 * Real.log phi) =
                  U.tau0 * (2 * Real.pi / (8 * Real.log phi)) := by ring
  rw [h2pi_ell, h2pi_tau]
  have h_factor : 2 * Real.pi / (8 * Real.log phi) ≠ 0 := by
    apply div_ne_zero hpi h8log
  rw [mul_div_mul_right _ _ h_factor]

/-- 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α']

/-- Display speed equals structural speed: (λ_kin/τ_rec) = c. -/
lemma display_speed_eq_c_of_nonzero (U : RSUnits)
  (hτ : tau_rec_display U ≠ 0) : (lambda_kin_display U) / (tau_rec_display U) = U.c := by
  have h := lambda_kin_from_tau_rec U
  calc
    (lambda_kin_display U) / (tau_rec_display U)
        = (U.c * tau_rec_display U) / (tau_rec_display U) := by rw [h]
    _   = U.c * (tau_rec_display U / tau_rec_display U) := by rw [mul_div_assoc]
    _   = U.c * 1 := by rw [div_self hτ]
    _   = U.c := by rw [mul_one]

What this page does not claim

The theorem does not assert that any measured wavelength or time matches a predicted value. The display rate is not claimed to equal the speed of light in this declaration; that is a separate result with its own conditions. The identity does not by itself establish that the framework's units correspond to physical units.

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: