Constants Kdisplay Core K Gate Ratio

The K-gate ratio

The K-gate ratio is a fixed number defined by the framework's ledger, a discrete record of recognition events. Its value is π / (4 ln φ), where φ is the golden ratio, approximately 1.618. The framework's machine-checked library of formal theorems proves that this same constant appears in two separate places: when the clock-side display unit is divided by its base time unit, and when the length-side display unit is divided by its base length unit. Both ratios equal K_gate_ratio exactly.

The two display definitions share a common shape. The clock-side display time is (2π·τ₀) / (8 ln φ), and the length-side display length is (2π·ℓ₀) / (8 ln φ), where τ₀ and ℓ₀ are the framework's base time and length units. Dividing each display value by its corresponding base unit cancels the base unit entirely, leaving only the shared constant π / (4 ln φ). The library proves this cancellation for both sides, and then proves that the speed of light times the clock-side display time equals the length-side display length, a consistency condition the framework calls kinematic consistency.

What the declaration does not claim is that this constant has any physical meaning on its own. It is a definitional choice, not a derived result. The library does not prove that K_gate_ratio is special among all possible ratios, nor does it connect this constant to any measured physical quantity. The golden ratio enters through the framework's earlier forcing chain, but the K-gate ratio itself is simply the number that makes the two display definitions line up with each other.

/-- Clock-side ratio equals K_gate_ratio. -/
@[simp] lemma tau_rec_display_ratio (U : RSUnits) (hτ : U.tau0 ≠ 0) :
  (tau_rec_display U) / U.tau0 = K_gate_ratio := by
  unfold tau_rec_display K_gate_ratio
  field_simp [hτ]
  ring

/-- Length-side ratio equals K_gate_ratio. -/
@[simp] lemma lambda_kin_display_ratio (U : RSUnits) (hℓ : U.ell0 ≠ 0) :
  (lambda_kin_display U) / U.ell0 = K_gate_ratio := by
  unfold lambda_kin_display K_gate_ratio
  field_simp [hℓ]
  ring

/-- 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

K_gate_ratio is not derived from the forcing chain; it is a definitional choice. The declaration does not claim any measured physical value matches this constant. The golden ratio's role here is not proved to be unique among display constants.

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: