defect_tendsto_atTop_at_zero
plain-language theorem explainer
The declaration establishes that defect(x) diverges to positive infinity as x approaches zero from above. Researchers formalizing the Law of Existence cite it to justify that non-unity states incur unbounded cost. The proof reduces the claim to the known divergence of the reciprocal by applying an algebraic lower bound and the tendsto_atTop predicate from Mathlib.
Claim. As $x$ tends to $0$ from above, $J(x)$ tends to $+∞$, where $J(x) := (x + x^{-1})/2 - 1$.
background
The Law of Existence module formalizes the principle that an entity exists if and only if its defect vanishes. The functional J is defined as $(x + x^{-1})/2 - 1$ for real x, and defect coincides with J on the positive reals. The module lists supporting results such as defect_zero_iff_one, which equates vanishing defect with the value 1, and nothing_cannot_exist, which asserts that defect exceeds any bound near zero.
proof idea
The tactic proof unfolds defect and J, then invokes tendsto_inv_nhdsGT_zero to obtain the divergence of the reciprocal. It rewrites the tendsto_atTop goal, pulls back a sufficiently large bound via the reciprocal limit, and applies linarith twice to establish the lower bound $(x + x^{-1})/2 - 1 ≥ x^{-1}/2 - 1$ together with positivity on the punctured neighborhood.
why it matters
This result supplies the analytic content for the module's nothing_cannot_exist statement and reinforces that unity is the unique point of zero defect. It closes the local argument that existence is economically inevitable by showing the cost functional is minimized only at 1. The divergence aligns with the J-cost appearing in the forcing chain and the Recognition Composition Law.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.