spectralGap_k2_val
plain-language theorem explainer
The declaration fixes the spectral gap at k-core depth 2 to exactly 1 over phi squared. Network modelers checking the phi-decay ladder for the Internet AS graph would cite this concrete value when verifying the predicted ratio of successive gaps. The equality follows at once by reflexivity on the definition of spectralGap.
Claim. $λ_2(2) = φ^{-2}$
background
The module develops the spectral gap λ₂(k) of the Internet AS-level graph under the phi-ladder hypothesis. The function spectralGap(k) is defined as the reciprocal of phi raised to k, which directly encodes the RS prediction that λ₂(k) decays as φ^{-k}. This rests on the upstream definition spectralGap(k) := phi ^ (-k) from the InternetSpectralGap module. The local setting states that the ratio λ₂(k+1)/λ₂(k) equals 1/φ, with the k=2 case giving approximately 0.382.
proof idea
The proof is a one-line wrapper that applies reflexivity to the definition of spectralGap at argument 2.
why it matters
This value anchors the phi-ladder prediction for network spectral gaps inside Recognition Science. It supplies the concrete k=2 instance of the general decay λ₂(k) = φ^{-k} that follows from the self-similar fixed point phi. No downstream theorems are recorded yet, but the result contributes to the certification of the Internet spectral gap model.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.