continuous_no_isolated_zero_defect
plain-language theorem explainer
If a positive real has zero defect, every neighborhood contains another point with arbitrarily small defect. Researchers deriving discreteness from cost landscapes cite this to show continuous spaces lack isolated J-minima. The proof reduces to the unit point via the zero-defect characterization, then explicitly constructs a nearby point and bounds its quadratic J-cost below epsilon by case split on the size of epsilon.
Claim. Let $J(x) = (x + x^{-1})/2 - 1$. For every real $x > 0$, if the defect of $x$ is zero then for every $ε > 0$ there exists real $z ≠ x$ with $|z - x| < ε$ and defect of $z$ less than $ε$.
background
The DiscretenessForcing module establishes that continuous configuration spaces admit no stable J-minima because any point can be perturbed by an arbitrarily small amount at arbitrarily small cost. The defect functional equals J on positive reals, and the upstream LawOfExistence theorem defect_zero_iff_one states that defect(x) = 0 if and only if x = 1 for x > 0. The module document records that J possesses a unique minimum at unity and that infinitesimal perturbations therefore produce infinitesimal defect.
proof idea
The tactic proof applies defect_zero_iff_one to obtain x = 1. It sets t = min(ε/2, 1/2), takes z = 1 + t, verifies the distance bound by direct comparison, and rewrites defect(z) as t²/(2(1+t)). The bound t²/(2(1+t)) < ε is obtained by first comparing to t²/2, then splitting into cases ε ≤ 1 (where the quadratic is at most ε²/8) and ε > 1 (where it is at most 1/8) using linarith, sq_le_sq', and norm_num.
why it matters
This result supplies one direction of the discreteness argument recorded in the module document: continuous spaces yield no stable configurations, while discrete spaces permit them. It instantiates the J-uniqueness property from the forcing chain (T5) inside the concrete setting of the real line. The theorem therefore contributes to the larger claim that RS existence requires a discrete configuration space.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.
papers checked against this theorem (showing 5 of 5)
-
Video models copy training cases rather than learn physics laws
"when generalizing to new cases, models are observed to prioritize different factors when referencing training data: color > size > velocity > shape"
-
Policy gradients fine-tune diffusion policies to top benchmark scores
"PG methods are ubiquitous in training RL policies with other policy parameterizations; nevertheless, they had been conjectured to be less efficient for diffusion-based policies."
-
Self-distillation turns feedback into denser RL signals
"SDPO also outperforms baselines in standard RLVR environments that only return scalar feedback by using successful rollouts as implicit feedback for failed attempts."
-
Simple pixel Transformers generate competitive ImageNet samples by predicting clean data
"simple, large-patch Transformers on pixels can be strong generative models: using no tokenizer, no pre-training, and no extra loss."
-
Tiny changes fool neural networks and transfer across models
"deep neural networks learn input-output mappings that are fairly discontinuous to a significant extend. We can cause the network to misclassify an image by applying a certain imperceptible perturbation, which is found by maximizing the network's prediction error."