theorem
proved
barrier_eq
show as:
view math explainer →
open explainer
Generate a durable explainer page for this declaration.
open lean source
IndisputableMonolith.Unification.ConsciousnessBandwidth on GitHub at line 63.
browse module
All declarations in this module, on Recognition.
explainer page
depends on
formal source
60def barrierTicks : ℕ := 360
61
62/-- 360 = 8 × 45: the barrier spans exactly 45 octaves. -/
63theorem barrier_eq : barrierTicks = 8 * 45 := by norm_num [barrierTicks]
64
65/-- 360 = lcm(8, 45). -/
66theorem barrier_is_lcm : barrierTicks = Nat.lcm 8 45 := by
67 native_decide
68
69/-- The barrier period in RS time units (τ₀ = 1). -/
70noncomputable def barrierPeriod : ℝ := (barrierTicks : ℝ) * τ₀
71
72theorem barrierPeriod_pos : 0 < barrierPeriod := by
73 unfold barrierPeriod τ₀ tick barrierTicks
74 norm_num
75
76theorem barrierPeriod_eq : barrierPeriod = 360 := by
77 unfold barrierPeriod τ₀ tick barrierTicks
78 norm_num
79
80/-! ## §2. Boundary Area Model -/
81
82/-- Boundary area as a function of extent (spherical boundary).
83 A(L) = 4πL². -/
84noncomputable def boundaryArea (L : ℝ) : ℝ := 4 * Real.pi * L ^ 2
85
86theorem boundaryArea_pos {L : ℝ} (hL : 0 < L) : 0 < boundaryArea L := by
87 unfold boundaryArea
88 exact mul_pos (mul_pos (by linarith) Real.pi_pos) (sq_pos_of_pos hL)
89
90theorem boundaryArea_monotone {L₁ L₂ : ℝ} (h₁ : 0 < L₁) (h : L₁ ≤ L₂) :
91 boundaryArea L₁ ≤ boundaryArea L₂ := by
92 unfold boundaryArea
93 apply mul_le_mul_of_nonneg_left