def
definition
J_bit
show as:
view math explainer →
open explainer
Generate a durable explainer page for this declaration.
open lean source
IndisputableMonolith.Astrophysics.ObservabilityLimits on GitHub at line 52.
browse module
All declarations in this module, on Recognition.
explainer page
depends on
formal source
49/-! ## Fundamental RS Constants -/
50
51noncomputable def φ : ℝ := Constants.phi
52noncomputable def J_bit : ℝ := Real.log φ
53
54/-- Constants.phi equals Mathlib's goldenRatio (same definition) -/
55theorem phi_eq_goldenRatio : Constants.phi = goldenRatio := by
56 simp only [Constants.phi, goldenRatio]
57
58/-- Coherence energy E_coh = φ^(-5) in eV -/
59noncomputable def E_coh : ℝ := φ ^ (-(5 : ℤ))
60
61/-- Fundamental tick τ_0 (in natural units) -/
62noncomputable def τ_0 : ℝ := 1 / (8 * J_bit)
63
64/-- Recognition length l_rec = √(ℏG/(πc³)) (Planck scale) -/
65-- In natural units where c = ℏ = G = 1:
66noncomputable def l_rec : ℝ := Real.sqrt (1 / Real.pi) -- Check if rewrite failed here
67
68/-! ## Observability Constraints -/
69
70/-- Observability threshold: minimum flux for recognition -/
71noncomputable def F_threshold : ℝ := E_coh / τ_0
72
73/-- Coherence volume: maximum assembly volume -/
74noncomputable def V_coherence : ℝ := l_rec ^ 3
75
76/-- Maximum mass from coherent assembly in N cycles -/
77noncomputable def M_max (N : ℕ) (ρ : ℝ) : ℝ := ρ * V_coherence * N
78
79/-! ## J-Cost Optimization -/
80
81/-- The J-cost for mass configuration at scale ratio r -/
82noncomputable def J_mass (r : ℝ) : ℝ := Cost.Jcost r