Foundation Logic Realization Positive Ratio Has Identity Step

The identity step

In the Recognition Science framework, a comparison is a way of assigning a cost to the act of recognizing one thing as another. The framework's founding theorem forces this cost to take a specific form, and from that form a chain of results derives constants and dimensions. Before any of that can happen, the framework needs a starting point: a distinguished element, the identity, and a step that moves away from it. The declaration positiveRatio_hasIdentityStep is the machine-checked proof that this starting point always exists for the continuous, positive-ratio setting.

In plain terms, the theorem states: for any comparison operator on positive real numbers that satisfies the Laws of Logic, there exists some element whose comparison cost with the identity is not zero. The proof is short because it leans on a more general fact. Any realization of the framework's LogicRealization structure that is nontrivial, meaning it has more than one element, automatically has an identity step. The continuous positive-ratio realization is nontrivial, so the identity step follows. The declaration is a theorem in the machine-checked library of formal theorems, meaning its proof has been verified by a computer and requires no additional axioms beyond the standard logical ones.

What this step buys is the ability to build arithmetic. The identity step feeds into a separate construction that folds a sequence of steps into the positive real numbers, producing a copy of the natural numbers inside the carrier. A companion theorem proves this embedding is injective, so the arithmetic does not collapse: distinct steps land on distinct positive reals. The identity step is thus the hinge that connects the abstract comparison structure to the concrete numbers that later derivations use.

The declaration does not claim that the identity step is unique, nor does it identify which specific positive real serves as the step generator. It also does not assert that the arithmetic extracted is the only possible one, or that the framework's full forcing chain is complete. The theorem is a scaffolding result, not a destination: it secures the foundation on which the framework's later, more dramatic conclusions are built.

/-- The continuous positive-ratio realization satisfies the abstract
identity-step predicate. -/
theorem positiveRatio_hasIdentityStep
    (C : ComparisonOperator) (h : SatisfiesLawsOfLogic C) :
    (ofPositiveRatioComparison C h).hasIdentityStep :=
  hasIdentityStep_of_nontrivial _

theorem hasIdentityStep_of_nontrivial (R : LogicRealization) :
    R.hasIdentityStep :=
  R.nontrivial

/-- The continuous positive-ratio orbit interpretation is injective. -/
theorem positiveRatio_interpret_injective
    (C : ComparisonOperator) (h : SatisfiesLawsOfLogic C) :
    Function.Injective (positiveRatioOrbitInterpret C h) := by
  intro a b hab
  have hval := congrArg Subtype.val hab
  rw [positiveRatioOrbitInterpret_val, positiveRatioOrbitInterpret_val] at hval
  exact ArithmeticFromLogic.embed_injective
    (ArithmeticFromLogic.generatorOfLawsOfLogic h) hval

What this page does not claim

The identity step is unique or that a specific generator is identified. The extracted arithmetic is the only possible arithmetic for the carrier. The full Universal Forcing chain is completed by this declaration alone.

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/LogicRealization.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: