theorem proved term proof

`thermal_eigenvalue_relevant`

No prose has been written for this declaration yet. The Lean source and graph data below render without it.

formal statement (Lean)

 107theorem thermal_eigenvalue_relevant : 1 < thermal_eigenvalue := one_lt_phi

proof body

Term-mode proof.

 108
 109/-! ## 4. The Forced Leading-Order ν -/
 110
 111/-- Leading-order correlation-length exponent: ν₀ = 1/y_t.
 112    This is the standard RG relationship between the thermal eigenvalue
 113    and the divergence of the correlation length at the critical point. -/

used by (1)

From the project-wide theorem graph. These declarations reference this one in their body.

nu_leading_lt_one in IndisputableMonolith.Physics.ThermalFixedPoint decl_use

depends on (16)

Lean names referenced from this declaration's body.

of in IndisputableMonolith.Astrophysics.NucleosynthesisTiers decl_use
one_lt_phi in IndisputableMonolith.Constants decl_use
of in IndisputableMonolith.Foundation.DAlembert.LedgerFactorization decl_use
is in IndisputableMonolith.Foundation.OptionAEmpiricalProgram decl_use
of in IndisputableMonolith.Foundation.PhiForcingDerived decl_use
is in IndisputableMonolith.Foundation.SimplicialLedger.EdgeLengthFromPsi decl_use
of in IndisputableMonolith.Foundation.SpectralEmergence decl_use
is in IndisputableMonolith.GameTheory.MechanismDesignFromSigma decl_use
of in IndisputableMonolith.Information.PhysicsComplexityStructure decl_use
is in IndisputableMonolith.Mathematics.RamanujanBridge.MockThetaPhantom decl_use
divergence in IndisputableMonolith.NavierStokes.DiscreteNSOperator decl_use
and in IndisputableMonolith.NumberTheory.CirclePhaseLift decl_use
point in IndisputableMonolith.Numerics.Interval.Basic decl_use
one_lt_phi in IndisputableMonolith.PhiSupport decl_use
one_lt_phi in IndisputableMonolith.PhiSupport.Lemmas decl_use
thermal_eigenvalue in IndisputableMonolith.Physics.ThermalFixedPoint decl_use