impossible_infinite_cost
plain-language theorem explainer
No real number x ≤ 0 equals the value of any configuration. Modal geometry researchers cite this result to mark the lower boundary of the possibility space. The proof is a one-line term-mode contradiction that invokes the built-in positivity field on every configuration and closes with linear arithmetic.
Claim. For every real number $x$ with $x ≤ 0$, there is no configuration $c$ such that the value field of $c$ equals $x$.
background
In ModalGeometry, configurations are taken from the ILG structure whose value field is required to be strictly positive. The J-cost, introduced in PhiForcingDerived, diverges to infinity as the argument approaches zero from above, so the region x ≤ 0 is excluded from the possibility space. Upstream lemmas supply the ledger factorization that calibrates J and the spectral emergence that fixes the discrete tier structure underlying all admissible values.
proof idea
The term proof introduces the witness pair ⟨c, hc⟩, extracts the positivity fact 0 < c.value from the Config structure, and obtains an immediate contradiction with the hypothesis x ≤ 0 by linarith.
why it matters
The theorem supplies the lower edge of the possibility ball used throughout ModalGeometry. It realizes the boundary statement that ∂P is a limit point where J(x) → ∞ rather than an attainable configuration, thereby closing the forcing chain step that separates admissible costs from the infinite-cost region. No downstream uses are recorded yet.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.