ThermalFixedPointCert
plain-language theorem explainer
The ThermalFixedPointCert structure certifies that the golden ratio phi is the unique positive root of the Fibonacci characteristic polynomial, that powers of phi obey the recurrence, and that the thermal eigenvalue equals phi with leading correlation-length exponent 1/phi. Physicists deriving critical exponents on the recognition lattice cite this certificate when fixing the RG scaling. It assembles the properties directly from the module's definitions of the characteristic polynomial, thermal eigenvalue, and nu_leading.
Claim. Let $phi$ denote the golden ratio. The structure certifies that the characteristic polynomial $lambda^2 - lambda - 1$ of the recurrence $a_{n+2}=a_{n+1}+a_n$ vanishes at $phi$, that $phi$ is its unique positive real root, that $phi^{n+2}=phi^{n+1}+phi^n$ for all natural $n$, that the thermal eigenvalue of the recognition-lattice fixed point equals $phi$, and that the leading correlation-length exponent satisfies $nu_0=1/phi$.
background
In the recognition lattice $Z^3$ with unit cell $Q_3$, the renormalization group operates along the phi-ladder, the unique geometric scaling sequence forced by self-similarity $r^2=r+1$. Consecutive rungs obey the Fibonacci recurrence whose characteristic polynomial is $lambda^2-lambda-1$, with positive root $phi$ (from PhiForcing T6). The thermal eigenvalue $y_t$ is the growth rate per ladder step and equals $phi$, while the leading correlation-length exponent is $nu_0=1/y_t=1/phi$ (standard RG relation).
proof idea
This is a structure definition that bundles five properties drawn from sibling definitions in the same module. The fields directly reference the characteristic polynomial root at phi, its uniqueness among positive reals, the Fibonacci cascade for powers of phi, the equality thermal_eigenvalue=phi, and nu_leading=1/phi. No tactics or reductions are performed; the structure simply records these facts for downstream instantiation.
why it matters
This certificate supplies the thermal fixed-point data required by the downstream definition thermalFixedPointCert, which populates the structure with lemmas such as fibonacci_char_poly_root and thermal_eigenvalue_eq_phi. It completes the derivation chain from PhiForcing (T6) through the phi-ladder and Fibonacci recurrence to the thermal eigenvalue phi and nu_0=1/phi, anchoring critical exponents in the recognition framework. The result aligns with the eight-tick octave and D=3 by fixing the scaling on the lattice.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.