IndisputableMonolith.Foundation.MaximalForcing.IndependenceWitness
Defines an explicit countermodel pair that witnesses independence of a claim over an admissible class. Anyone classifying claims in a maximal-forcing closure cites this when a statement is neither forced nor selected. The module packages the witness type and the predicate that a claim is independent relative to that pair; no deep proof work lives here.
claimAn independence witness is an explicit countermodel pair $(M_+, M_-)$ over an admissible class such that a claim $C$ holds in one realization and fails in the other. A claim is independent of the witness when both sides of the pair are admissible and disagree on $C$.
background
Maximal forcing organizes Recognition Science claims by a closure operator: the set of statements currently targeted by a primitive in a chosen universe of realizations. Completeness requires every claim in that closure to be tagged forced, independent, or selected (the last only temporarily).
Independence is not a residual bin. It is discharged by an explicit countermodel pair over the admissible class: two realizations that both satisfy the ambient constraints yet disagree on the claim. That pair is the mathematical content of this module.
Upstream, ForcingClosure supplies the claim set under classification. Downstream classification work consumes the witness when demoting a selected claim or recording that a statement cannot be forced.
proof idea
This is a definition module. It introduces the witness structure (the countermodel pair) and the independence predicate relative to that pair. No substantial theorems are proved here; the argument structure is type-and-predicate packaging for use by claim-classification modules.
why it matters in Recognition Science
ForcedInvariant (claim classification) requires every closure target to end as forced, independent, or selected. Selected is temporary: it must be promoted by a deeper admissibility condition or demoted by countermodel. This module supplies the countermodel side of that fork.
Without an explicit witness type, independence would be an informal residual rather than a checkable status in the forcing program. The module therefore sits on the path that closes the maximal-forcing ledger: every claim either forced by the Recognition chain (T0–T8 and related constraints) or honestly independent via a named pair of admissible realizations.
scope and limits
- Does not prove any particular claim is independent; only defines the witness shape.
- Does not construct concrete countermodels for physics constants or ladder parameters.
- Does not classify forced or selected claims; that lives in ForcedInvariant.
- Does not enlarge or compute the forcing closure itself.