No prose has been written for this declaration yet. The Lean source and graph data below render
without it.
generate prose now
formal statement (Lean)
298noncomputable def shiftedHValueOf (x : ℝ) (hx : 0 < x) : ShiftedHValue :=
proof body
Definition body.
299 ⟨H x, H_ge_one x hx⟩
300
301/-! ## §5. The Defect Pseudometric -/
302
303/-- **Defect distance**: d(x,y) = J(x/y) measures the "cost of deviation"
304 between two positive reals.
305
306 Properties:
307 - d(x,x) = 0 (identity)
308 - d(x,y) = d(y,x) (symmetry, from J reciprocity)
309 - d(x,y) ≥ 0 (non-negativity) -/
depends on (17)
Lean names referenced from this declaration's body.
-
H
in IndisputableMonolith.Algebra.CostAlgebra
decl_use
-
H_ge_one
in IndisputableMonolith.Algebra.CostAlgebra
decl_use
-
ShiftedHValue
in IndisputableMonolith.Algebra.CostAlgebra
decl_use
-
of
in IndisputableMonolith.Astrophysics.NucleosynthesisTiers
decl_use
-
H
in IndisputableMonolith.Cost.FunctionalEquation
decl_use
-
Defect
in IndisputableMonolith.CPM.LNALBridge
decl_use
-
of
in IndisputableMonolith.Foundation.DAlembert.LedgerFactorization
decl_use
-
reciprocity
in IndisputableMonolith.Foundation.LedgerForcing
decl_use
-
cost
in IndisputableMonolith.Foundation.MultiplicativeRecognizerL4
decl_use
-
cost
in IndisputableMonolith.Foundation.ObserverForcing
decl_use
-
identity
in IndisputableMonolith.Foundation.ObserverForcing
decl_use
-
of
in IndisputableMonolith.Foundation.PhiForcingDerived
decl_use
-
from
in IndisputableMonolith.Foundation.PrimitiveDistinction
decl_use
-
of
in IndisputableMonolith.Foundation.SpectralEmergence
decl_use
-
of
in IndisputableMonolith.Information.PhysicsComplexityStructure
decl_use
-
two
in IndisputableMonolith.QFT.SpinStatistics
decl_use
-
identity
in IndisputableMonolith.RRF.Foundation.VantageCategory
decl_use