lemma
proved
term proof
J_bit_pos
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)
55lemma J_bit_pos : 0 < J_bit := by
proof body
Term-mode proof.
56 unfold J_bit φ
57 exact Real.log_pos Constants.one_lt_phi
58
59/-! ## Recognition Cost Model -/
60
61/-- Recognition cost for scale ratio x: J(x) = ½(x + 1/x) - 1 -/
used by (7)
From the project-wide theorem graph. These declarations reference this one in their body.
depends on (13)
Lean names referenced from this declaration's body.
-
one_lt_phi
in IndisputableMonolith.Constants
decl_use
-
J_bit_pos
in IndisputableMonolith.Constants.PlanckScaleMatching
decl_use
-
scale
in IndisputableMonolith.Cosmology.LargeScaleStructureFromRS
decl_use
-
Constants
in IndisputableMonolith.CPM.LawOfExistence
decl_use
-
Model
in IndisputableMonolith.CPM.LawOfExistence
decl_use
-
J_bit_pos
in IndisputableMonolith.Foundation.ConstantDerivations
decl_use
-
cost
in IndisputableMonolith.Foundation.MultiplicativeRecognizerL4
decl_use
-
cost
in IndisputableMonolith.Foundation.ObserverForcing
decl_use
-
J_bit_pos
in IndisputableMonolith.Foundation.PhiForcing
decl_use
-
for
in IndisputableMonolith.Foundation.UniversalForcingSelfReference
decl_use
-
Cost
in IndisputableMonolith.Measurement.RSNative.Core
decl_use
-
one_lt_phi
in IndisputableMonolith.PhiSupport
decl_use
-
one_lt_phi
in IndisputableMonolith.PhiSupport.Lemmas
decl_use