RecognitionEvent
plain-language theorem explainer
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.
Claim. A 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
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.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.