pith. sign in
module module high

IndisputableMonolith.Physics.TachyonFreeTachyonFromRS

show as:
view Lean formalization →

This module establishes the tachyon-free condition in Recognition Science by proving J >= 0 for all states. Physicists deriving stable spectra from the phi-ladder would cite it to rule out tachyonic modes before computing masses. It consists of supporting definitions and a non-negativity lemma built directly on the imported Constants module.

claimThe tachyon-free condition holds when $J(x) = (x + x^{-1})/2 - 1$ satisfies $J(x) >= 0$ for every admissible state $x$, with $J$ the cost function on the recognition ladder.

background

The module imports the RS time quantum tau_0 = 1 tick from Constants. It defines auxiliary objects including StringMode, stringModeCount, massless_state, and TachyonFreeCert to isolate the J-cost non-negativity statement. The J function itself originates from the T5 uniqueness step, where J(x) equals cosh(log x) - 1 and is therefore non-negative by the range of the hyperbolic cosine.

proof idea

This is a definition module, no proofs. It assembles the J >= 0 claim through the sibling lemma jcost_nonneg and the certificate TachyonFreeCert, each relying on the algebraic identity imported from Constants.

why it matters in Recognition Science

The module supplies the stability prerequisite for all downstream mass formulas on the phi-ladder. It directly implements the tachyon-free requirement that follows from T5 J-uniqueness and precedes any application of the mass formula yardstick * phi^(rung - 8 + gap(Z)). No parent theorem is listed in the used-by graph, yet the construction closes the logical step from the forcing chain to physical spectra.

scope and limits

depends on (1)

Lean names referenced from this declaration's body.

declarations in this module (6)