Foundation Primitive Recognition Calculus Prcjcost Canonical Rcl Surface

The rational surface

The composition law is a rule that ties together the cost of two separate events and the cost of their combined or compared result. In the Recognition Science framework, the canonical cost function is J(q) = ((q + 1/q) / 2) - 1, where q is a positive ratio. The declaration canonical_rcl_surface establishes, in a machine-checked library of formal theorems, that this formula satisfies the composition law for all nonzero rational numbers. In plain terms: if you take two rational ratios, compute J for each, and also compute J for their product and their quotient, the two sides of the composition rule balance exactly.

The proof is algebraic and discrete. It works on rational numbers, not on all real numbers. The declaration does not establish that J is the only cost function satisfying the law. That uniqueness statement is a separate, continuous theorem, which the library bridges to but does not derive from this rational surface. The rational result is a necessary check, not the full classification.

In Recognition Science, this rational surface is the discrete foundation. The framework models recognition as a ledger of discrete events, and the cost of recognition is forced by the composition law. The rational proof shows the formula is consistent on the exact fractions that arise from discrete orbits. It also respects normalization: reducing a ratio by its greatest common divisor does not change the cost. This matters because the discrete ledger should not depend on how a ratio is represented.

The declaration does not claim to classify all possible cost functions on rationals. That remains an open target, named in the library as PRCNativeCostUniquenessTarget. The rational surface is a stepping stone, not the destination. What it does establish is that the canonical formula is a valid solution on the rational grid, and that this grid connects honestly to the continuous uniqueness theorem that the framework relies on.

/-- Canonical PRC J-cost satisfies the RCL algebraically on nonzero ratio
orbits. This is the rational surface of the composition law, not the
continuous-real uniqueness theorem. -/
theorem canonical_rcl_surface {x y : RatioOrbit}
    (hx : x.toRat ≠ 0) (hy : y.toRat ≠ 0) :
    RatioOrbit.crossEq (rclLHS x y) (rclRHS x y) := by
  rw [RatioOrbit.crossEq_iff_toRat_eq]
  unfold rclLHS rclRHS
  rw [RatioOrbit.add_toRat, RatioOrbit.add_toRat, RatioOrbit.add_toRat,
    RatioOrbit.mul_toRat, RatioOrbit.mul_toRat, RatioOrbit.mul_toRat,
    RatioOrbit.mul_toRat,
    onRatioOrbit_toRat, onRatioOrbit_toRat, onRatioOrbit_toRat,
    onRatioOrbit_toRat, div_toRat]
  simp [two_toRat]
  rw [RatioOrbit.mul_toRat]
  have hxy : x.toRat * y.toRat ≠ 0 := mul_ne_zero hx hy
  field_simp [hx, hy, hxy]
  ring_nf

/-- Normalizing a ratio representative by native orbit GCD preserves the PRC
cost. -/
theorem normalized_invariant (q : RatioOrbit) :
    RatioOrbit.crossEq (onRatioOrbit q)
      (onRatioOrbit (DistinctionNat.normalizeRatio q)) := by
  rw [RatioOrbit.crossEq_iff_toRat_eq]
  rw [onRatioOrbit_toRat, onRatioOrbit_toRat, DistinctionNat.normalizeRatio_toRat]

What this page does not claim

This answer does not claim that the rational surface alone classifies all cost functions. This answer does not claim that the composition law is established for all real numbers by this declaration. This answer does not claim that the rational surface is the same as the continuous uniqueness theorem.

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/PrimitiveRecognitionCalculus/PRCJCost.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: