impossible_infinite_cost
plain-language theorem explainer
No configuration exists whose value is a non-positive real. Modal geometry work cites this to enforce that possibility space excludes the region of infinite J-cost. The proof assumes existence then derives an immediate contradiction from the built-in positivity of Config.value.
Claim. For every real number $x$ with $x ≤ 0$, there is no configuration $c$ satisfying $c.value = x$.
background
ModalGeometry imports Possibility and Actualization to define a space of configurations whose values are governed by the J-cost function. In the ILG framework, Config is equipped with a positivity axiom stating that every configuration value is strictly positive. The accompanying module comment identifies the boundary ∂P as the limit point where J(x) diverges to infinity as the argument approaches zero from above; non-positive values therefore lie outside any attainable configuration.
proof idea
The term proof opens by introducing the assumed witness pair, extracts the positivity statement c.pos, and closes the contradiction with linear arithmetic on the reals.
why it matters
The declaration marks the lower edge of the possibility space in the modal layer. It aligns with the Recognition Science boundary description where J-cost becomes infinite, consistent with the J-uniqueness and phi-ladder constructions that set physical scales. No parent theorems or downstream citations are recorded.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.