divergence_at_zero_direction
The declaration shows that the J-cost function on positive reals admits no finite upper bound. Researchers formalizing cost-minimization selection in pre-geometric models cite it to establish that the zero-cost point is the unique stable configuration. The proof proceeds by case split on the sign of any candidate bound C, followed by explicit substitution of a positive test value and linear-arithmetic contradiction.
claimThere does not exist a real number $C$ such that $J(x) = (x-1)^2/(2x)$ satisfies $J(x) ≤ C$ for every $x > 0$.
background
The Cost-First Existence module encodes the pre-Big-Bang selection principle: a positive real pattern exists in the recognition sense precisely when its J-cost vanishes, which occurs uniquely at the unit. The cost function itself is supplied by the upstream lemma Jcost_eq_sq, which rewrites J(x) as the squared ratio (x-1)^2/(2x) for x ≠ 0, together with the evaluation Jcost_unit0 giving J(1) = 0. These two facts convert the abstract cost-minimization statement into concrete algebraic comparisons.
proof idea
The tactic proof splits on whether the putative bound C is negative. When C < 0 the assumption applied at ε = 1 together with Jcost_unit0 yields an immediate contradiction by linarith. When C ≥ 0 the proof selects the test value ε = 1/(2C+4), invokes Jcost_eq_sq to obtain the closed form (2C+3)^2/(2(2C+4)), rewrites the target inequality, and closes with nlinarith after noting the quadratic comparison 4C+9 > 0.
why it matters in Recognition Science
The result populates the nothing_diverges slot inside the downstream costFirstExistenceCert definition, thereby completing the certificate that existence is selected by cost minimization. It directly supports the module claim that only the J-minimum at x = 1 is stable while all other positive values are transiently unstable, aligning with the Recognition Science premise that laws arise from the constraint that the universe minimizes J.
scope and limits
- Does not establish any lower bound on J-cost.
- Does not treat arguments outside the positive reals.
- Does not quantify the divergence rate as the argument approaches zero.
- Does not invoke the phi-ladder or dimensional forcing steps.
Lean usage
have h : ¬ ∃ (C : ℝ), ∀ (ε : ℝ), 0 < ε → Jcost ε ≤ C := divergence_at_zero_directionformal statement (Lean)
56theorem divergence_at_zero_direction :
57 ¬ ∃ (C : ℝ), ∀ (ε : ℝ), 0 < ε → Jcost ε ≤ C := by
proof body
Tactic-mode proof.
58 intro ⟨C, hC⟩
59 -- Pick ε = 1/(2*(|C|+2)); then J(ε) > |C|+1 > C
60 -- Actual proof: pick ε = 1/4, then J(1/4) = (1/4-1)²/(2·1/4) = (9/16)/(1/2) = 9/8
61 -- That only bounds J away from C when C < 9/8.
62 -- For large C, pick ε = 1/(C+2):
63 -- J(1/(C+2)) = (1/(C+2)-1)²/(2/(C+2)) = (C+1)²/(C+2)²·(C+2)/2 = (C+1)²/(2(C+2))
64 -- For C ≥ 0: (C+1)²/(2(C+2)) > C ↔ (C+1)² > 2C(C+2) = 2C²+4C ↔ C²+2C+1 > 2C²+4C ↔ 0 > C²+2C-1
65 -- This fails for C ≥ 1. Need a better choice. Use ε = 1/(2C+4):
66 -- J(1/(2C+4)) = (1/(2C+4)-1)²/(2/(2C+4)) = ((2C+3)/(2C+4))²·(2C+4)/2 = (2C+3)²/(2(2C+4))
67 -- Compare with C: (2C+3)²/(2(2C+4)) > C ↔ (2C+3)² > 2C(2C+4) = 4C²+8C
68 -- = 4C²+12C+9 > 4C²+8C ↔ 4C+9 > 0, which holds for C > -9/4.
69 -- For C ≤ -3, J(ε) ≥ 0 > C since C < 0. Done by cases.
70 -- Use J(1) = 0 to handle C < 0, and a direct computation for C ≥ 0
71 by_cases hC_neg : C < 0
72 · linarith [hC 1 one_pos, Jcost_unit0]
73 push_neg at hC_neg -- C ≥ 0
74 -- J(1/(2C+4)) = (2C+3)²/(2(2C+4)) > C for C ≥ 0
75 have h2C4 : (0 : ℝ) < 2 * C + 4 := by linarith
76 have hε := hC (1 / (2 * C + 4)) (div_pos one_pos h2C4)
77 have hJval : Jcost (1 / (2 * C + 4)) = (2 * C + 3) ^ 2 / (2 * (2 * C + 4)) := by
78 rw [Jcost_eq_sq (by positivity)]
79 field_simp
80 ring
81 rw [hJval] at hε
82 have hnum : 0 ≤ (2 * C + 3) ^ 2 := sq_nonneg _
83 -- (2C+3)²/(2(2C+4)) ≤ C ↔ (2C+3)² ≤ 2C(2C+4) = 4C²+8C
84 -- But (2C+3)² = 4C²+12C+9 > 4C²+8C = 2C(2C+4) for C ≥ 0 (since 4C+9 > 0)
85 have hrewrite : (2 * C + 3) ^ 2 / (2 * (2 * C + 4)) ≤ C ↔
86 (2 * C + 3) ^ 2 ≤ C * (2 * (2 * C + 4)) := by
87 rw [div_le_iff₀ (by positivity : (0 : ℝ) < 2 * (2 * C + 4))]
88 rw [hrewrite] at hε
89 nlinarith [sq_nonneg (2 * C + 3)]
90