theorem proved term proof

`frequencyRatioCost_nonneg`

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

formal statement (Lean)

  40theorem frequencyRatioCost_nonneg {r : ℝ} (hr : 0 < r) :
  41    0 ≤ frequencyRatioCost r :=

proof body

Term-mode proof.

  42  Jcost_nonneg hr
  43
  44/-! ## φ as Minimal-Cost Non-Trivial Ratio -/
  45
  46/-- A self-similar ratio satisfies r² = r + 1 (the defining equation of φ). -/

depends on (17)

Lean names referenced from this declaration's body.

of in IndisputableMonolith.Astrophysics.NucleosynthesisTiers decl_use
Jcost_nonneg in IndisputableMonolith.Cost decl_use
frequencyRatioCost in IndisputableMonolith.Cost.FrequencyLadder decl_use
Jcost_nonneg in IndisputableMonolith.Cost.JcostCore decl_use
of in IndisputableMonolith.Foundation.DAlembert.LedgerFactorization decl_use
A in IndisputableMonolith.Foundation.IntegrationGap decl_use
of in IndisputableMonolith.Foundation.PhiForcingDerived decl_use
as in IndisputableMonolith.Foundation.SimplicialLedger.ContinuumBridge decl_use
of in IndisputableMonolith.Foundation.SpectralEmergence decl_use
Jcost_nonneg in IndisputableMonolith.Gravity.CoherenceCollapse decl_use
Jcost_nonneg in IndisputableMonolith.Gravity.EnergyProcessingBridge decl_use
of in IndisputableMonolith.Information.PhysicsComplexityStructure decl_use
A in IndisputableMonolith.Masses.Anchor decl_use
Cost in IndisputableMonolith.Measurement.RSNative.Core decl_use
A in IndisputableMonolith.Modal.Actualization decl_use
Jcost_nonneg in IndisputableMonolith.NavierStokes.PhiLadderCutoff decl_use
self in IndisputableMonolith.RecogSpec.Core decl_use