Function propagateOperatorConstraints

Run constraint propagation to a fixed point over the operators the reader accepted, filling in variable values the granted steps force.

Only acceptances propagate. A rejection is not a truth value: it strikes the premise it lives in, and the caller excludes that premise here via options.excludedPremiseIds — so nothing inside a struck premise contributes, and no value is ever forced false by a refusal.

Each step merges what it forces into the variable's current value rather than overwriting it or declining to write, so two steps that force opposite values leave the variable CONTESTED instead of letting whichever step ran first decide. That merge is the join of the knowledge order, every rule's trigger is monotone in that same order, and the state space is finite — so the sweep converges to the least fixed point above the reader's assignment and reaches it whatever order premises, expressions and rules are visited in.

Each rule moves one truth component in one direction, and that is not decoration: an accepted A → B fires forward on A being told true and merges told-true into B, and backward on B being told false merging told-false into A. Transferring both components at once would read the conditional as a biconditional and derive B false from A false. The one-directional pairing is what a material implication licenses; only iff carries both components both ways.

Because only the told-true component travels forward, a contested variable can produce an uncontested true downstream and leave every aggregate fact reading clean. evaluateArgument reports contestedVariableIds so a conflict is never inferred from the aggregates. Attribution's counterfactual depends on that: withholding an assertion and re-closing must give one answer, and must not let mutually supporting premises certify each other.

A reader's own assertion takes part in the merge like any other source. If the reader asserts a value that a granted step contradicts, the result is CONTESTED — the conflict is reported, not silently resolved in either direction.

Axiomatic-bound variables are forced to true by ArgumentEngine's pre-pass before this function runs, and are merged on the same footing.