Counterfactual
plain-language theorem explainer
Counterfactuals collect reachable configurations from a given state that were not selected by actualization and carry strictly higher J-cost. Recognition theorists analyzing why certain futures remain unrealized would cite this when separating realized paths from higher-cost alternatives. The definition is a direct set comprehension over the possibility membership, inequality to Actualize, and the J comparison.
Claim. For a configuration $c$, the set of counterfactuals is defined as the collection of all $y$ such that $y$ belongs to the possibility space of $c$, $y$ differs from the actualized successor of $c$, and the cost $J$ evaluated at the value of $y$ strictly exceeds the cost $J$ at the value of the actualized successor.
background
Config is a simplified point in recognition state space carrying a positive real value (generalizing bond multiplier), a time coordinate in ticks, and a log-bound constraint ensuring physical scale. J is the fundamental cost function $J(x) = (x + x^{-1})/2 - 1$, the unique functional satisfying d'Alembert factorization plus normalization. Actualize selects the J-minimizing successor from the possibility set of its argument, serving as the deterministic bridge from possibility to realized state. The local setting is modal logic development inside Recognition Science, where possibility is the transitive closure of the reachability relation and actualization is cost-driven selection.
proof idea
The definition is a direct set comprehension that filters configurations satisfying three conditions: membership in the possibility set of c, distinctness from the actualized state, and strictly greater J value.
why it matters
This definition supports downstream derivations of life-ignition rungs and exact fermionic half-gap equalities by formalizing the distinction between realized and unrealized higher-cost paths. It connects directly to J-uniqueness (T5) and the actualization step in the forcing chain. It is referenced in the animal complexity bound at rung 19 and in the D=3 cosmological gap calculation.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.