Physics Tachyon Free Tachyon From Rs

Tachyon-free spectrum

A tachyon is a hypothetical particle whose mass squared is negative, which would let it outrun light. In the standard string theory picture, a tachyon-free spectrum means the theory has no such unstable modes. The Recognition Science (RS) framework reaches the same conclusion from a different direction: its core cost function, which measures the price of a recognition event, is always zero or positive. Since a negative cost would correspond to a tachyon-like mode, the framework's cost function being non-negative is exactly the tachyon-free condition.

The framework's recognition cost, a number that prices how hard it is for reality to keep a discrete record of an event, is defined as J(x) = (x + 1/x)/2 - 1. The result jcost_nonneg proves that for any positive x, this cost is never negative. The massless case, where the cost is exactly zero, happens at x = 1, which the result massless_state establishes. This matches the physical idea that a massless state has no cost penalty.

The module also catalogs five canonical string modes: tachyon-suppressed, massless, massive, winding, and momentum. The result stringModeCount proves there are exactly five such modes, a count that the framework connects to a five-dimensional configuration space. The TachyonFreeCert structure bundles these three results: five modes, non-negative cost, and zero cost at masslessness. The definition tachyonFreeCert assembles them into a single certificate, all with no unproved axioms.

In plain language, the module proves that the RS framework's cost function cannot go negative, and therefore the framework has no room for tachyons. It also fixes the number of string modes at five and identifies the massless point. The practical consequence is that the framework's mathematics is consistent with a tachyon-free string theory in ten dimensions, without needing an extra postulate to exclude the tachyon.

/-- J ≥ 0 always: tachyon-free condition. -/
theorem jcost_nonneg {r : ℝ} (hr : 0 < r) : 0 ≤ Jcost r := by
  by_cases h : r = 1
  · rw [h, Jcost_unit0]
  · exact le_of_lt (Jcost_pos_of_ne_one r hr h)

/-- Massless state: J = 0. -/
theorem massless_state : Jcost 1 = 0 := Jcost_unit0

theorem stringModeCount : Fintype.card StringMode = 5 := by decide

What this page does not claim

This does not claim that tachyons are experimentally observed or ruled out by measurement. This does not claim that the five-mode count reproduces the full particle spectrum of any specific string theory. This does not claim that the cost function is derived from string theory; it is an independent framework result.

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/Physics/TachyonFreeTachyonFromRS.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: