Foundation Distinction To T4 Forced Quotient Recognition Work Constraint

The forced quotient constraint

The declaration forcedQuotient_recognition_work_constraint is a theorem in the Recognition Science framework's machine-checked library of formal theorems. It starts from the weakest possible input: a witness that some collection K contains two distinct elements, written as ∃ x y : K, x ≠ y. From that single distinction, the framework constructs a quotient, a way of grouping all elements of K into two classes, and proves that this two-class structure carries a recognition-work cost satisfying a specific constraint. The theorem's plain content is that the mere existence of a difference forces a minimal, two-state model of recognition, and that this model obeys the framework's cost law.

The construction works by building a quotient of K, denoted ForcedQuotient h, which is proven equivalent to the Boolean type Bool, the set with two elements usually called true and false. The framework then transports its standard Boolean configuration space and its recognition-work cost across this equivalence. The key theorem, forcedQuotientRecognitionCost_transport, states that the cost of any element in the quotient equals the cost of its corresponding Boolean value. This is a definitional equality, meaning the two costs are the same by construction, not by a separate proof. The result is a recognition-work surface on the quotient that is generated by the distinction itself, with no additional assumptions about K.

The constraint theorem itself, forcedQuotient_recognition_work_constraint, asserts that there exists a certificate, a formal witness, that the cost function on the quotient satisfies the RecognitionWorkConstraintCert property. This property is the framework's way of certifying that the cost function meets its defining axioms, including the forced composition law and the other conditions that lead to the unique cost function J(x) = (x + 1/x)/2 - 1. The theorem is proved by applying the general recognition_work_constraint_theorem to the specific cost function built on the quotient. It is a theorem in the strongest sense: it is checked by the Lean 4 kernel with no additional axioms beyond the standard three, and no framework-specific assumptions about the nature of K beyond its having two distinct elements.

What this theorem does not claim is equally important. It does not claim that the quotient is the only possible model, nor that the cost constraint is unique. It establishes existence, not uniqueness, of the certificate. It does not claim anything about the physical interpretation of K or the quotient; the theorem is purely structural, about the logical consequences of a distinction. It does not claim that T0 through T4 separation axioms, which are also derived in the same module, follow from this single theorem alone; those are separate theorems, though they are proved in the same file and use the same quotient construction. The theorem is a foundation stone, not a complete building.

In the broader framework, this result is Phase 1 of a closure path from a distinction to the early forcing spine. It shows that the framework's structure does not need to be assumed; it can be forced from the mere existence of a difference. This matters because it grounds the framework's later results, such as the eight-tick cycle and three spatial dimensions, in a logical foundation that is as minimal as possible. The reader can now see that the framework's claims are not arbitrary postulates but consequences of a single, unavoidable starting point: the fact that things can be told apart.

/-- The forced quotient-to-Bool coordinate equivalence. -/
noncomputable def forcedQuotientBoolEquiv
    {K : Type*} (h : ∃ x y : K, x ≠ y) :
    ForcedQuotient h ≃ Bool :=
  forcedQuotientEquivBool h

/-- The transported cost is literally the Boolean recognition cost under the
forced quotient coordinate. -/
theorem forcedQuotientRecognitionCost_transport
    {K : Type*} (h : ∃ x y : K, x ≠ y) (Γ : ForcedQuotient h) :
    (forcedQuotientRecognitionCost h).C Γ =
      UnifiedForcingChain.TMinus1ToT0.boolRecognitionCost.C
        (forcedQuotientBoolEquiv h Γ) :=
  rfl

/-- The forced quotient carries the recognition-work constraint theorem. -/
theorem forcedQuotient_recognition_work_constraint
    {K : Type*} (h : ∃ x y : K, x ≠ y) :
    Nonempty (CostFunction.RecognitionWorkConstraintCert (ForcedQuotient h)) :=
  CostFunction.recognition_work_constraint_theorem
    (forcedQuotientRecognitionCost h)

/-- The forced quotient carries the recognition-work constraint theorem. -/
theorem forcedQuotient_recognition_work_constraint
    {K : Type*} (h : ∃ x y : K, x ≠ y) :
    Nonempty (CostFunction.RecognitionWorkConstraintCert (ForcedQuotient h)) :=
  CostFunction.recognition_work_constraint_theorem
    (forcedQuotientRecognitionCost h)

What this page does not claim

This theorem does not claim uniqueness of the cost constraint certificate. This theorem does not claim that the quotient model is the only possible model of recognition. This theorem does not claim that the T0 through T4 separation axioms follow from this single theorem alone.

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