pith. sign in
theorem

defect_zero_iff_one

proved
show as:
module
IndisputableMonolith.Foundation.LawOfExistence
domain
Foundation
line
58 · github
papers citing
48 papers (below)

plain-language theorem explainer

The equivalence that defect vanishes precisely when the argument equals unity for positive reals supplies the sharp characterization of the J-cost minimum. Researchers formalizing the Law of Existence and the determinism resolution cite this result to equate zero defect with the unique existent. The tactic proof unfolds defect to J, splits the biconditional, and reduces the forward direction to the quadratic identity (x-1)^2=0 via linarith and nlinarith.

Claim. For every real $x>0$, let $J(x)= (x + x^{-1})/2 -1$. Then $J(x)=0$ if and only if $x=1$.

background

The LawOfExistence module supplies a literal formalization of the Law of Existence: a positive real exists precisely when its defect vanishes. Defect is defined by defect x := J x, where J is the cost functional calibrated on the positive reals by the ledger factorization and phi-forcing structures. Upstream results include the J-cost structure in PhiForcingDerived.of and the nuclear-density tiering in NucleosynthesisTiers.of, both of which presuppose the same J on (0,infty). The present theorem isolates the unique zero of this functional.

proof idea

The proof is a tactic-mode algebraic reduction. It first simplifies defect and J, then applies constructor to split the biconditional. The forward direction assumes defect x =0, obtains x + x^{-1}=2 by linarith, multiplies through by x, clears the denominator with field_simp, and invokes nlinarith on the non-negativity of (x-1)^2. The converse direction substitutes directly.

why it matters

This characterization is invoked by determinism_resolution to establish the unique J-cost minimizer, by discreteness_forcing_principle to force discrete ontology, and by continuous_no_isolated_zero_defect to show that continuous spaces admit no isolated zero-defect points. It completes the T5 J-uniqueness step in the forcing chain and supplies the concrete condition used in inevitability_equivalence.summary. The result closes the gap between the abstract cost functional and the claim that only unity is stable.

Switch to Lean above to see the machine-checked source, dependencies, and usage graph.