Foundation Multiplicative Recognizer L4 Multiplicative Identity

The multiplicative identity

In mathematics, an identity element is a number that leaves others unchanged under an operation. For multiplication, that number is 1: multiplying any positive number by 1 gives the number back. A cost function, in the Recognition Science framework, assigns a nonnegative number to the effort of distinguishing two events. The declaration multiplicative_identity states that this cost is zero when the two events are the same, specifically at the multiplicative identity 1. It proves that the derived cost of comparing 1 with itself is exactly 0.

The theorem is a conditional one. It applies to a multiplicative recognizer, which is a structure pairing a geometric recognizer on positive real numbers with a continuous comparison operator that satisfies the Law of Logic. The Law of Logic is a set of conditions including identity, non-contradiction, and scale invariance. The proof of multiplicative_identity is direct: it uses the identity condition of the comparator to show that the cost at 1 is 0. This is a theorem in the machine-checked library of formal theorems, not an assumption.

What this declaration does not claim is broader. It does not state that all recognizers have zero cost at 1. The equality-induced cost on positive reals fails this property in general. The theorem only holds for the specific multiplicative recognizer structure with a Law-of-Logic-satisfying comparator. It also does not imply that the cost function is uniquely determined; other conditions are needed for that. The declaration is a building block, not a complete theory.

/-- **(L1) Identity.** The derived cost vanishes at the multiplicative
identity. -/
theorem multiplicative_identity (m : MultiplicativeRecognizer 𝒞) :
    m.cost 1 = 0 := by
  show m.comparator 1 1 = 0
  exact m.laws.identity 1 (by norm_num)

What this page does not claim

The theorem does not apply to recognizers with equality-induced cost on positive reals. It does not claim that all recognizers satisfy the identity condition. It does not determine the full form of the cost function.

Verify this page

Every tagged claim above names its theorem. To check one yourself rather than trust this page, elaborate the source module with Lean 4 and audit its axiom basis:

$ lake env lean IndisputableMonolith/Foundation/MultiplicativeRecognizerL4.lean
expected axiom basis: [propext, Classical.choice, Quot.sound] (the Lean kernel's standard three; no RS-specific axioms)

A page whose claims cannot be reproduced this way does not ship. In production, every anchor links to the exact declaration in the public source release, and this block carries the build receipt for the page itself.

Derived articles

This page is generated by a question-recursion engine: the questions its answers raise become the next pages. The current agenda, with open targets marked red: