exclusivity_cert_exists
plain-language theorem explainer
ExclusivityCert existence certifies that the RCL derivation chain is nonempty and that exclusivity constraints uniquely determine the cost function J. Foundational uniqueness arguments in Recognition Science cite this to establish non-circular derivation of the composition law from constraints alone. The proof constructs the certificate directly by packaging the two upstream theorems on chain validity and cost uniqueness.
Claim. There exists a certificate whose fields are a nonempty RCL derivation chain together with the statement that every set of exclusivity constraints satisfying all_hold yields a function $J:ℝ→ℝ$ such that $J(x)≥0$ for all $x>0$ and $J(1)=0$.
background
The module supplies a non-circular proof that any framework satisfying NonStatic, ZeroParameters, DerivesObservables and SelfSimilar must obey the Recognition Composition Law and therefore coincide with RS. ExclusivityCert is the structure that records this conclusion: its chain_valid field holds a nonempty RCLDerivation while its cost_unique field asserts that the constraints force a unique nonnegative cost function vanishing at unity. Upstream, constraints_determine_cost constructs this J explicitly as $(x + x^{-1})/2 - 1$, and rcl_chain_is_valid asserts that the four-step derivation from universal cost through the d'Alembert relation to RS is complete.
proof idea
The proof is a one-line term construction that instantiates the ExclusivityCert structure by supplying rcl_chain_is_valid to the chain_valid field and constraints_determine_cost to the cost_unique field.
why it matters
This theorem closes Gap 1 by giving the non-circular version of the NoAlternatives argument: it derives the RCL from the four framework axioms without pre-loading the conclusion. It thereby supports the claim that RS is the unique zero-parameter framework and connects directly to T5 (J-uniqueness) in the forcing chain. The module documentation notes that earlier versions relied on RSConnectionData that already contained the target; the present certificate removes that circularity.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.