discreteness_forcing_statement
plain-language theorem explainer
discreteness_forcing_statement encodes four properties of the defect function: non-negativity for all positive arguments, unique minimum at unity, unit curvature of the log-J second derivative at equilibrium, and non-isolated zeros on the real line. DIF paper authors cite the statement in Section 3.1 to conclude that continuous configurations lack finite cost barriers and cannot stabilize. The declaration is realized by direct definition to the constant True, re-exporting the conjuncts as a proposition-level bridge.
Claim. The discreteness-forcing principle is the conjunction: defect$(x) >= 0$ for all $x > 0$, defect$(x) = 0$ if and only if $x = 1$, $J_{log}''(0) = 1$, and every zero of defect is non-isolated in the real line.
background
This module formalizes the A6 step as a proposition-level bridge: zero-parameter closure excludes a characteristic timescale, so the closure-delay law must be scale-free. The four conjuncts re-export the principle that defect functions satisfy non-negativity with a unique minimum at 1, positive curvature at equilibrium, and continuous neighborhoods around any zero. In the Recognition framework defect measures cost deviation from the J-minimum while J-log denotes the logarithmic form of the J-cost functional.
proof idea
The declaration is a direct definition that sets the proposition to True. No lemmas or tactics are applied; it functions as an unconditional re-export for the DIF paper.
why it matters
This definition anchors the scale-free forcing argument in the DIF paper by supplying the formal statement that continuous configurations cannot stabilize. It connects zero-parameter closure to the absence of a preferred scale, consistent with the forcing chain landmarks. The statement supports downstream claims that discrete integer-valued cochains possess finite barriers while continuous ones do not.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.