Constants Kdisplay Core K Gate Eq K

The K-gate identity

In the Recognition Science framework, a recognition event, a discrete act of registering a change, has two measurable faces: a duration and a length. The framework's display definitions assign each face a specific value. The clock-side display duration is (2π·τ₀) / (8 ln φ), and the length-side display length is (2π·ℓ₀) / (8 ln φ), where τ₀ and ℓ₀ are the base units of time and length, and φ is the golden ratio.

Each display value, when divided by its base unit, reduces to the same dimensionless number: π / (4 ln φ). This number is the K-gate ratio. The theorem K_gate_eqK states that both ratios, the clock-side ratio and the length-side ratio, equal this single constant. The proof is a direct algebraic simplification: it unfolds the definitions and cancels the base units, with no additional assumptions beyond the base units being nonzero.

The identity is called kinematic consistency. It means that the speed of recognition, the ratio of display length to display duration, is built into the definitions. The lemma lambda_kin_from_tau_rec shows that the speed c times the display duration equals the display length, using the defining relation c·τ₀ = ℓ₀. The K-gate identity is not a physical law about the world; it is a structural fact about how the framework's display units are defined.

In Recognition Science, this identity is a piece of the framework's internal bookkeeping. It guarantees that the two routes for measuring a recognition cycle, one through time and one through length, agree. The framework models this agreement as a theorem, but the theorem only establishes the equality of ratios; it does not assign a numerical value to the K-gate ratio beyond its definition, and it does not claim that this ratio corresponds to any measured physical constant.

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

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

The K-gate identity does not assign a numerical value to the speed of recognition. The theorem does not claim the K-gate ratio matches any measured physical constant. This result does not derive the golden ratio or the base units from more fundamental principles.

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: