CandidateStatus
plain-language theorem explainer
Derivation status labels organize candidate values for the amplitude constant in the ILG kernel. Researchers on the DIF amplitude hypothesis cite these labels when documenting proposals such as the phi to the minus two case. The declaration is a bare inductive definition that introduces three constructors with no further obligations.
Claim. An inductive type classifying the derivation status of candidate amplitudes for the ILG kernel constant $C$, equipped with constructors denoting derivation from prior results, status as a hypothesis, or status as a candidate.
background
The ILG kernel takes the form $w(k,a)=1+C·(max(0.01,a/(k τ₀)))^α$, where $C$ is the free amplitude parameter. Upstream definitions supply the BIT kernel families (constant, inverse, exponential) and fix the active edge count per tick at $A=1$. The module resides inside the DIF amplitude hypothesis paper and records possible numerical or symbolic choices for $C$ that remain compatible with Recognition Science constraints.
proof idea
The declaration is a bare inductive definition that introduces the three constructors derived, hypothesis, and candidate. No lemmas are applied and no tactics are used; the object functions solely as a classification scheme for downstream records.
why it matters
The type populates the AmplitudeCandidate structure and appears in the concrete records for the phi to the minus two hypothesis, the phi to the minus three-halves candidate, and the eight-tick aligned candidate. It organizes the hypothesis space for the kernel amplitude inside the Recognition framework, linking to the self-similar fixed point phi and the eight-tick octave without closing any open question.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.