IndisputableMonolith.Foundation.MaximalForcing.IndependenceWitness
Packages an explicit countermodel pair that witnesses independence of a claim over an admissible class. Claim classifiers in the maximal forcing program cite it when a target is not forced. It sits between the forcing-closure claim set and the forced/independent/selected taxonomy. Content is definitional: a witness structure plus a predicate that a claim is independent relative to that witness.
claimAn independence witness is an explicit countermodel pair $(M_0,M_1)$ over an admissible class such that a claim $C$ holds in one realization and fails in the other, so $C$ is independent of the forcing closure rather than forced by it.
background
Maximal forcing works on a closure: the claim set currently targeted by a primitive in a chosen universe of realizations. Upstream, ForcingClosure states that the program is complete only when every claim in that closure is classified as forced, independent, or selected with a named principle scheduled for tightening.
Independence is the branch that needs a concrete countermodel, not a uniqueness proof. This module supplies that apparatus: a pair of admissible realizations that disagree on the claim. The surrounding framework is the RS forcing chain (unique $J$, $\varphi$, eight-tick octave, $D=3$), where each structural claim must eventually be forced or honestly marked independent.
proof idea
This is a definition module, not a theorem file. It introduces a witness type (an explicit countermodel pair for a claim over an admissible class) and a predicate relating a claim to such a witness. No forcing or uniqueness argument is proved here; downstream classifiers consume the definitions when tagging a closure member independent.
why it matters in Recognition Science
Feeds the claim-classification layer (ForcedInvariant): every claim in a closure target must be forced, independent, or selected. Downstream doc-comment: Selected is temporary and must be promoted to forced by a deeper admissibility condition or demoted to independent by countermodel. This module is the demotion side: it names the countermodel pair that justifies an independent tag. Without it, the maximal-forcing ledger cannot close the independent branch of the taxonomy that sits above the T5–T8 forcing landmarks.
scope and limits
- Does not prove any particular physics claim is independent.
- Does not construct concrete numerical or geometric countermodels.
- Does not auto-discharge Selected tags in a closure.
- Does not change membership or completeness of a forcing closure.
- Does not establish forced uniqueness for J, phi, octave, or D=3.