modal_K
plain-language theorem explainer
The distribution property of modal necessity holds over configuration properties: if an implication between two properties is necessary at a configuration, and the antecedent property is necessary, then the consequent is necessary. Modal logicians and Recognition Science researchers developing possibility spaces would cite this as the standard K axiom instantiated in the configuration model. The proof is a direct term-mode unfolding that instantiates the universal quantifier definition of □ at an arbitrary future configuration.
Claim. Let $p$ and $q$ be properties of configurations and let $c$ be a configuration. If the necessity of the implication $p$ implies $q$ holds at $c$, and the necessity of $p$ holds at $c$, then the necessity of $q$ holds at $c$, where necessity of a property $r$ at $c$ means $r$ holds at every possible future configuration of $c$.
background
In the Modal.Possibility module, a configuration is a point in recognition state space given by the structure with a positive real value, a time coordinate in natural numbers, and a logarithmic bound ensuring physical scale. ConfigProp is the abbreviation for the type of properties from configurations to propositions. The necessity operator is defined so that a property is necessary at a configuration precisely when it holds in all possible futures of that configuration, with the interpretation that necessity corresponds to being forced by cost minimization.
proof idea
The term proof introduces the two hypotheses that the necessity of the implication and the necessity of the antecedent hold at the given configuration. It then takes an arbitrary future configuration and applies the implication (which holds at that future) to the antecedent fact (which also holds at that future) to obtain the consequent at the future. This establishes necessity of the consequent at the original configuration.
why it matters
This theorem supplies the K axiom for the modal logic of possibility over configurations, a basic distribution law required for any further modal reasoning in the Recognition Science framework. No immediate parent theorems or downstream uses are recorded, and the result sits apart from the T0-T8 forcing chain. The accompanying comment notes that the stronger T axiom fails because a configuration lies outside its own possibility set, indicating an open direction for weaker temporal modalities.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.