IsNearMathematical
plain-language theorem explainer
A costed configuration space is near-mathematical at threshold ε when every configuration has intrinsic cost strictly below ε. Anyone citing the effectiveness principle (near-balanced configs refer to arbitrary positive-cost objects) or the approximate mathematical backbone uses this predicate. The body is a one-line universal bound on the space's cost function J.
Claim. A costed space $(C,J)$ is near-mathematical at threshold $\varepsilon\in\mathbb{R}$ when $J(x)<\varepsilon$ for every configuration $x\in C$.
background
The module develops the Algebra of Aboutness: reference is ontological compression, not a primitive. One configuration (symbol) points to another (object) when the connecting ledger entry minimizes cost. A CostedSpace equips a type $C$ with a nonnegative cost map $J:C\to\mathbb{R}$, generalizing the RS cost $J(x)=\frac12(x+1/x)-1$ (equivalently $\cosh(\log x)-1$) to arbitrary configuration spaces.
The sibling predicate IsMathematical is the exact zero-cost case: every configuration has $J=0$. Near-mathematical relaxes that to a uniform strict upper bound $\varepsilon$. The module's effectiveness principle states that near-balanced configurations ($J\approx 0$) can refer to any positive-cost object; this definition is the formal carrier of that "near" language.
Upstream cost maps (observer events, multiplicative recognizers, PRC ratios, rung-coarsened multisets) all supply concrete $J$ instances that can be packaged as CostedSpace data.
proof idea
Definition only, no proof. The predicate is the proposition $\forall x,, J_{CS}(x)<\varepsilon$, read off the CostedSpace cost field. Nonnegativity of $J$ is already in the structure and is not re-proved here.
why it matters
This is the approximate counterpart of the mathematical backbone: zero-cost configurations have universal referential capacity, and near-zero ones are the working hypothesis behind the effectiveness principle listed in the module doc. It sits in Foundation.Reference beside ReferenceStructure, Meaning, PerfectSymbol, and IsMathematical, giving a graded notion of "how mathematical" a costed space is.
No downstream uses are wired yet (used_by is empty), so the declaration is presently a named interface for later composition and effectiveness theorems rather than a lemma already consumed by the forcing chain. It does not itself invoke T5 J-uniqueness, RCL, or the phi ladder; those enter only when a concrete RS cost is installed as the CostedSpace.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.