Constants Kdisplay Core

The display core

The KDisplayCore module in the Recognition Science framework's machine-checked library of formal theorems defines two display quantities and proves they are locked together. The first, tau_rec_display, is a clock-side display: a time interval built from a base time tau0. The second, lambda_kin_display, is a length-side display: a distance built from a base length ell0. Both take the same form, a base quantity multiplied by a common factor. That factor is K_gate_ratio, equal to pi divided by 4 times the natural logarithm of the golden ratio phi, where phi is the positive solution to r squared equals r plus 1, about 1.618.

The module proves that each display, divided by its base, equals K_gate_ratio. It also proves a kinematic consistency: the framework's speed c times the time display equals the length display. This is not a numerical coincidence; it is a theorem in the library, checked by the kernel. The two lemmas, tau_rec_display_ratio and lambda_kin_display_ratio, establish the ratios, and the theorem K_gate_eqK bundles them into a single statement: both route ratios equal the same constant.

In plain terms, the module says that when the framework displays a recognition cycle on the clock side and a matching distance on the ruler side, the ratio of each display to its base is the same number. That shared ratio, K_gate_ratio, is not chosen freely. It is forced by the definitions, which themselves come from the framework's forcing chain. The golden ratio appears because it is the unique self-similar scaling in the framework, and the factor 8 in the denominator reflects the eight-tick recognition cycle that the framework derives as a theorem.

What this changes for a reader is the picture of how units behave. Instead of a clock and a ruler being independent instruments, the framework models them as two displays of one underlying recognition process. The module gives the exact conversion factor between the two displays, and it does so with a proof, not a postulate. The constant K_gate_ratio is the bridge: it converts a base time into a display time, and a base length into a display length, with the same multiplier on both sides.

/-- Canonical K-gate: both route ratios equal K_gate_ratio. -/
theorem K_gate_eqK (U : RSUnits) (hτ : U.tau0 ≠ 0) (hℓ : U.ell0 ≠ 0) :
  ((tau_rec_display U) / U.tau0 = K_gate_ratio) ∧ ((lambda_kin_display U) / U.ell0 = K_gate_ratio) := by
  exact ⟨tau_rec_display_ratio U hτ, lambda_kin_display_ratio U hℓ⟩

/-- Kinematic consistency: c · τ_rec(display) = λ_kin(display). -/
lemma lambda_kin_from_tau_rec (U : RSUnits) : U.c * tau_rec_display U = lambda_kin_display U := by
  simp only [tau_rec_display, lambda_kin_display]
  -- Goal: U.c * (2 * π * τ₀ / (8 * log φ)) = 2 * π * ℓ₀ / (8 * log φ)
  have h : U.c * U.tau0 = U.ell0 := U.c_ell0_tau0
  calc U.c * (2 * Real.pi * U.tau0 / (8 * Real.log phi))
      = (2 * Real.pi * (U.c * U.tau0)) / (8 * Real.log phi) := by ring
    _ = (2 * Real.pi * U.ell0) / (8 * Real.log phi) := by rw [h]

What this page does not claim

This module does not derive the value of the speed c or the base units tau0 and ell0. The K-gate ratio is not claimed to be a measured physical constant; it is a definitional constant within the framework.

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/KDisplayCore.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: