30 refine ⟨?_⟩ 31 -- Proposition-level bridge: this module records the argument surface. 32 exact hZP.no_characteristic_time 33 34/-! ## Discreteness forcing (editor concern #4) 35 36The editor flagged that "continuous configurations cannot stabilize under J-cost 37minimization" is hand-wavy. We record the precise formal content here: the 38`discreteness_forcing_principle` from `Foundation.DiscretenessForcing` establishes 39that J has a unique isolated minimum at x=1, positive curvature J''(0)=1, and 40any zero of the defect in R>0 is non-isolated in the reals (every neighborhood 41contains other points). The discrete ledger arises because stable closure requires 42finite cost barriers between distinct states, which continuous configurations lack. 43 44This module re-exports the key facts for the DIF certificate. -/ 45 46/-- The discreteness-forcing principle from the Lean framework. 47 Re-exported as a proposition-level statement for the DIF paper. 48 The four conjuncts are: 49 (1) defect(x) >= 0 for all x > 0 50 (2) defect(x) = 0 iff x = 1 (unique minimum) 51 (3) J_log''(0) = 1 (positive curvature at equilibrium) 52 (4) Any zero of defect is non-isolated in R (continuous neighborhoods 53 always contain nearby points, preventing finite cost barriers) 54 55 The paper's Section 3.1 claim that "continuous configurations cannot 56 stabilize" follows from conjunct (4): in a continuous space, x=1 has 57 no finite cost barrier separating it from nearby configurations. 58 Discrete configurations (integer-valued cochains) do have such barriers. -/
depends on (30)
Lean names referenced from this declaration's body.