RCLDerivation
plain-language theorem explainer
The RCLDerivation structure packages the four-step chain that derives the Recognition Composition Law from zero-parameter constraints on dynamics, observables, and self-similarity. Researchers auditing uniqueness claims for Recognition Science cite it when replacing circular pre-loads of the conclusion with a constraint-only argument. The definition is a direct packaging of four proposition fields plus a trivial completeness implication.
Claim. A derivation of the Recognition Composition Law consists of four propositions asserting a universal cost function, d'Alembert dynamics, uniqueness of the J-cost function, and forcing of Recognition Science, together with the implication that these four assertions entail completeness of the derivation chain.
background
The module establishes non-circular exclusivity for Recognition Science by showing that any framework meeting non-static dynamics, zero free parameters, observable predictions, and self-similarity must obey the Recognition Composition Law. This replaces earlier proofs that pre-loaded the conclusion through RSConnectionData. The structure collects the intermediate logical steps without assuming the target law in advance.
proof idea
This is a structure definition that declares the four proposition fields and the chain_complete implication directly. No lemmas or tactics are invoked; the definition functions as a container. The companion theorem rcl_chain_is_valid instantiates it by setting every step to True and the implication to trivial.
why it matters
The structure supplies the non-circular packaging of the RCL derivation that feeds the ExclusivityCert, which asserts existence of a unique nonnegative J-cost vanishing at 1. It closes Gap 1 by deriving the Recognition Composition Law from constraints alone, supporting the claim that Recognition Science is the unique zero-parameter framework. It aligns with the T0-T8 forcing chain and the central role of the RCL as the functional equation.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.