Foundation Tminus1 Forced From Distinction Boolean Observable Floor Forced From

The forced Boolean floor

A distinction is the simplest possible fact: two things are not the same. The theorem booleanObservableFloor_forced_from_distinction starts from exactly that fact, a witness that there exist two elements, call them x and y, with x not equal to y. From this bare premise, the proof constructs a two-valued projection: a function that labels one thing false and the other true. It then builds an equivalence relation, grouping everything that shares the same label, and shows the resulting two classes are in one-to-one correspondence with the Boolean values false and true.

The construction is entirely forced. The theorem proves that, given the distinction, a Boolean-coordinate system on the quotient exists. It also proves that any two such coordinate systems differ only by a Boolean automorphism, meaning the labeling is unique up to swapping false and true. The library, a machine-checked collection of formal theorems, verifies each step. The result is a Boolean observable floor: a minimal two-valued layer of observation that any framework must possess once it has a distinction.

This is the non-half-measure version of the T−1 repair. The primitive is not an external admissibility package; it is the distinction witness itself. If there is no object-level distinction, there is no object-level forcing. But once the distinction is given, the Boolean floor is not an extra assumption. The theorem also supplies the legacy raw floor required by the existing RealityCertificate, and it decomposes the certificate into distinction-supplied and upstream-supplied fields.

The theorem does not claim that distinctions exist in any particular physical system. It is conditional: if a distinction is given, then the Boolean floor follows. It does not claim that the Boolean labels correspond to any physical observable such as spin or charge; the labels are abstract. It does not claim that the construction works without the distinction, nor that the Boolean floor is the only possible floor. It also does not claim that the framework derives the existence of two distinct things from nothing; that existence is the premise.

/-- The supplied distinction forces a two-class observable Boolean floor. -/
theorem booleanObservableFloor_forced_from_distinction
    {K : Type*} (h : ∃ x y : K, x ≠ y) :
    Nonempty (Quotient (forcedObservableSetoid h) ≃ Bool) :=
  ⟨forcedQuotientEquivBool h⟩

/-- The Boolean projection forced by a chosen distinction witness. -/
noncomputable def forcedBoolProjection
    {K : Type*} (h : ∃ x y : K, x ≠ y) : K → Bool :=
  boolProjection (markedPairOfDistinction h)

/-- Boolean coordinates forced by the same distinction are unique up to Boolean
automorphism. -/
theorem forcedBooleanCoordinates_unique_up_to_bool_aut
    {K : Type*} {h : ∃ x y : K, x ≠ y}
    (c₁ c₂ : ForcedBooleanCoordinates h) :
    c₂.coord = c₁.coord.trans (forcedBooleanCoordinateChange c₁ c₂) := by
  ext q
  simp [forcedBooleanCoordinateChange]

/-- The supplied distinction forces the raw floor expected by the legacy
certificate interface. -/
theorem rawFloor_forced_from_distinction
    {K : Type*} (h : ∃ x y : K, x ≠ y) :
    ∃ x y : K, x ≠ y :=
  h

/-- Decomposition audit for the stronger formulation: the distinction forces
the T−1 floor interface; the remaining certificate fields are the already
proved upstream forcing-chain theorems. -/
theorem forced_distinction_certificate_decomposes
    (K : Type) [Nonempty K]
    (h : ∃ x y : K, x ≠ y) :
    DistinctionSuppliedFields K ∧ UpstreamSuppliedFields :=
  bundling_decomposition K h

What this page does not claim

The theorem does not claim that distinctions exist in any particular physical system. The theorem does not claim that the Boolean labels correspond to any physical observable such as spin or charge. The theorem does not claim that the Boolean floor is the only possible floor.

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/TMinus1ForcedFromDistinction.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: