multiplicative_recognizer_L4
plain-language theorem explainer
Composition consistency (the d'Alembert / L4 law) is derived, not postulated, for recognizers whose event space is the positive reals. Recognition Core re-exports this as a public citation target at the T0/T4 layer. The declaration is a one-line abbrev of the inhabited L4-derivability certificate on multiplicative recognizers.
Claim. There exists a certificate that the fourth composition law (d'Alembert consistency) is derivable on the positive multiplicative event space $\mathbb{R}_{>0}$: for a multiplicative recognizer (geometric recognizer onto positives plus continuous comparator obeying the Law of Logic, with cost data), L4 follows from that data rather than being assumed as an axiom.
background
Recognition Core aggregates the T0/T4 recognition-geometry layer: recognizer, indistinguishability quotient, full signature, and completeness. The module's public list singles out this entry as the place where composition consistency is obtained on the multiplicative event space.
A multiplicative recognizer pairs a geometric recognizer with codomain ${x:\mathbb{R}\mid x>0}$, a continuous comparison operator on positives that satisfies the Law of Logic (the Aristotelian conditions), and the cost-functional data needed to force the fourth law automatically. L4 is the composition / d'Alembert consistency condition on that comparator; in the broader framework it is the same structural demand as the Recognition Composition Law on the J-cost.
Upstream, l4DerivableCert_inhabited states that for any carrier type the type of L4-derivability certificates is nonempty, by exhibiting the canonical certificate built from the multiplicative recognizer package.
proof idea
Pure re-export. The abbrev is definitionally the theorem that L4DerivableCert is inhabited for every carrier, i.e. a one-line pointer to MultiplicativeRecognizer.l4DerivableCert_inhabited, which itself packages the constructive witness l4DerivableCert. No local tactics or algebraic work occur in this file.
why it matters
Closes the public story that the d'Alembert composition law is a theorem on the positive multiplicative event space, not an extra postulate. That is the Recognition Composition Law landmark at the recognizer layer: once the comparator and cost data of a multiplicative recognizer are fixed, L4 is forced. The module places this beside recognizer-induces-logic and the recognition lattice, so downstream lattice and signature work can cite a single Core name rather than the Foundation path. No used_by edges are recorded yet; the value is the stable citation surface for the paper-upgrade L4 certificate inside the forcing chain's early geometry.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.