Necessary
plain-language theorem explainer
Necessary encodes modal necessity for properties of configurations in Recognition Science modal logic. Researchers working on cost-forced dynamics or S5 modal interpretations of physical necessity would cite it when stating that a property must hold in every reachable future. The definition is a direct universal quantification over the possibility set of the given configuration.
Claim. For a property $p$ of configurations and a configuration $c$, the necessity operator holds at $c$ if and only if $p(y)$ is true for every $y$ belonging to the possibility set $P(c)$ of reachable futures from $c$.
background
Configurations are points in recognition state space, formalized as a structure carrying a positive real value (generalizing bond multipliers), a natural-number time coordinate in ticks, and a logarithmic bound $|log(value)| ≤ 16$ that keeps values within physically relevant scales. ConfigProp is the type of predicates on these configurations. The possibility set Possibility c collects configurations reachable from c at finite J-cost, where J is the cost function induced by the Recognition Composition Law J(xy) + J(x/y) = 2J(x)J(y) + 2J(x) + 2J(y).
proof idea
As a definition it directly encodes the universal quantification over the possibility set: for all y in Possibility c, p y. No lemmas or tactics are invoked; the body is the primitive statement of necessity as forced by cost minimization.
why it matters
It supplies the necessity operator □ that pairs with Possible to implement the modal grammar of the framework. Downstream results invoke it in no_interaction_implies_additive (EntanglementGate) and bilinear_family_forced (Inevitability) to derive additive and bilinear forms, and in actual_has_zero_modal_distance and s5_actuality_implies_possibility (ModalOntologyStructure) to establish S5 properties. It fills the necessity half of the modal ontology step, aligning with the T5–T8 forcing chain where necessity corresponds to cost-minimization forcing.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.