RecognitionCostSystem
plain-language theorem explainer
RecognitionCostSystem packages a cost function on the reals, a witness that the function obeys the Recognition Composition Law, a sigma map on n-tuples, and a positive integer window W. Algebraists working in the cost layer of Recognition Science cite the structure when constructing canonical instances or deriving conservation identities. The declaration is a pure structure definition with no proof obligations or computational content.
Claim. A recognition cost system for dimension $n$ consists of a function $c : ℝ → ℝ$, a proof that $c$ satisfies the recognition composition law $∀ x,y > 0, c(xy) + c(x/y) = 2 c(x) c(y) + 2 c(x) + 2 c(y)$, a map $σ : (Fin n → ℝ) → ℝ$, and a positive integer $W$.
background
The CostAlgebra module assembles algebraic properties of cost functions that obey the Recognition Composition Law. SatisfiesRCL is the predicate encoding the single primitive identity of Recognition Science: $J(xy) + J(x/y) = 2 J(x) J(y) + 2 J(x) + 2 J(y)$ for positive reals, equivalently the calibrated d'Alembert equation in logarithmic coordinates. The sigma field is described in the module doc-comment as the canonical conservation functional given by the sum of logarithms on positive coordinates. Upstream imports supply the definition of J, the theorem RCL_holds that J satisfies the law, and related structures from NucleosynthesisTiers and ObserverForcing.
proof idea
This is a structure definition that directly assembles the four required fields: cost function, RCL witness, sigma map, and positive W. No lemmas are invoked and no tactics are used; the declaration functions solely as a type for later constructions.
why it matters
The structure supplies the interface that packages any cost function obeying the Recognition Composition Law, the foundational primitive of the entire framework. It is instantiated by canonicalRecognitionCostSystem to produce the concrete system with cost = J, rcl = RCL_holds, and the supplied window W; that instance then feeds conservation arguments and decision-theoretic results. The declaration therefore completes the algebraic packaging step before the forcing chain and phi-ladder applications.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.