RecognitionBridge
plain-language theorem explainer
RecognitionBridge decomposes a cost bridge into a recognizer map R from configurations to events, a strictly positive scale ι from events to reals, and a reference configuration. Researchers deriving state equivalence from zero defect would cite the structure when factoring costs for the identity chain in the RS ontology. The declaration is a direct structure definition whose fields enable the subsequent ratio and equivalence lemmas.
Claim. A recognition bridge from configurations $C$ to events $E$ consists of a recognizer $R: C → E$, a strictly positive scale $ι: E → ℝ$, and a reference configuration $c_{ref} ∈ C$.
background
In the RS ontology module, existence and truth arise as selection outcomes under the J-functional: RSExists holds when defect collapses to zero, and RSTrue requires existence plus stabilization along an orbit. CostBridge supplies the scalar map χ: C → ℝ with χ_pos, while RecognitionBridge refines it by inserting an observable recognizer R and embedding ι so that χ(c) equals the ratio ι(R(c))/ι(R(c_ref)). The defect functional, defined as J(x) for positive x, satisfies defect(1) = 0 and is invoked directly in the zero-cost equivalences.
proof idea
The structure is declared by its four fields R, ι, ι_pos, and c_ref. Ratio and pairRatio are immediate quotients of ι values; positivity follows from div_pos on ι_pos. Zero-cost equivalences apply defect_zero_iff_one to the pairRatio, then use div_eq_iff and div_self for the scale-equality direction, with injectivity hypotheses composed via hInj.
why it matters
The structure supplies the interface required for the event-space equivalence pipeline in Paper §3.1 (Eq. 15–17), converting zero defect of the pair ratio into equality of events under ι-injectivity and further into state equality under R-injectivity. It operationalizes the cost decomposition that links the abstract CostBridge to concrete recognition maps, supporting the reverse direction (identity implies zero cost) without injectivity assumptions. No downstream uses are recorded yet.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.