Foundation Multiplicative Recognizer L4 Multiplicative Reciprocal Symmetry

Reciprocal symmetry

In mathematics, a function is symmetric under reciprocation if it assigns the same value to a positive number and to its reciprocal. For a cost function that measures the effort of comparing two quantities, this symmetry says the effort of comparing a ratio x to 1 is the same as the effort of comparing 1/x to 1. The declaration establishes that this symmetry holds automatically for a specific class of cost functions built from a continuous comparison operator satisfying the Law of Logic.

The classical background is the d'Alembert functional equation, named after Jean le Rond d'Alembert's 1747 work on vibrating strings. The equation F(xy) + F(x/y) = P(F(x), F(y)) expresses route independence: the cost of comparing x and y through multiplication and division does not depend on the path taken. In the framework, this equation is the multiplicative form of composition consistency (L4), and it holds for any recognizer whose event space is the positive reals under multiplication, equipped with a continuous comparison operator satisfying the Law of Logic.

In Recognition Science, the framework's account of how reality keeps a discrete record of events, a recognizer assigns costs to comparisons. The declaration multiplicative_reciprocal_symmetry proves that for any such recognizer on positive reals with a Law-of-Logic-satisfying comparator, the derived cost satisfies m.cost x = m.cost (x⁻¹) for all positive x. This is a theorem in the machine-checked library of formal theorems, derived from the comparator's properties, not an assumption.

The result is conditional, not universal. The equality-induced cost on the positive reals, which assigns zero on the diagonal and a positive weight elsewhere, fails to satisfy composition consistency (L4). The theorem holds only for recognizers paired with a continuous comparison operator satisfying the Law of Logic. The symmetry is a consequence of the comparator's non-contradiction and scale invariance properties, not a property of every possible cost function.

What this establishes is that reciprocal symmetry is not a separate postulate but a derived consequence of the multiplicative structure and the Law of Logic. It strengthens the framework's claim that the cost of recognition is forced, not chosen: once the event space and comparator are fixed, the symmetry follows. This matters because it narrows the class of admissible cost functions and supports the framework's broader derivation of physical constants from the forcing chain.

/-- **(L2) Reciprocal symmetry.** The derived cost is symmetric under
reciprocation, a consequence of non-contradiction plus scale invariance. -/
theorem multiplicative_reciprocal_symmetry
    (m : MultiplicativeRecognizer 𝒞) :
    ∀ x : ℝ, 0 < x → m.cost x = m.cost (x⁻¹) := by
  intro x hx
  show m.comparator x 1 = m.comparator (x⁻¹) 1
  -- C(x, 1) = C(1, x) (non-contradiction) = C(x⁻¹, 1) (scale by x⁻¹)
  have hsymm : m.comparator x 1 = m.comparator 1 x :=
    m.laws.non_contradiction x 1 hx (by norm_num)
  have hxinv : (0 : ℝ) < x⁻¹ := inv_pos.mpr hx
  have hscale : m.comparator (x⁻¹ * x) (x⁻¹ * 1) = m.comparator x 1 :=
    m.laws.scale_invariant x 1 (x⁻¹) hx (by norm_num) hxinv
  -- (x⁻¹ * x) = 1 and (x⁻¹ * 1) = x⁻¹
  have hxx : x⁻¹ * x = 1 := inv_mul_cancel₀ (ne_of_gt hx)
  rw [hxx, mul_one] at hscale
  -- so C(1, x⁻¹) = C(x, 1)
  -- chain: C(x, 1) = C(1, x) (above), and C(1, x⁻¹) = C(x, 1) gives
  -- C(1, x) and C(1, x⁻¹) both equal C(x, 1)... use non-contradiction on x⁻¹
  have hsymm2 : m.comparator (x⁻¹) 1 = m.comparator 1 (x⁻¹) :=
    m.laws.non_contradiction (x⁻¹) 1 hxinv (by norm_num)
  rw [hsymm2, ← hscale]

/-- **L4 is automatic in the abstract form for any multiplicative recognizer.**

The polynomial form trivially gives the existence form. -/
theorem multiplicativeRecognizer_satisfies_L4
    (m : MultiplicativeRecognizer 𝒞) :
    MultiplicativeL4 m := by
  obtain ⟨P, _, _, hroute⟩ := multiplicativeRecognizer_satisfies_L4_polynomial m
  exact ⟨P, hroute⟩

/-- **L4 is automatic in the abstract form for any multiplicative recognizer.**

The polynomial form trivially gives the existence form. -/
theorem multiplicativeRecognizer_satisfies_L4
    (m : MultiplicativeRecognizer 𝒞) :
    MultiplicativeL4 m := by
  obtain ⟨P, _, _, hroute⟩ := multiplicativeRecognizer_satisfies_L4_polynomial m
  exact ⟨P, hroute⟩

What this page does not claim

The theorem does not claim that every recognizer satisfies reciprocal symmetry; the equality-induced cost on the positive reals is a counterexample. The theorem does not derive the fine-structure constant alpha or any specific physical constant value. The theorem does not prove the Riemann Hypothesis; it only establishes a structural equivalence for the multiplicative case.

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: