candidate_phi_3half
plain-language theorem explainer
The declaration defines the amplitude candidate C = phi to the power -3/2 for the ILG kernel specification. Researchers enumerating discrete field amplitudes on the phi-ladder would cite it when listing DIF candidates. The definition is a direct record construction that assigns the numerical value, a derivation label, and candidate status.
Claim. The candidate kernel amplitude is defined by $C = phi^{-3/2}$, equipped with derivation label ``RS canonical ILG spec'' and marked with candidate status.
background
AmplitudeCandidate is a structure that records a real number C, a derivation string, and a status flag for kernel amplitudes in the DIF model. The module enumerates several phi-based candidates for this constant. Upstream results supply the phi constant via RSNativeUnits, the fundamental tick as the time quantum, and the canonical arithmetic object that keeps the construction realization-independent.
proof idea
The definition is a direct record literal that sets the C field to phi raised to -3/2, the derivation field to the string ``RS canonical ILG spec'', and the status field to candidate.
why it matters
This entry populates the list of amplitude candidates examined in the DIF amplitude hypothesis. It aligns with the phi self-similar fixed point and eight-tick octave from the forcing chain. No downstream theorems depend on it yet, so its selection as the physical amplitude remains open.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.