derivedCostOn
plain-language theorem explainer
The definition extracts a cost function from any comparison operator on an ordered field by evaluating the operator at the input and the multiplicative identity. Researchers on the Recognition Science bootstrap from logic to reals cite it when converting abstract comparison operators into concrete cost maps. It is realized as a one-line wrapper applying the operator directly to the input and unit element.
Claim. Let $K$ be a type with multiplicative identity. For a comparison operator $C : K → K → K$, the derived cost is the map $r ↦ C(r, 1)$.
background
ComparisonOperatorOn abbreviates a binary map on a linearly ordered field, serving as the comparison operator in the Law of Logic. The module DomainBootstrap closes the bootstrap loop by showing that any ordered field supporting such an operator, together with Archimedean and Dedekind-completeness hypotheses, is canonically isomorphic to the reals. Upstream, the Identity property states that comparing a thing with itself costs zero, the mathematical counterpart of the Aristotelian law A = A. The constant K is the dimensionless bridge ratio defined non-circularly as the square root of phi.
proof idea
The definition is a one-line wrapper that applies the comparison operator to the input value and the multiplicative identity.
why it matters
This definition supplies the concrete cost extraction step inside the DomainBootstrap module, enabling the uniqueness theorem that any ordered field supporting the Law of Logic is isomorphic to the reals. It fills the move from the functional-equation formulation to domain-specific operators without adding hypotheses. The construction touches the framework's recovery of the real line from the comparison operator while leaving the completeness conditions explicit.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.