pith. the verified trust layer for science. sign in
theorem

discreteness_forcing_principle

proved
show as:
module
IndisputableMonolith.Foundation.DiscretenessForcing
domain
Foundation
line
517 · github
papers citing
8 papers (below)

plain-language theorem explainer

The discreteness forcing principle states that the defect functional equals the cost J(x) = (x + x^{-1})/2 - 1 for x > 0, is nonnegative, vanishes uniquely at x = 1, has log-coordinate second derivative equal to 1 at zero, and that this minimum is not isolated in the positive reals. Researchers deriving discreteness from variational cost landscapes in Recognition Science would cite it as the bridge from continuous drift to stable ontology. The proof is a term-mode conjunction of four prior facts on nonnegativity, uniqueness, curvature, and real

Claim. Let $J(x) = (x + x^{-1})/2 - 1$ for $x > 0$ and let $J(t) = J(e^t) = e^t + e^{-t} - 2)/2$ in log coordinates. Then $J(x) ≥ 0$, $J(x) = 0$ if and only if $x = 1$, the second derivative of the log form at zero equals 1, and the zero set of $J$ is not isolated in the positive reals. Hence stable minima cannot exist in a continuous configuration space.

background

The DiscretenessForcing module formalizes how the cost landscape forces discrete structure. The defect functional is defined as defect(x) = J(x) for x > 0, where J is the Recognition cost. In log coordinates J_log(t) = cosh(t) - 1 forms a convex bowl with minimum at t = 0. The module imports J_log and its second derivative from the same file and defect properties from LawOfExistence. Upstream, J_log_second_deriv_at_zero records that the curvature at the minimum is exactly 1, setting the minimum step cost. defect_nonneg and defect_zero_iff_one establish nonnegativity and the unique zero at unity.

proof idea

The proof is a term-mode conjunction that directly supplies defect_nonneg for the first conjunct, defect_zero_iff_one for the second, and J_log_second_deriv_at_zero for the curvature. The final conjunct uses a short tactic that substitutes x = 1 from the uniqueness fact and exhibits the explicit nearby point 1 + ε/2 to witness non-isolation in the reals.

why it matters

This theorem supplies the second link in the forcing chain after J-uniqueness and before the ledger and phi-ladder steps. It is invoked by zero_param_forces_scale_free to encode the zero-parameter argument for scale-free structure. In the Recognition framework it converts the cost bowl into the requirement that stable existence (RSExists) demands discrete configuration space, prior to the eight-tick octave and D = 3.

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

papers checked against this theorem (showing 8 of 8)