theorem proved term proof

`nu_corrected_at_zero`

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

formal statement (Lean)

 162theorem nu_corrected_at_zero (D : ℝ) :
 163    nu_corrected D 0 = nu_leading := by

proof body

Term-mode proof.

 164  unfold nu_corrected; rw [anomalous_nu_correction_zero]; ring
 165
 166/-- The Q₃ spectral-gap multiplicity equals the graph degree D = 3.
 167    This is the structural reason why D = 3 appears in the denominator
 168    of the anomalous correction. -/

depends on (17)

Lean names referenced from this declaration's body.

of in IndisputableMonolith.Astrophysics.NucleosynthesisTiers 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
gap in IndisputableMonolith.Gap45.Derivation decl_use
of in IndisputableMonolith.Information.PhysicsComplexityStructure decl_use
correction in IndisputableMonolith.Information.QuantumChannelCapacityFromPhi decl_use
gap in IndisputableMonolith.Masses.AnchorPolicy decl_use
gap in IndisputableMonolith.Masses.RSBridge.Anchor decl_use
is in IndisputableMonolith.Mathematics.RamanujanBridge.MockThetaPhantom decl_use
anomalous_nu_correction_zero in IndisputableMonolith.Physics.ThermalFixedPoint decl_use
nu_corrected in IndisputableMonolith.Physics.ThermalFixedPoint decl_use
nu_leading in IndisputableMonolith.Physics.ThermalFixedPoint decl_use
gap in IndisputableMonolith.RSBridge.Anchor decl_use