pith. machine review for the scientific record. sign in
structure definition def or abbrev high

DecaySpectrumCert

show as:
view Lean formalization →

DecaySpectrumCert packages the three properties that certify a decay spectrum on the phi-ladder: exactly five channels, consecutive lifetimes in geometric ratio phi, and strictly positive values. A physicist constructing exotic-decay models inside Recognition Science would cite the certificate to assert that the spectrum matches the required ladder structure. The declaration is a bare structure definition that introduces the bundled fields with no computational content or lemmas.

claimA structure certifying that the set of decay channels has cardinality 5, that lifetimes satisfy $lifetime(k+1)/lifetime(k)=phi$ for every natural number $k$, and that $lifetime(k)>0$ for every $k$, where the five channels are alpha, beta-minus, beta-plus, electron-capture and spontaneous-fission and $lifetime(k)=phi^k$.

background

The module defines five canonical exotic decay channels (alpha, beta-minus, beta-plus, electron-capture, spontaneous-fission) that realize configDim D=5. The lifetime function is supplied by the sibling definition lifetime(k) := phi^k. The upstream phi_ratio definition from Quasicrystal supplies the inverse 1/phi, while the present phi_ratio field asserts the forward ratio phi itself. The local setting is that each lifetime occupies one rung of the phi-ladder, furnishing a discrete spectrum for decays.

proof idea

The declaration is a structure definition with an empty proof body. It simply declares the three field types; no lemmas are applied and no tactics are invoked.

why it matters in Recognition Science

The structure is instantiated downstream by decaySpectrumCert, which supplies the concrete witnesses decayChannel_count, lifetime_ratio and lifetime_pos. It thereby certifies the phi-ladder decay spectrum required by the Recognition Science physics module and links the five channels to the self-similar fixed point phi (T6). The certificate closes one link in the chain from the J-cost functional equation to observable decay lifetimes.

scope and limits

formal statement (Lean)

  38structure DecaySpectrumCert where
  39  five_channels : Fintype.card DecayChannel = 5
  40  phi_ratio : ∀ k, lifetime (k + 1) / lifetime k = phi
  41  lifetime_always_pos : ∀ k, 0 < lifetime k
  42

used by (1)

From the project-wide theorem graph. These declarations reference this one in their body.

depends on (4)

Lean names referenced from this declaration's body.