balancedEvent
plain-language theorem explainer
The balancedEvent definition constructs the canonical recognition event whose ratio is exactly 1. Researchers proving minimum-cost properties in the information ledger cite it as the zero-cost reference state. The definition is a direct constructor application that pairs the number 1 with its positivity witness.
Claim. Let $e_0$ be the recognition event with ratio $1$, where a recognition event is any positive real number that encodes a physical fact in the ledger.
background
A RecognitionEvent is the structure consisting of a positive real ratio together with a proof that the ratio exceeds zero. Every physical fact is thereby encoded as such a ratio $x > 0$, and its information content is the associated J-cost. The module states that J-cost vanishes precisely at $x = 1$, which is the balanced state carrying no encoded information.
proof idea
The definition is a one-line constructor application that supplies the ratio 1 and the positivity fact one_pos to inhabit the RecognitionEvent structure.
why it matters
This definition supplies the zero-cost reference required by the downstream theorems that establish the balanced state has minimum information cost and is the unique minimum. It realizes the IC-001 claim that the state $x = 1$ has J-cost zero, corresponding to perfect balance with no physical content in the Recognition Science ledger.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.