rs_true_neg_imp_neg_rs_true
plain-language theorem explainer
RS-truth excludes its own negation: if the negated predicate stabilizes under the recognition dynamics and cost bridge, the original predicate cannot be stable. Researchers deriving Boolean properties of RS-truth in the ontology module cite this when establishing negation laws. The term proof derives a direct contradiction by equating the predicate value at the stable configuration to both true and false.
Claim. Let $C$ be a type of configurations, let $bridge$ map configurations to positive reals with the cost structure, let $B$ be a dynamics map on $C$, let $c_0$ and $c_*$ be configurations, and let $P$ be a predicate on $C$. If the negation of $P$ holds at the stable configuration $c_*$ (where defect vanishes), the negated predicate evaluates to true there, and it stabilizes along the orbit of $B$ from $c_0$ to $c_*$, then $P$ itself does not hold at $c_*$ under the same conditions.
background
In the RS ontology, truth is an operational outcome of cost minimization: a predicate $P$ is RS-true when the target configuration has zero defect under the cost bridge, $P$ evaluates to true there, and $P$ stabilizes along the orbit of the dynamics $B$ from seed $c_0$ to that target. The CostBridge structure supplies the positive scalar map needed for defect calculations, while RSTrue packages existence, evaluation, and stabilization into a single Prop. This setting replaces primitive truth with verifiable selection under the J-cost functional. The upstream CPM2D bridge supplies a concrete fluid-model instance of the cost map, confirming the general result applies to discretized physical configurations.
proof idea
The term proof introduces the two RSTrue assumptions, each carrying a triple that includes the Boolean value of the predicate at the stable point. Simplification extracts that the negated predicate is true at that point, hence the original predicate is false there. Rewriting this equality into the second assumption produces true = false, which is discharged directly by the Boolean lemma false_ne_true.
why it matters
This implication supplies the forward direction for the biconditional rs_true_neg_iff_neg_rs_true once RS-decidability is assumed, completing the Boolean negation law inside the ontology module. It reinforces the selection rule that truth corresponds to stabilization under cost minimization, without presupposing classical logic primitives. In the Recognition framework it supports deriving logical structure from the J-uniqueness and forcing chain, closing one step toward consistent RS-decidability for predicates.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.