Foundation Tminus1 Forced From Distinction Forced Distinction Certificate Decomp

The distinction witness

In mathematics, a distinction is the simplest possible fact: there exist two objects, x and y, such that x is not equal to y. The Recognition Science framework's library of machine-checked formal theorems contains a declaration, forced_distinction_certificate_decomposes, that takes this single witness as its only input. The theorem establishes that from this one fact, the framework can construct two separate packages of structure: the DistinctionSuppliedFields and the UpstreamSuppliedFields. These are not assumed or imported from outside; they are derived, step by step, from the bare fact that two things differ.

The construction works by first choosing the two distinct objects, labeling one as the base and the other as the alternate. From this marked pair, the library defines a Boolean projection: a function that sends every object to either false or true, depending on which of the two classes it belongs to. This projection generates an equivalence relation, grouping objects that project to the same value. The quotient of this relation is a two-class set, and the library proves this quotient is equivalent to the Boolean type, the two-element set {false, true}. A further theorem shows these Boolean coordinates are unique up to a Boolean automorphism, meaning the labeling is essentially forced once the distinction is given.

The declaration forced_distinction_certificate_decomposes is the bundling of this entire construction into a single statement. It says that, given any nonempty type K with a witness that two of its elements differ, the framework can produce both the distinction-supplied fields and the upstream-supplied fields. The theorem is proved in the library's file TMinus1ForcedFromDistinction.lean, and it depends on the classical choice axiom to pick the two distinct elements, but it introduces no new axioms specific to the framework. The result is a formal guarantee that the Boolean floor of the framework's reality certificate is not an extra measure, but a consequence of the distinction itself.

What this theorem does not claim is equally important. It does not assert that a distinction exists in any particular physical system; it only says that if one exists, the Boolean floor follows. It does not derive the full recognition chain, the cost function, or any of the later constants like the golden ratio; those come from further theorems in other files. The declaration is about the Boolean and observable floor only, not about any higher structure. It also does not claim that the choice of which object is base and which is alternate is canonical; that choice is made by the classical choice axiom, and the uniqueness theorem only says the coordinates are unique up to a Boolean automorphism, not that there is a single preferred labeling.

The practical consequence is that the framework's foundation does not rest on a stack of ad hoc assumptions. The Boolean floor, the two-class observable structure, and the equivalence relation are all forced by the minimal possible input: a single distinction. This makes the framework's starting point as lean as it can be, and it means that any system with at least two distinguishable objects automatically carries the entire Boolean floor of the framework's reality certificate.

/-- 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

/-- 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]

/-- Extract the marked pair carried by a distinction witness. -/
noncomputable def markedPairOfDistinction
    {K : Type*} (h : ∃ x y : K, x ≠ y) : MarkedPair K where
  base := Classical.choose h
  alt := Classical.choose (Classical.choose_spec h)
  distinct := Classical.choose_spec (Classical.choose_spec h)

What this page does not claim

The theorem does not assert that a distinction exists in any particular physical system. The theorem does not derive the full recognition chain, the cost function, or any later constants. The theorem does not claim a canonical choice of which object is base and which is alternate.

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: