Independent
plain-language theorem explainer
A reality claim is independent over an admissible class when two admissible realizations disagree on it. Anyone separating forced invariants from free parameters in the Maximal Forcing Closure program cites this predicate. The body is a plain existential: two admissible points, one where the claim holds and one where it fails.
Claim. Fix a type $R$ of realizations, an admissible class $A \subseteq R$, and a claim $C$ given by a predicate on $R$. The claim $C$ is independent over $A$ when there exist $r_0, r_1 \in A$ such that $C$ holds at $r_0$ and fails at $r_1$.
background
This module opens the Maximal Forcing Closure program. The target is to derive every invariant that is shared by all admissible realizations, and to prove that every leftover degree of freedom is either forced by a deeper admissibility condition or independent by countermodel. The file only sets the primitive claim language; it does not assert the crown theorem.
A reality claim packages audit metadata (a string label) with a predicate holds on realizations. The companion notion of forcedness says the claim holds at every admissible point. Independence is the complementary witness: two admissible points that split on the claim.
Downstream, the same independence idea appears in configuration spaces for cost-from-distinction, where independent configurations share no predicates and cost is required to be additive on their join.
proof idea
Pure definition, not a proved theorem. The predicate is the existential statement that two members of the admissible set disagree on whether the claim holds. No lemmas are applied; the body is the mathematical content.
why it matters
Independence is the dual of forcedness in the Maximal Forcing language. The program needs both: forced claims become derived invariants; independent claims are closed by countermodel rather than by further axioms. Downstream, CostFromDistinction uses an independence relation on configurations for the additivity axiom of cost (independent join of inconsistent configs has strictly larger cost; three-way additivity; extension of calibrated costs through consistent independent extensions). ConfigSpace packages independence as a structural field. Cosmology also consumes the notion in the vacuum-fluctuation structural certificate. In the broader RS chain this sits under the forcing program that aims to pin T5–T8 style invariants and leave only genuine free parameters.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.