CostBridge
plain-language theorem explainer
The configuration-to-cost bridge supplies a map from abstract configurations to positive real scalars that serves as input for defect and stabilization calculations. Researchers formalizing decidability of predicates under recognition dynamics cite this when constructing the interface between configuration space and the J-cost domain. The declaration is a direct structure with a single field and positivity constraint requiring no further proof.
Claim. A configuration-to-cost bridge on a type $C$ consists of a function $χ : C → ℝ$ such that $χ(c) > 0$ for all $c ∈ C$.
background
In the Recognition Science ontology, existence and truth emerge as outcomes of cost minimization under the unique J function rather than as primitive notions. The module defines RSExists via zero defect on the cost image and RSTrue via stabilization of predicates along orbits. The configuration-to-cost bridge provides the necessary scalar map that converts configurations into the real-valued inputs required by these definitions.
proof idea
The declaration is a structure definition that introduces the cost map field together with its positivity axiom. No tactics or lemmas are invoked; the structure serves as a pure interface type for all subsequent predicate definitions in the module.
why it matters
This structure earns its place by enabling the definitions of RSExists_cfg and RSTrue that replace placeholder notions of existence and truth with cost-based selection. It is used directly by RecognitionBridge and the Boolean-law theorems such as rs_true_and and rs_true_neg_iff_neg_rs_true. In the broader framework it connects the J-uniqueness and phi-forcing chain (T5-T6) to operational predicate reasoning, closing the loop from the forcing chain to verifiable ontology.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.