Foundation Boolean Projection From Mark

The two-valued shadow

Boolean projection is the act of compressing a collection of possibilities into a two-valued answer: true or false, yes or no, selected or not. Any set with at least two elements admits such a compression, but not uniquely. A set of three objects can be collapsed in six different ways, since any of the three can be the one that maps to false while the other two map to true. Without an additional rule, no single collapse is more natural than another.

The classical remedy is to choose a distinguished element. In set theory and logic, fixing a base point turns a set into a pointed set, and the pointed structure selects a canonical two-valued map: the base point goes to false, everything else goes to true. This is the standard construction behind characteristic functions and indicator functions. The same idea appears in computer science as the classic test for equality against a sentinel value.

In Recognition Science, the framework models recognition as a discrete record of events, a ledger that tracks which distinctions have been made. The framework's library, a machine-checked collection of formal theorems, formalizes this pointed-set intuition in a module called BooleanProjectionFromMark. A mark, a named two-point choice inside a larger carrier set, is defined as a structure holding a base element, an alternative element, and a proof that they differ. From any such mark, the library defines a Boolean projection: the base maps to false, every other element maps to true.

The module proves two results. First, given a mark, the induced projection is canonical: it sends the marked base to false and the marked alternative to true, and this behavior is forced by the definition. Second, without a mark, no canonical projection exists: the library exhibits a three-element set with two different marked pairs whose projections disagree. These two theorems are packaged into a certificate structure, a single object that bundles both facts for downstream use.

What this establishes in plain language is a precise boundary. A carrier with at least two points always has a two-valued shadow, but the shadow is not canonical until a mark is supplied. The mark is the minimal extra structure that turns an arbitrary collapse into a determined one. This matters because later stages of the framework build on canonical projections; knowing exactly when a projection is forced, and when it is not, prevents ambiguity from silently entering the chain of reasoning.

/-- The Boolean projection determined by a marked pair: the base point maps to
`false`, and every non-base point maps to `true`. -/
noncomputable def boolProjection {K : Type*} (m : MarkedPair K) : K → Bool := by
  classical
  exact fun z => if z = m.base then false else true

/-- Given a marked pair, the induced Boolean projection sends the marked base
to `false` and the marked alternative to `true`. -/
theorem boolProjection_canonical_given_mark {K : Type*} (m : MarkedPair K) :
    boolProjection m m.base = false ∧ boolProjection m m.alt = true := by
  classical
  constructor
  · simp [boolProjection]
  · have halt_ne_base : m.alt ≠ m.base := fun h => m.distinct h.symm
    simp [boolProjection, halt_ne_base]

/-- Without a mark, a three-point carrier has multiple inequivalent Boolean
shadows. This witnesses that non-singletonness alone does not canonically
select a Boolean floor projection. -/
theorem bool_projection_not_canonical_without_mark :
    ∃ (K : Type) (m1 m2 : MarkedPair K),
      boolProjection m1 ≠ boolProjection m2 := by
  classical
  let m1 : MarkedPair (Fin 3) :=
    { base := 0
      alt := 1
      distinct := by decide }
  let m2 : MarkedPair (Fin 3) :=
    { base := 1
      alt := 0
      distinct := by decide }
  refine ⟨Fin 3, m1, m2, ?_⟩
  intro h
  have h0 := congrArg (fun f : Fin 3 → Bool => f 0) h
  simp [boolProjection, m1, m2] at h0

/-- The Boolean-projection certificate is theorem-backed. -/
theorem booleanProjectionFromMarkCert : BooleanProjectionFromMarkCert where
  marked_pair_projection := boolProjection_canonical_given_mark
  no_canonical_projection_without_mark :=
    bool_projection_not_canonical_without_mark

What this page does not claim

This module does not claim that any particular mark is canonical, only that a projection is canonical once a mark is given. The non-canonical result does not say that a three-element carrier has no Boolean projection; it says no unique one exists without a mark. No claim is made here about how marks arise in the broader Recognition Science framework.

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