pith. machine review for the scientific record. sign in
structure definition def or abbrev high

RecognitionEvent

show as:
view Lean formalization →

RecognitionEvent encodes each physical fact as a positive real ratio x in the ledger, with its information content given by the J-cost J(x). Researchers constructing ledger models in Recognition Science cite this structure when building balanced event lists or deriving conservation laws. The declaration is a bare structure definition supplying the ratio field and its positivity witness to make J-cost well-defined.

claimA recognition event consists of a real number $x > 0$ together with a witness that $x > 0$.

background

The InformationIsLedger module identifies information with the physical ledger under IC-001. Every physical fact is represented by a recognition ratio whose information content is the J-cost J(x), zero precisely when x equals 1. Upstream, ObserverForcing.cost defines the cost of an event as Jcost e.state, while LedgerFactorization.of calibrates J on the positive reals and DomainBootstrap.required supplies the minimal structure needed to state the conditions.

proof idea

Direct structure definition with two fields: ratio of type ℝ and ratio_pos witnessing ratio > 0. No lemmas or tactics are invoked; the declaration simply introduces the type used by downstream ledger operations.

why it matters in Recognition Science

This structure supplies the basic ledger entry type consumed by LedgerForcing.add_event, add_event_balanced, and conservation_from_balance. It realizes the first core claim of IC-001 that every recognition ratio carries a definite non-negative J-cost, and it sits at the base of the forcing chain linking T5 J-uniqueness to the eight-tick octave and D = 3. It leaves open the explicit identification of J with the Recognition Composition Law.

scope and limits

formal statement (Lean)

  46structure RecognitionEvent where
  47  /-- The recognition ratio x > 0. -/
  48  ratio : ℝ
  49  /-- Positivity is required for J-cost to be well-defined. -/
  50  ratio_pos : ratio > 0
  51
  52/-- The information cost of a recognition event = J(x). -/

used by (40)

From the project-wide theorem graph. These declarations reference this one in their body.

… and 10 more

depends on (15)

Lean names referenced from this declaration's body.