decaySpectrumCert
plain-language theorem explainer
This definition assembles a certificate for the decay spectrum on the phi-ladder by supplying exactly five channels, a uniform lifetime ratio of phi between consecutive rungs, and strict positivity of all lifetimes. Physicists modeling exotic nuclear decays or phi-based mass ladders would cite it to confirm the spectrum's structural invariants. The construction is a direct record assembly from prior theorems on channel count, ratio equality, and positivity.
Claim. Let DecaySpectrumCert be the structure requiring Fintype.card(DecayChannel) = 5, lifetime(k+1)/lifetime(k) = phi for all k, and 0 < lifetime(k) for all k. Then decaySpectrumCert is the instance of this structure in which the channel count equals 5, the ratio equals phi, and all lifetimes are positive.
background
DecaySpectrumCert encodes the structural invariants of the decay spectrum derived from the phi-ladder: exactly five canonical channels (alpha, beta-minus, beta-plus, electron-capture, spontaneous-fission), consecutive lifetimes forming a geometric sequence with common ratio phi, and all lifetimes strictly positive. The module Physics.DecaySpectrumFromPhiLadder places this certificate in the local setting where each lifetime occupies one rung up the phi-ladder, with configDim D = 5 for the channel count. Upstream results supply the pieces: decayChannel_count proves the cardinality by decision, lifetime_ratio establishes the ratio equality by unfolding the lifetime definition and applying ring simplification, and lifetime_pos shows positivity via pow_pos on phi_pos.
proof idea
The definition is a one-line record constructor that directly assigns five_channels to decayChannel_count, phi_ratio to lifetime_ratio, and lifetime_always_pos to lifetime_pos.
why it matters
This definition supplies the concrete certificate that closes the structural verification of the five-channel decay spectrum inside the Recognition Science phi-ladder framework, directly supporting the mass formula via rung differences and the eight-tick octave. It fills the physics-depth slot described in the module doc-comment without introducing axioms or hidden hypotheses. No downstream theorems are listed, leaving open whether the certificate will be invoked in later derivations of branching ratios or decay rates.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.