divergence_at_zero_direction
plain-language theorem explainer
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.
Claim. There 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
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.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.