FrameworkConstraints
plain-language theorem explainer
FrameworkConstraints encodes the four propositional assumptions required to derive the Recognition Composition Law without circularity. A researcher establishing uniqueness of the Recognition Science framework cites this structure to start the non-circular exclusivity argument. The declaration is a bare structure definition whose fields are the properties non-static, zero-parameters, derives-observables, and self-similar.
Claim. A framework $F$ satisfies the constraints when it has dynamics (non-static), contains no free parameters (zero-parameters), produces measurable predictions (derives-observables), and admits a scale hierarchy (self-similar).
background
The module addresses whether Recognition Science is the unique zero-parameter framework without circular assumptions. It defines FrameworkConstraints via four fields, each a Prop: non-static for time evolution, zero-parameters for absence of free parameters, derives-observables for production of measurable predictions, and self-similar for existence of a scale hierarchy. Any framework obeying these four must satisfy the Recognition Composition Law and therefore be isomorphic to RS.
proof idea
The declaration is a structure definition that directly introduces the four propositional fields. No lemmas or tactics are applied; the fields encode the constraints listed in the module documentation and the attached derivation chain comments.
why it matters
This structure supplies the non-circular starting point for the exclusivity argument. It supports downstream siblings such as RCLDerivation and exclusivity_cert_exists. The four constraints align with the forcing chain steps that force J-uniqueness, the phi fixed point, the eight-tick octave, and D=3. The module documentation notes that earlier NoAlternatives results pre-loaded the conclusion, which this definition avoids.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.