Encyclopedia Foundation Foundation Discreteness Forcing J Log Quadratic Approx
ARTICLE 3 claims 3 theorems
Foundation Discreteness Forcing J Log Quadratic Approx
A machine-checked theorem shows that near its minimum, the framework's cost function behaves like a simple parabola, a fact that underpins why stable configurations must be discrete.
The quadratic approximation
In calculus, many smooth functions look like a parabola near their lowest point. The Recognition Science framework's cost function, which assigns a nonnegative penalty to every possible configuration, is no exception. In logarithmic coordinates, where a value x is written as e^t, the cost becomes cosh(t) - 1. The theorem J_log_quadratic_approx states that for small t, this cost is very close to t²/2, with the error bounded by |t|⁴/20. This is a precise, machine-checked version of the familiar Taylor approximation.
The classical fact here is the Taylor series of the hyperbolic cosine: cosh(t) = 1 + t²/2 + t⁴/24 + ... . The theorem formalizes the first two terms and bounds the remainder. The second derivative of the cost at its minimum is exactly 1, which means the parabola has unit curvature. This unit curvature is not an accident; it is forced by the cost function's defining properties, which include reciprocal symmetry and a composition law.
In the framework, this approximation is the bridge from a continuous world to a discrete one. The argument runs as follows. If configurations could vary continuously, then any configuration could be perturbed by an arbitrarily small amount, and the cost would change by an arbitrarily small amount. No configuration would be locked in; everything would drift. The theorem shows that near the minimum, the cost grows quadratically, so infinitesimal moves cost infinitesimal amounts. Stability, in this account, requires a discrete set of allowed configurations, where moving to a neighbor costs a finite, nonzero amount. The framework's library proves that a continuous configuration space has no isolated stable points, while a discrete one can.
What the theorem does not claim is just as important. It does not say that the quadratic approximation is exact, nor that it holds for large t. It does not, by itself, prove that the physical world is discrete; that conclusion requires additional premises about what it means for a configuration to exist and be stable. The approximation is a local statement about the shape of the cost function near its minimum, and its role is to make the transition from continuous to discrete reasoning precise.
THEOREM J_log_quadratic_approx · IndisputableMonolith/Foundation/DiscretenessForcing.lean
/-- **THEOREM (GROUNDED)**: Quadratic approximation of J_log.
For small perturbations, the cost is approximately quadratic in the log-ratio. -/
theorem J_log_quadratic_approx (ε : ℝ) (hε : |ε| < 1) :
|J_log ε - ε^2 / 2| ≤ |ε|^4 / 20 := by
-- J_log ε = Jcost (exp ε) = Real.cosh ε - 1
have h_cosh : J_log ε = Real.cosh ε - 1 := by
simp [J_log, Real.cosh_eq, Real.exp_neg]
rw [h_cosh]
have h_abs : |ε|^4 = ε^4 := by
calc |ε|^4 = (|ε|^2)^2 := by ring
_ = (ε^2)^2 := by rw [sq_abs]
_ = ε^4 := by ring
rw [h_abs]
exact cosh_quadratic_bound ε hε
THEOREM J_log_second_deriv_at_zero · IndisputableMonolith/Foundation/DiscretenessForcing.lean
/-- The second derivative of J_log at t = 0 is 1.
This sets the "stiffness" of the cost bowl and determines
the minimum step cost for discrete configurations. -/
theorem J_log_second_deriv_at_zero : deriv (deriv J_log) 0 = 1 := by
-- J_log(t) = cosh(t) - 1
-- J_log'(t) = sinh(t)
-- J_log''(t) = cosh(t)
-- J_log''(0) = cosh(0) = 1
have h1 : deriv J_log = Real.sinh := by
ext t
unfold J_log
rw [deriv_sub_const, Real.deriv_cosh]
rw [h1, Real.deriv_sinh]
exact Real.cosh_zero
THEOREM continuous_no_isolated_zero_defect · discrete_minimum_stable · IndisputableMonolith/Foundation/DiscretenessForcing.lean
/-- In a path-connected space with continuous J, there are no isolated stable points.
Intuition: If x is stable with defect(x) = 0, and the space is path-connected,
we can find a path from x to any nearby point. Along this path, defect varies
continuously, so we can get arbitrarily close to zero defect at other points.
This prevents "locking in" to x — we can always drift away with negligible cost.
Note: The actual proof requires the intermediate value theorem and connectedness.
We use ℝ as the configuration space for concreteness. -/
theorem continuous_no_isolated_zero_defect :
∀ x : ℝ, 0 < x → defect x = 0 →
∀ ε > 0, ∃ z : ℝ, z ≠ x ∧ |z - x| < ε ∧ defect z < ε := by
intro x hx_pos hx ε hε
-- Since defect = 0 implies x = 1, we work at x = 1
have hx_eq_1 : x = 1 := (defect_zero_iff_one hx_pos).mp hx
subst hx_eq_1
-- Take z = 1 + min(ε/2, 1/2) to ensure z > 0 and close to 1
let t := min (ε / 2) (1 / 2 : ℝ)
have ht_pos : t > 0 := by positivity
have ht_le_half : t ≤ 1 / 2 := min_le_right _ _
use 1 + t
constructor
· linarith
constructor
· simp only [add_sub_cancel_left, abs_of_pos ht_pos]
calc t ≤ ε / 2 := min_le_left _ _
_ < ε := by linarith
· -- defect(1 + t) = J(1 + t) = t²/(2(1+t)) for small t > 0
-- For t ≤ min(ε/2, 1/2), we show this is less than ε
simp only [defect, J]
have ht_pos' : 1 + t > 0 := by linarith
have hne : 1 + t ≠ 0 := ht_pos'.ne'
-- Compute J(1+t) = ((1+t) + (1+t)⁻¹)/2 - 1 = t²/(2(1+t))
have key : (1 + t + (1 + t)⁻¹) / 2 - 1 = t^2 / (2 * (1 + t)) := by
field_simp
ring
rw [key]
-- Now show t²/(2(1+t)) < ε
have h1t_ge1 : 1 + t ≥ 1 := by linarith
have h2 : 2 * (1 + t) ≥ 2 := by linarith
have h3 : t^2 / (2 * (1 + t)) ≤ t^2 / 2 := by
apply div_le_div_of_nonneg_left (sq_nonneg t) (by positivity)
exact h2
have ht_le_half : t ≤ 1/2 := ht_le_half
have ht_le_eps2 : t ≤ ε / 2 := min_le_left _ _
-- Case split: ε ≤ 1 vs ε > 1
by_cases hε_le1 : ε ≤ 1
· -- For ε ≤ 1, t ≤ ε/2, so t²/2 ≤ (ε/2)²/2 = ε²/8 < ε
calc t^2 / (2 * (1 + t)) ≤ t^2 / 2 := h3
_ ≤ (ε/2)^2 / 2 := by
apply div_le_div_of_nonneg_right _ (by positivity)
apply sq_le_sq'
· linarith
· exact ht_le_eps2
_ = ε^2 / 8 := by ring
_ < ε := by nlinarith
· -- For ε > 1, t ≤ 1/2, so t²/2 ≤ 1/8 < 1 < ε
push_neg at hε_le1
calc t^2 / (2 * (1 + t)) ≤ t^2 / 2 := h3
_ ≤ (1/2)^2 / 2 := by
apply div_le_div_of_nonneg_right _ (by positivity)
apply sq_le_sq'
· linarith
· exact ht_le_half
_ = 1/8 := by norm_num
_ < ε := by linarith
/-- **Key Theorem**: In a discrete configuration space, the unique minimum is stable.
If 1 ∈ configs (the point with defect = 0), then it's strictly isolated:
all other configurations have defect ≥ min_gap.
This is why discrete spaces support stable existence. -/
theorem discrete_minimum_stable (D : DiscreteConfigSpace) (_h1 : (1 : ℝ) ∈ D.configs) :
∀ x ∈ D.configs, x ≠ 1 → defect x ≥ D.min_gap := by
intro x hx hx_ne
exact D.gap_property x hx hx_ne
What this page does not claim
The quadratic approximation is not exact and does not hold for large t. The theorem does not by itself prove that physical space is discrete. The framework's cost function is not claimed to be the only possible one.
Verify this page
Every tagged claim above names its theorem. To check one yourself rather than trust this page, elaborate the source module with Lean 4 and audit its axiom basis:
$ lake env lean IndisputableMonolith/Foundation/DiscretenessForcing.lean
expected axiom basis: [propext, Classical.choice, Quot.sound] (the Lean kernel's standard three; no RS-specific axioms)
A page whose claims cannot be reproduced this way does not ship. In production, every anchor links to the exact declaration in the public source release, and this block carries the build receipt for the page itself.
Derived articles
This page is generated by a question-recursion engine: the questions its answers raise become the next pages. The current agenda, with open targets marked red:
- What exactly does the framework mean by a configuration existing and being stable?
- How does the unit curvature of the cost function relate to the golden ratio and the forcing chain?
- What physical evidence would distinguish a discrete configuration space from a continuous one?
MACHINE LAYER · GROUNDED CLAIM TABLE · CLICK TO EXPAND
THEOREM J_log_quadratic_approx · IndisputableMonolith/Foundation/DiscretenessForcing.lean
/-- **THEOREM (GROUNDED)**: Quadratic approximation of J_log. For small perturbations, the cost is approximately quadratic in the log-ratio. -/ theorem J_log_quadratic_approx (ε : ℝ) (hε : |ε| < 1) : |J_log ε - ε^2 / 2| ≤ |ε|^4 / 20 := by -- J_log ε = Jcost (exp ε) = Real.cosh ε - 1 have h_cosh : J_log ε = Real.cosh ε - 1 := by simp [J_log, Real.cosh_eq, Real.exp_neg] rw [h_cosh] have h_abs : |ε|^4 = ε^4 := by calc |ε|^4 = (|ε|^2)^2 := by ring _ = (ε^2)^2 := by rw [sq_abs] _ = ε^4 := by ring rw [h_abs] exact cosh_quadratic_bound ε hεThe theorem J_log_quadratic_approx states that for small t, this cost is very close to t²/2, with the error bounded by |t|⁴/20. J_log_quadratic_approx · IndisputableMonolith/Foundation/DiscretenessForcing.leanTHEOREM J_log_second_deriv_at_zero · IndisputableMonolith/Foundation/DiscretenessForcing.lean
/-- The second derivative of J_log at t = 0 is 1. This sets the "stiffness" of the cost bowl and determines the minimum step cost for discrete configurations. -/ theorem J_log_second_deriv_at_zero : deriv (deriv J_log) 0 = 1 := by -- J_log(t) = cosh(t) - 1 -- J_log'(t) = sinh(t) -- J_log''(t) = cosh(t) -- J_log''(0) = cosh(0) = 1 have h1 : deriv J_log = Real.sinh := by ext t unfold J_log rw [deriv_sub_const, Real.deriv_cosh] rw [h1, Real.deriv_sinh] exact Real.cosh_zeroThe second derivative of the cost at its minimum is exactly 1, which means the parabola has unit curvature. J_log_second_deriv_at_zero · IndisputableMonolith/Foundation/DiscretenessForcing.leanTHEOREM continuous_no_isolated_zero_defect · discrete_minimum_stable · IndisputableMonolith/Foundation/DiscretenessForcing.lean
/-- In a path-connected space with continuous J, there are no isolated stable points. Intuition: If x is stable with defect(x) = 0, and the space is path-connected, we can find a path from x to any nearby point. Along this path, defect varies continuously, so we can get arbitrarily close to zero defect at other points. This prevents "locking in" to x — we can always drift away with negligible cost. Note: The actual proof requires the intermediate value theorem and connectedness. We use ℝ as the configuration space for concreteness. -/ theorem continuous_no_isolated_zero_defect : ∀ x : ℝ, 0 < x → defect x = 0 → ∀ ε > 0, ∃ z : ℝ, z ≠ x ∧ |z - x| < ε ∧ defect z < ε := by intro x hx_pos hx ε hε -- Since defect = 0 implies x = 1, we work at x = 1 have hx_eq_1 : x = 1 := (defect_zero_iff_one hx_pos).mp hx subst hx_eq_1 -- Take z = 1 + min(ε/2, 1/2) to ensure z > 0 and close to 1 let t := min (ε / 2) (1 / 2 : ℝ) have ht_pos : t > 0 := by positivity have ht_le_half : t ≤ 1 / 2 := min_le_right _ _ use 1 + t constructor · linarith constructor · simp only [add_sub_cancel_left, abs_of_pos ht_pos] calc t ≤ ε / 2 := min_le_left _ _ _ < ε := by linarith · -- defect(1 + t) = J(1 + t) = t²/(2(1+t)) for small t > 0 -- For t ≤ min(ε/2, 1/2), we show this is less than ε simp only [defect, J] have ht_pos' : 1 + t > 0 := by linarith have hne : 1 + t ≠ 0 := ht_pos'.ne' -- Compute J(1+t) = ((1+t) + (1+t)⁻¹)/2 - 1 = t²/(2(1+t)) have key : (1 + t + (1 + t)⁻¹) / 2 - 1 = t^2 / (2 * (1 + t)) := by field_simp ring rw [key] -- Now show t²/(2(1+t)) < ε have h1t_ge1 : 1 + t ≥ 1 := by linarith have h2 : 2 * (1 + t) ≥ 2 := by linarith have h3 : t^2 / (2 * (1 + t)) ≤ t^2 / 2 := by apply div_le_div_of_nonneg_left (sq_nonneg t) (by positivity) exact h2 have ht_le_half : t ≤ 1/2 := ht_le_half have ht_le_eps2 : t ≤ ε / 2 := min_le_left _ _ -- Case split: ε ≤ 1 vs ε > 1 by_cases hε_le1 : ε ≤ 1 · -- For ε ≤ 1, t ≤ ε/2, so t²/2 ≤ (ε/2)²/2 = ε²/8 < ε calc t^2 / (2 * (1 + t)) ≤ t^2 / 2 := h3 _ ≤ (ε/2)^2 / 2 := by apply div_le_div_of_nonneg_right _ (by positivity) apply sq_le_sq' · linarith · exact ht_le_eps2 _ = ε^2 / 8 := by ring _ < ε := by nlinarith · -- For ε > 1, t ≤ 1/2, so t²/2 ≤ 1/8 < 1 < ε push_neg at hε_le1 calc t^2 / (2 * (1 + t)) ≤ t^2 / 2 := h3 _ ≤ (1/2)^2 / 2 := by apply div_le_div_of_nonneg_right _ (by positivity) apply sq_le_sq' · linarith · exact ht_le_half _ = 1/8 := by norm_num _ < ε := by linarith/-- **Key Theorem**: In a discrete configuration space, the unique minimum is stable. If 1 ∈ configs (the point with defect = 0), then it's strictly isolated: all other configurations have defect ≥ min_gap. This is why discrete spaces support stable existence. -/ theorem discrete_minimum_stable (D : DiscreteConfigSpace) (_h1 : (1 : ℝ) ∈ D.configs) : ∀ x ∈ D.configs, x ≠ 1 → defect x ≥ D.min_gap := by intro x hx hx_ne exact D.gap_property x hx hx_neThe framework's library proves that a continuous configuration space has no isolated stable points, while a discrete one can. continuous_no_isolated_zero_defect · discrete_minimum_stable · IndisputableMonolith/Foundation/DiscretenessForcing.lean