costCompose
plain-language theorem explainer
The binary cost operation supplies the algebraic rule for combining two J-costs according to the Recognition Composition Law. Researchers deriving properties of composed recognition events in the Recognition Science algebra would cite this definition. It is introduced as the direct transcription of the right-hand side of the RCL without any lemmas.
Claim. $a ★ b := 2ab + 2a + 2b$ for $a, b ∈ ℝ$, equivalently $2(a + 1)(b + 1) - 2$. This is the cost of the product ratio when $a = J(x)$ and $b = J(y)$ for the J-cost function.
background
The J-cost function is defined by $J(x) = ½(x + x^{-1}) - 1$ and is the unique cost obeying the Recognition Composition Law $J(xy) + J(x/y) = 2J(x)J(y) + 2J(x) + 2J(y)$. In this module the binary cost operation is introduced as the right-hand side of the RCL applied to two costs. Upstream results define cost via derivedCost in MultiplicativeRecognizerL4 and via Jcost in ObserverForcing, establishing that recognition events carry nonnegative J-costs.
proof idea
The declaration is a direct definition of the operation. It transcribes the algebraic expression from the RCL without invoking any lemmas or tactics beyond the definition itself. Subsequent properties such as commutativity are proved by unfolding this definition and applying ring normalization.
why it matters
This definition establishes the composition operation for costs in the Recognition framework, directly implementing the RCL. It serves as the foundation for all downstream theorems in the module, including the commutativity result, the associator defect theorem, the non-negativity preservation, and the factored form. The operation connects to the J-uniqueness in the forcing chain (T5) and enables the study of the shifted monoid structure H = J + 1.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.