nothingness_infinite_cost
plain-language theorem explainer
For any real bound M there exists a positive ratio x such that the J-cost J(x) exceeds M. Researchers deriving the information-theoretic basis of physics cite this to show that the zero-ratio limit carries unbounded cost. The proof constructs an explicit x = 1/(2(|M|+2)) and verifies the inequality by algebraic expansion of the J-cost formula followed by linear arithmetic.
Claim. For every real number $M$, there exists a positive real number $x$ such that $J(x) > M$, where $J(x) = (x + x^{-1})/2 - 1$.
background
The module InformationIsLedger treats information as the physical ledger itself: every recognition event is a ratio x > 0 carrying a definite J-cost. J-cost is the function J(x) = (x + x^{-1})/2 - 1, which vanishes only at x = 1 (balanced state) and is symmetric under x to 1/x. The local setting states that J(x) > 0 precisely when the event carries physical content, with the zero-ratio limit forced to infinite cost. Upstream structures supply the J-cost definition (PhiForcingDerived.of) and the ledger factorization (DAlembert.LedgerFactorization.of) that calibrate the cost function.
proof idea
The tactic proof introduces M, builds the positive quantity |M| + 2, then sets x = 1/(2(|M| + 2)). It proves x > 0 by division of positives, unfolds Jcost, simplifies the reciprocal via field_simp, expands the expression (x + 1/x)/2 - 1 into 1/(4(|M|+2)) + |M| + 1 by ring, and closes the inequality with linarith using the non-negative absolute value of M.
why it matters
This result supplies the final step of IC-001 by proving J(x) diverges as x approaches 0 from above, completing the certificate that declares the information-ledger equivalence derived. It realizes the RS claim that nothingness is infinitely costly and therefore impossible, aligning with the forcing chain where recognition events must occur. The theorem feeds the downstream IC-001 certificate string that lists all eight core claims as established.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.