ExclusivityConstraints
plain-language theorem explainer
ExclusivityConstraints packages four axioms required of any zero-parameter dynamical framework: time evolution, absence of free parameters, production of measurable predictions, and admission of a self-similar scale hierarchy. Uniqueness arguments for Recognition Science cite this structure when showing that the axioms alone force the Recognition Composition Law without circular loading of the target theory. The declaration is a direct structure definition that conjoins the four properties into a single predicate.
Claim. A framework satisfies exclusivity constraints when it has time evolution, zero free parameters, derives measurable predictions, and admits a scale hierarchy, with all four properties holding simultaneously.
background
The module supplies a non-circular route to framework uniqueness. It encodes four properties drawn from the question of whether any zero-parameter framework must recover the Recognition Composition Law: non-static requires dynamics (time evolution); zero-parameters requires no free constants; derives-observables requires production of measurable quantities; self-similar requires a scale hierarchy. These are packaged together via their conjunction in the structure field all_hold.
proof idea
This is a structure definition that directly conjoins the four axioms into a single predicate with no lemmas or computational steps.
why it matters
The structure supplies the hypothesis interface for the non-circular exclusivity argument. It is used by constraints_determine_cost to derive the J-cost function J(x) = (x + x^{-1})/2 - 1 and by ExclusivityCert to certify a valid RCL derivation chain. This closes the circularity gap left by the earlier NoAlternatives theorem, aligning with the T5 J-uniqueness and RCL landmarks of the forcing chain.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.