Pith. sign in
module module high

IndisputableMonolith.Foundation.MultiplicativeRecognizerL4

show as:
view Lean formalization →

Defines the multiplicative recognizer: event space ℝ>0 with continuous comparison obeying the Law of Logic, paired with cost-functional data. Shows that (L4) and its polynomial form hold automatically on this space via identity and reciprocal symmetry. RecognitionCore imports it as the concrete L4 instance at the recognizer layer. Argument is structure plus direct algebraic verification of the L4 identities.

claimA multiplicative recognizer is a recognizer whose event space is $\mathbb{R}_{>0}$, with a continuous comparison operator satisfying the Law of Logic, together with cost-functional data. On this space the identity $J(1)=0$ and reciprocal symmetry $J(x)=J(x^{-1})$ hold, and both the Law-of-Logic axiom (L4) and its polynomial form are derived automatically.

background

Recognition Geometry treats a recognizer as a map from configurations to an event space $\mathcal{E}$, inducing a Law-of-Logic realization on $\mathcal{E}$ (RecognizerInducesLogic). The companion paper argues any such recognizer generates that realization; this module specializes to the multiplicative case.

The event space is the positive reals $\mathbb{R}_{>0}$. Comparison is continuous and obeys the Law of Logic functional equation (from LogicAsFunctionalEquation). Cost data is the J-cost $J(x)=(x+x^{-1})/2-1$ (T5 uniqueness), which is the natural cost on multiplicative ratios.

PrimitiveDistinction supplies the underlying distinction structure. The module packages geometric recognizer data with cost-functional data so that (L4) is not an extra axiom but a derived identity on this event space.

proof idea

Definition module with supporting lemmas, not a single theorem. It introduces the MultiplicativeRecognizer structure (event space $\mathbb{R}_{>0}$, continuous comparison, cost), then verifies multiplicative identity $J(1)=0$ and reciprocal symmetry $J(x)=J(x^{-1})$.

From those, MultiplicativeL4 and MultiplicativeL4Polynomial are obtained by direct algebraic expansion of the RCL-style identities. Certificates (L4DerivableCert) package the derivability claim for downstream use. No deep tactic proof: the work is structure design plus routine cost identities.

why it matters in Recognition Science

Feeds RecognitionCore, the public aggregator at the T0/T4 layer of the forcing chain: recognizer, indistinguishability quotient, full recognition signature, and completeness. RecognitionCore is the formal answer to why a single Boolean observable is atomic but not complete.

This module supplies the concrete multiplicative instance where (L4) is automatic rather than postulated. That closes the gap between abstract recognizer-induces-logic (RecognizerInducesLogic) and the cost-functional side used in T5 J-uniqueness and the Recognition Composition Law. Downstream signature and completeness arguments can cite L4 as derived on $\mathbb{R}_{>0}$ rather than assumed.

scope and limits

used by (1)

From the project-wide theorem graph. These declarations reference this one in their body.

depends on (3)

Lean names referenced from this declaration's body.

declarations in this module (16)