  19  no_characteristic_time : Prop
  20
  21/-- Proposition-level output: closure-delay survival law is scale-free. -/
  22structure ZeroParamScaleFree where
  23  /-- Encodes the power-law form in dimensionless time ratio. -/
  24  survival_power_law : Prop
  25
  26/-- Gap 2 packaging: dimensional/zero-parameter argument encoded as proposition. -/
  27def zero_param_forces_scale_free
  28    (hZP : ZeroParamClosure) :
  29    ZeroParamScaleFree := by
  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

papers checked against this theorem

No papers in the current corpus map onto this theorem yet.