Foundation Maximal Forcing Admissible Realization Forced After Tightening

Forcing after tightening

A recognition framework, a discrete record of events, often starts by asking which statements hold in every allowed world. The set of allowed worlds is an admissibility class. A claim is forced when every world in the class satisfies it. The declaration ForcedAfterTightening records a simple monotonicity: if a claim is forced on a wider class, it remains forced on any narrower class. The machine-checked theorem forced_of_forced_under_tightening proves this directly: a world in the narrower class is also in the wider one, so it satisfies the claim.

The declaration also carries a second, sharper meaning. It names the situation where a claim is not forced on the current class, but becomes forced after the class is tightened by adding a deeper law. The definition requires two things: a tightening from the wider class A to the narrower class B, and the claim being forced on B. The tightening itself is a structure with a subset proof and a strictness witness. The witness is a placeholder in the base definition, but a later structure, LegitimateTightening, replaces it with a proof obligation: the tightening must do real work and be justified by a deeper law, not chosen freely.

The real-work condition is non-vacuous. The theorem tightening_does_work shows that if a claim is independent over A but forced over B, then some A-admissible world fails the claim and cannot be B-admissible. The tightening excludes at least one world. The legitimateTightening_of_flip constructor assembles a legitimate tightening from an independence-to-forcing flip plus a named, proved deeper law. This makes legitimacy a discharged proof obligation, not a stored True.

What the declaration does not claim is as precise as what it does. It does not assert that any particular tightening is legitimate. It does not name any specific deeper law. It does not prove that any particular claim is forced after tightening. It only defines the predicate and proves the monotonicity theorem. The legitimacy of a tightening, with its deeper law and proof, is a separate structure that must be supplied for each application.

/-- If a claim is forced on a wider admissible class, it remains forced after
tightening. -/
theorem forced_of_forced_under_tightening {R : Type u}
    {A B : AdmissibilityClass R} {C : RealityClaim R}
    (hT : Tightening A B) (hA : Forced A.admissible C) :
    Forced B.admissible C := by
  intro r hr
  exact hA r (hT.subset r hr)

/-- 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 **legitimate** tightening. Beyond the subset order it carries:

* `does_work`: a proof the gate is non-vacuous (some `A`-admissible realization is
  excluded by `B`); and
* `deeper_law` together with `deeper_law_proof`: the actual RS forcing theorem that
  justifies the added constraint, so the tightening is forced by a deeper law, not
  chosen freely. `deeper_law_label` names it for the audit.

This replaces `strict_witness := True`: legitimacy is now a discharged proof
obligation, not a stored `True`. -/
structure LegitimateTightening {R : Type u} (A B : AdmissibilityClass R) where
  subset : ∀ r : R, r ∈ B.admissible -> r ∈ A.admissible
  does_work : ∃ r : R, r ∈ A.admissible ∧ r ∉ B.admissible
  deeper_law : Prop
  deeper_law_proof : deeper_law
  deeper_law_label : String

What this page does not claim

No specific claim is asserted to be forced after tightening; the declaration only defines the predicate. No particular tightening is asserted to be legitimate; that requires a separate proof of a deeper law. The strictness witness in the base Tightening structure carries no content until a legitimate tightening supplies a proof.

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: