module module high

`IndisputableMonolith.Foundation.MultiplicativeRecognizerL4`

MultiplicativeRecognizerL4 defines the multiplicative recognizer on positive reals equipped with a continuous comparison operator satisfying the Law of Logic. It pairs geometric recognizer data with cost-functional data to enable automatic derivation of L4. Researchers constructing the Recognition Science forcing chain cite this module for the multiplicative event space. The module assembles imported results from LogicAsFunctionalEquation, RecognizerInducesLogic, and PrimitiveDistinction without introducing new proofs.

claimLet $\mathcal{E}=\mathbb{R}_{>0}$. A multiplicative recognizer is a recognizer $r:\mathcal{C}\to\mathcal{E}$ equipped with a continuous comparison operator on $\mathcal{E}$ that satisfies the Law of Logic, paired with the cost-functional data required to derive (L4) automatically.

background

Recognition Science starts from a single functional equation on recognizers that map configurations to events. This module specializes the general recognizer to the multiplicative case whose event space is the positive reals. It relies on the unification result that any recognizer automatically generates a Law-of-Logic realization on its event space, as stated in the companion paper RS_Recognition_Geometry_Logic_Unification.tex.

proof idea

this is a definition module, no proofs

why it matters in Recognition Science

The module supplies the multiplicative recognizer structure required by the root IndisputableMonolith module to expose the master forcing-chain theorem. It completes the foundation layer for deriving L4 on the multiplicative event space and feeds directly into the T0-T8 chain.

scope and limits

Does not prove the Law of Logic from first principles.
Does not treat non-multiplicative event spaces.
Does not derive physical constants or mass ladders.
Does not contain numerical verification or simulation code.

used by (1)

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

IndisputableMonolith module_import

depends on (3)

Lean names referenced from this declaration's body.

IndisputableMonolith.Foundation.LogicAsFunctionalEquation module_import
IndisputableMonolith.Foundation.PrimitiveDistinction module_import
IndisputableMonolith.Foundation.RecognizerInducesLogic module_import

declarations in this module (13)

structure MultiplicativeRecognizer L63
def cost L78
theorem cost_def L81
def MultiplicativeL4 L90
def MultiplicativeL4Polynomial L98
theorem multiplicativeRecognizer_satisfies_L4_polynomial L111
theorem multiplicativeRecognizer_satisfies_L4 L122
theorem L4_derivable_on_multiplicative_event_space L133
theorem multiplicative_identity L149
theorem multiplicative_reciprocal_symmetry L156
structure L4DerivableCert L185
def l4DerivableCert L200
theorem l4DerivableCert_inhabited L206