MultiplicativeL4
The definition MultiplicativeL4 encodes the multiplicative form of composition consistency (L4) for recognizers whose event space is the positive reals. Researchers deriving logic from recognition costs would cite it when establishing route independence under multiplication and division. It directly states the existence of a combiner P such that the sum of costs on a product and a quotient equals P applied to the two separate costs.
claimLet $m$ be a multiplicative recognizer on positive reals equipped with a continuous comparison operator satisfying the laws of logic. Then there exists a function $P : ℝ → ℝ → ℝ$ such that for all positive reals $x, y$, the induced cost of $xy$ plus the induced cost of $x/y$ equals $P$ applied to the induced cost of $x$ and the induced cost of $y$.
background
This module supplies the honest conditional version of (L4) Composition Consistency once the event space is restricted to positive reals under multiplication. A MultiplicativeRecognizer pairs a geometric recognizer onto {x : ℝ // 0 < x} with a continuous ComparisonOperator whose comparator satisfies all four Aristotelian conditions plus scale invariance and non-triviality. The cost function is obtained by derivedCost on that comparator, so cost(r) records the comparison of r against 1. The module documentation states that the equality-induced cost fails (L4) on (ℝ>0, ·), but the Law-of-Logic cost yields the d'Alembert route-independence equation with a polynomial combiner of total degree at most two. Upstream results include the cost definition from ObserverForcing and the ledger factorization structure from DAlembert.LedgerFactorization.
proof idea
As a definition, MultiplicativeL4 directly introduces the predicate by writing the existential statement over the combiner P and the functional equation on the three costs. No lemmas or tactics are invoked inside the definition itself; it simply packages the route-independence condition that the downstream theorem multiplicativeRecognizer_satisfies_L4 later proves holds for every MultiplicativeRecognizer.
why it matters in Recognition Science
MultiplicativeL4 supplies the precise target predicate for the theorem multiplicativeRecognizer_satisfies_L4, which shows that every such recognizer automatically satisfies the multiplicative form of (L4). It thereby converts the abstract RecognizerComposition hypothesis from RecognizerInducesLogic into a derived result once the carrier is multiplicative and the comparator obeys the laws of logic. In the Recognition Science framework this step closes the gap between the general composition law and the concrete d'Alembert form that appears in the paper's unification of geometry and logic.
scope and limits
- Does not assert that the equality-induced cost satisfies (L4) on positive reals.
- Does not claim (L4) for recognizers whose event space is not the positive reals under multiplication.
- Does not construct or exhibit the explicit combiner P.
- Does not address non-continuous comparators or carriers lacking the Law of Logic.
formal statement (Lean)
90def MultiplicativeL4 (m : MultiplicativeRecognizer 𝒞) : Prop :=
proof body
Definition body.
91 ∃ P : ℝ → ℝ → ℝ,
92 ∀ x y : ℝ, 0 < x → 0 < y →
93 m.cost (x * y) + m.cost (x / y) = P (m.cost x) (m.cost y)
94
95/-- A polynomial-degree-2 form of (L4): the combiner is a polynomial of
96total degree at most two. This is the form the d'Alembert Inevitability
97Theorem produces. -/