structure
definition
def or abbrev
RecognitionEvent
show as:
view Lean formalization →
formal statement (Lean)
40structure RecognitionEvent where
41 source : ℕ
42 target : ℕ
43 ratio : ℝ
44 ratio_pos : 0 < ratio
45 deriving DecidableEq
46
47/-- The reciprocal event: B recognizes A with inverse ratio. -/
used by (40)
-
add_event -
add_event_balanced -
add_event_balanced_list -
balanced_list -
conservation_from_balance -
event_cost -
flow_contribution -
flow_contribution_reciprocal -
Ledger -
ledger_forcing_principle -
paired_log_sum_zero -
reciprocal -
reciprocal_eq_iff -
reciprocal_inj -
reciprocal_reciprocal -
reciprocity -
CoherentRecognition -
cooper_paired_reference_yields_observer -
cooper_pairing_yields_persistent -
cost -
cost_nonneg -
identity -
identity_cost -
identity_persistent -
IsPersistent -
nontrivial_recognition_forces_observer -
observer_forcing_certificate -
observer_forcing_status -
persistent_event_state_eq_identity -
persistent_state_unique