IndependenceWitness
plain-language theorem explainer
An independence witness packages two admissible realizations that disagree on a reality claim: one where the claim holds and one where it fails. Researchers classifying claims under maximal forcing cite it when a proposition is not forced by the admissible class. The declaration is a structure definition, the data carrier for the independent branch of claim classification, not a proved theorem.
Claim. Given a claim universe $U$ and a reality claim $C$ on its realizations, an independence witness consists of two admissible realizations $R_+$ and $R_-$ such that $C$ holds at $R_+$ and fails at $R_-$.
background
In the maximal-forcing layer, a claim universe bundles a type of realizations, an admissibility class, and a set of reality claims. A reality claim is a labeled predicate on realizations; the mathematical content is the holds predicate. A claim is independent over an admissible class when two admissible realizations disagree on it (the existential Independent proposition from the Primitive module).
The module insists that if a claim is not forced, maximal closure demands an explicit countermodel pair rather than a vague appeal to contingency. Admissibility is the filter that selects which realizations count for forcing and independence judgments.
proof idea
This is a structure definition, not a proof. It packages the six pieces of data that constitute an explicit countermodel pair: the yes-model, the no-model, proofs that both lie in the admissible class, a proof that the claim holds on the yes-model, and a proof that it fails on the no-model. The companion lemma independent_of_witness projects this data onto the existential Independent proposition by assembling the six fields into a single exists-witness.
why it matters
ClaimClassification uses this structure as the constructor for the independent branch, opposite the forced branch. Downstream, yardstickIndepWitness shows the absolute mass scale is a free coordinate rather than a forced invariant (two admissible yardsticks 1 and 2 disagree on $M_0=1$), and positiveIndepWitness exhibits independence for a positivity claim over a triangular selection universe. The structure also feeds MaximalClosureCert and extension transport (mem_extend_of_mem). In the Recognition Science forcing chain it is the bookkeeping device that separates forced invariants (T5 J-uniqueness through T8 dimension) from free coordinates such as the mass yardstick on the phi-ladder.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.