candidate_phi_sq
plain-language theorem explainer
The definition supplies the amplitude candidate with C set to phi to the negative two, derived from three-channel factorization and tagged as hypothesis status. Researchers testing kernel constants against the phi-ladder in the DIF amplitude paper would cite this entry when enumerating possible C values. It is realized by direct record construction that populates the AmplitudeCandidate structure fields.
Claim. The kernel amplitude candidate satisfies $C = phi^{-2}$, with derivation string ``3-channel factorization'' and status hypothesis.
background
The DIF AmplitudeHypothesis module introduces AmplitudeCandidate as a structure holding a real C, a derivation string, and a CandidateStatus tag. This lives inside Recognition Science where the phi-ladder supplies constants via phiRung n = phi^n, as recorded in RSNativeUnits.status together with coherence quantum phi^{-5}. Upstream results supply the canonical arithmetic object from ArithmeticOf.canonical and the non-resonant schedule from NonParasitism.canonical that underwrite the arithmetic and scheduling context for amplitude candidates.
proof idea
The definition is a direct structure instantiation that assigns C := phi ^ (-(2 : ℤ)), derivation := ``3-channel factorization'', and status := CandidateStatus.hypothesis. No lemmas are applied beyond the imported definition of phi.
why it matters
This definition feeds the theorem candidate_phi_sq_status that confirms its hypothesis status. It populates the phi^{-2} slot in the amplitude hypothesis paper, linking to the phi-ladder and T7 eight-tick octave of the forcing chain. It touches the open question of which candidate matches measured kernel amplitudes.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.