Foundation Maximal Forcing Admissible Realization Tightening Does Work

When tightening a theory does real work

In mathematics and physics, a theory often gains power when you add assumptions. The question is whether the new assumption actually rules something out, or merely relabels what was already there. The Recognition Science framework's machine-checked library of formal theorems addresses this with a precise result about its notion of admissible realization classes, which are sets of possible worlds or models that a theory permits. The theorem, named tightening_does_work, establishes that if a claim is independent over a wider class but forced over a narrower one, then the narrower class excludes at least one realization that the wider class admitted.

To see why this matters, consider what independence and forcing mean in this setting. A claim is independent over a class when there exist two admissible realizations, one satisfying the claim and one failing it. A claim is forced over a class when every admissible realization satisfies it. The theorem's premise is a flip: the claim is independent over the wider class A, but forced over the narrower class B. The proof then constructs the excluded realization directly. It takes the realization from the independence witness that fails the claim, and shows that this realization cannot be B-admissible, because if it were, the forcing property would require it to satisfy the claim, a contradiction.

The result is a formal theorem in the framework's library, proved with no gaps and no special axioms beyond the standard logical ones. Its role in the larger structure is to make the framework's notion of a legitimate tightening non-vacuous. A tightening from A to B is legitimate only if it does real work, meaning some A-admissible realization is excluded by B, and is justified by a deeper law rather than a free choice. The theorem provides the does_work component: it guarantees that when a claim flips from independent to forced, the tightening genuinely narrows the space of possibilities.

What the theorem does not claim is equally important. It does not assert that any particular tightening is justified by a deeper law; that requires a separate proof obligation, stored in the LegitimateTightening structure as a named law with its own proof. The theorem only establishes the existence of an excluded realization given the independence-to-forcing flip. It also does not say anything about which claim is being tightened, or what the deeper law is. Those details are parameters, filled in by the specific application. The theorem is a structural guarantee about the framework's machinery, not a statement about any particular physical law.

In plain terms, the theorem certifies that when the framework tightens its assumptions and a claim becomes forced as a result, the tightening is not a hollow gesture. It has excluded at least one world that was previously possible. This matters because it gives the framework's method of adding deeper laws a precise, checkable meaning: a legitimate tightening always narrows the space of admissible realizations, and the proof shows exactly how to find the excluded one.

/-- A tightening does real work when some realization admissible for the wider
class `A` is excluded by the narrower class `B`. This is derived from a genuine
independence-to-forcing flip: if a claim is independent over `A` but forced over
`B`, then the `A`-admissible realization that *fails* the claim cannot be
`B`-admissible, since everything `B`-admissible satisfies it. -/
theorem tightening_does_work {R : Type u} {A B : AdmissibilityClass R}
    {C : RealityClaim R}
    (hIndep : Independent A.admissible C) (hForced : Forced B.admissible C) :
    ∃ r : R, r ∈ A.admissible ∧ r ∉ B.admissible := by
  obtain ⟨_r0, r1, _h0, h1, _hC0, hnotC1⟩ := hIndep
  exact ⟨r1, h1, fun hr1B => hnotC1 (hForced r1 hr1B)⟩

/-- A class of admissible realizations. The type `R` is deliberately abstract:
different phases may instantiate it with strict logic realizations, costed
realizations, physical models, or domain-specific structures. -/
structure AdmissibilityClass (R : Type u) where
  admissible : Set R
  label : String

/-- A claim forced after tightening is a target for promotion from `Selected` to
`Forced`. -/
def ForcedAfterTightening {R : Type u} (A B : AdmissibilityClass R)
    (C : RealityClaim R) : Prop :=
  Nonempty (Tightening A B) ∧ Forced B.admissible C

/-- Smart constructor. A genuine independence-to-forcing flip plus a named, proved
deeper law assembles a legitimate tightening. -/
def legitimateTightening_of_flip {R : Type u} {A B : AdmissibilityClass R}
    {C : RealityClaim R}
    (hsub : ∀ r : R, r ∈ B.admissible -> r ∈ A.admissible)
    (hIndep : Independent A.admissible C) (hForced : Forced B.admissible C)
    (law : Prop) (law_proof : law) (law_label : String) :
    LegitimateTightening A B where
  subset := hsub
  does_work := tightening_does_work hIndep hForced
  deeper_law := law
  deeper_law_proof := law_proof
  deeper_law_label := law_label

What this page does not claim

The theorem does not assert that any particular tightening is justified by a deeper law. The theorem does not identify which claim is being tightened or what the deeper law is. The theorem does not establish that any specific physical claim is forced.

Verify this page

Every tagged claim above names its theorem. To check one yourself rather than trust this page, elaborate the source module with Lean 4 and audit its axiom basis:

$ lake env lean IndisputableMonolith/Foundation/MaximalForcing/AdmissibleRealization.lean
expected axiom basis: [propext, Classical.choice, Quot.sound] (the Lean kernel's standard three; no RS-specific axioms)

A page whose claims cannot be reproduced this way does not ship. In production, every anchor links to the exact declaration in the public source release, and this block carries the build receipt for the page itself.

Derived articles

This page is generated by a question-recursion engine: the questions its answers raise become the next pages. The current agenda, with open targets marked red: