IndisputableMonolith.Physics.ThermalFixedPoint

declarations in this module (23)

• def fibonacci_char_poly L48
• theorem fibonacci_char_poly_root L51
• theorem fibonacci_char_poly_unique_pos_root L55
• theorem fibonacci_recurrence L64
• theorem phi_ladder_growth L71
• def thermal_eigenvalue L91
• theorem thermal_eigenvalue_eq_phi L93
• theorem thermal_eigenvalue_uniqueness L96
• theorem thermal_eigenvalue_golden L101
• theorem thermal_eigenvalue_pos L104
• theorem thermal_eigenvalue_relevant L107
• def nu_leading L114
• theorem nu_leading_eq L116
• theorem nu_leading_pos L118
• theorem nu_leading_lt_one L122
• def anomalous_nu_correction L139
• theorem anomalous_nu_correction_zero L141
• theorem anomalous_nu_correction_small L147
• def nu_corrected L159
• theorem nu_corrected_at_zero L162
• theorem spectral_gap_multiplicity_eq_degree L169
• structure ThermalFixedPointCert L175
• def thermalFixedPointCert L182