def
definition
J
show as:
view math explainer →
open explainer
Read the cached plain-language explainer.
open lean source
IndisputableMonolith.Astrophysics.StellarAssembly on GitHub at line 62.
browse module
All declarations in this module, on Recognition.
explainer page
depends on
formal source
59/-! ## Recognition Cost Model -/
60
61/-- Recognition cost for scale ratio x: J(x) = ½(x + 1/x) - 1 -/
62noncomputable def J (x : ℝ) : ℝ := Cost.Jcost x
63
64/-- J is minimized at x = 1 with J(1) = 0 -/
65lemma J_unit_zero : J 1 = 0 := Cost.Jcost_unit0
66
67/-- J is nonnegative for positive arguments -/
68lemma J_nonneg {x : ℝ} (hx : 0 < x) : 0 ≤ J x := by
69 unfold J
70 have : Cost.Jcost x = (x - 1)^2 / (2 * x) := by
71 unfold Cost.Jcost
72 have hne : x ≠ 0 := ne_of_gt hx
73 field_simp [hne]
74 ring
75 rw [this]
76 exact div_nonneg (sq_nonneg _) (by linarith)
77
78/-! ## Stellar Configuration -/
79
80/-- A stellar configuration specifies the scale ratios for emission and storage -/
81structure StellarConfig where
82 /-- Scale ratio for photon emission events -/
83 r_emit : ℝ
84 /-- Scale ratio for mass storage events -/
85 r_store : ℝ
86 /-- Both ratios must be positive -/
87 emit_pos : 0 < r_emit
88 store_pos : 0 < r_store
89
90namespace StellarConfig
91
92/-- Recognition cost for emission -/