RecognitionEvent
plain-language theorem explainer
RecognitionEvent packages a source agent, target agent, and positive real ratio into a single object equipped with decidable equality. It supplies the atomic datum for the ledger forcing construction that derives double-entry bookkeeping from J-symmetry. The structure is introduced directly as a plain record with a positivity field and no further proof obligations.
Claim. A recognition event is a tuple $(s, t, r)$ where $s, t$ are natural numbers (agents), $r > 0$ is a real ratio, equipped with decidable equality.
background
The LedgerForcing module shows that J-symmetry forces double-entry ledger structure. RecognitionEvent extends the simpler positive-state event from ObserverForcing and the positive-ratio event from InformationIsLedger by adding explicit source and target agents. The reciprocal operation, defined in the same module, swaps source and target while inverting the ratio, using the reciprocal automorphism from CostAlgebra.
proof idea
This is a structure definition with no proof body. It declares the four fields and derives DecidableEq automatically.
why it matters
RecognitionEvent supplies the data type underlying the ledger forcing principle. It is consumed by add_event, add_event_balanced_list, and conservation_from_balance to enforce that every event is paired with its reciprocal, yielding net flow zero. The definition realizes the passage from J-symmetry (T5) to the double-entry constraint that produces conservation laws inside the Recognition Science framework.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.