Pith. sign in
module module moderate

IndisputableMonolith.Physics.DecaySpectrumFromPhiLadder

show as:
view Lean formalization →

Defines particle decay channels and lifetimes on the Recognition Science phi-ladder, with ratios fixed by powers of phi and a certificate packing the spectrum claims. Experimental or phenomenological RS work on width hierarchies would cite it. The module is largely definitional: channel data, closed-form lifetimes, positivity, and a cert bundle.

claimOn the $\varphi$-ladder, each decay channel is assigned a lifetime $\tau$ built from the RS time quantum and a $\varphi$-power; the module records channel count, lifetime ratios, positivity $\tau>0$, and a certificate that the spectrum is well-formed.

background

Recognition Science places masses and related scales on a discrete $\varphi$-ladder (golden-ratio self-similarity forced at T6). Lifetimes and widths are expected to inherit the same rung structure once the fundamental tick $\tau_0$ is fixed. The Constants import supplies that tick: $\tau_0=1$ in RS-native units.

This module turns that expectation into concrete Lean objects: a decay-channel type, a channel count, a lifetime map, lifetime ratios between channels, and a positivity lemma. A certificate structure packages the spectrum so downstream physics layers can assume a coherent decay hierarchy without re-deriving the ladder arithmetic.

proof idea

Definition-and-certificate module rather than a deep proof development. Channels and the lifetime formula are introduced as data; positivity of lifetime is a short inequality from the positivity of $\varphi$ and $\tau_0$; ratios are algebraic quotients of $\varphi$-powers. The cert constructor assembles these facts into one record for reuse.

why it matters in Recognition Science

Connects the phi-ladder mass formula (yardstick times $\varphi^{\mathrm{rung}-8+\mathrm{gap}(Z)}$) to decay phenomenology: if masses sit on rungs, partial widths and lifetimes should too. No downstream Lean dependents are recorded yet; the module is a physics-facing interface that later spectrum or branching-ratio theorems can import. It sits in the same constants ecosystem as $c=1$, $\hbar=\varphi^{-5}$, and the eight-tick octave, keeping decay times in RS-native units.

scope and limits

depends on (1)

Lean names referenced from this declaration's body.

declarations in this module (7)