Pith. sign in
module module high

IndisputableMonolith.Physics.TachyonFreeTachyonFromRS

show as:
view Lean formalization →

The module establishes the tachyon-free condition J ≥ 0 in Recognition Science. Physicists deriving spectra from the phi-ladder cite it to exclude superluminal modes. It collects sibling definitions and lemmas around the J-cost imported from Constants, with no internal proofs.

claimTachyon-free condition: $J \geq 0$ for all states, where $J(x) = (x + x^{-1})/2 - 1$.

background

The module sits in the Physics domain and imports the RS time quantum τ₀ = 1 tick from Constants. It introduces StringMode, stringModeCount, jcost_nonneg, massless_state, TachyonFreeCert, and tachyonFreeCert to encode the condition that the recognition cost remains non-negative. This setting follows the J-uniqueness fixed point and the Recognition Composition Law.

proof idea

This is a definition module, no proofs. It organizes the tachyon-free interface through the listed sibling declarations.

why it matters in Recognition Science

The module supplies the tachyon-free certification required by downstream physics derivations in Recognition Science. It directly implements the J ≥ 0 landmark that supports the forcing chain from T5 onward and the mass formula on the phi-ladder.

scope and limits

depends on (1)

Lean names referenced from this declaration's body.

declarations in this module (6)