constraints_determine_cost
plain-language theorem explainer
The theorem shows that any framework meeting the four exclusivity constraints admits a non-negative cost function J vanishing at 1. Researchers proving uniqueness of Recognition Science cite it to establish that the constraints force the specific cost. The proof is a direct construction exhibiting J(x) = (x + x^{-1})/2 - 1 and verifying the properties via algebraic inequalities on square roots.
Claim. If the four exclusivity constraints hold (non-static dynamics, zero free parameters, derivation of observables, and self-similarity), then there exists a real-valued function $J$ such that $J(x) >= 0$ for every positive real $x$ and $J(1) = 0$.
background
The module Non-Circular Framework Exclusivity addresses whether Recognition Science is the unique zero-parameter framework without circular assumptions. It defines ExclusivityConstraints as the structure whose fields are the four propositions non-static (has dynamics), zero_parameters (no free parameters), derives_observables (produces measurable predictions), and self_similar (admits a scale hierarchy), together with their conjunction all_hold.
proof idea
The proof assumes the constraints hold, then constructs the explicit function J(x) := (x + x^{-1})/2 - 1. A constructor splits the existential goal into the non-negativity predicate and the condition at 1. Non-negativity follows from nlinarith applied to x + x^{-1} >= 2 using non-negativity of squares involving square roots, followed by linarith; the value at 1 is discharged by simp.
why it matters
This supplies the cost_unique field of the ExclusivityCert in the downstream theorem exclusivity_cert_exists. It advances the non-circular exclusivity argument by deriving existence of the non-negative cost function from the four axioms alone, linking directly to T5 J-uniqueness in the forcing chain and the Recognition Composition Law. The result supports the claim that any framework satisfying the listed properties must be isomorphic to Recognition Science.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.