Foundation Boolean Projection From Mark Bool Projection Canonical Given Mark

The marked Boolean floor

A Boolean projection is a simple kind of map: it sends every element of some carrier set to one of two values, which we can call false and true. Any set with at least two elements admits many such maps, since there are many ways to split the set into two groups. The Recognition Science framework asks when such a two-valued shadow is canonical, meaning forced by the structure rather than chosen by hand.

The answer in the framework's machine-checked library of formal theorems is that a Boolean projection becomes canonical only after a distinguishing mark has been chosen. A marked pair is exactly that choice: a carrier set together with two named points, a base and an alternative, with a proof that they are distinct. Given such a pair, the framework defines the Boolean projection determined by it: the base point maps to false, and every other point maps to true. The theorem boolProjection_canonical_given_mark proves that this projection sends the base to false and the alternative to true, so the two marked points are kept apart by the map.

Without a mark, no such canonical choice exists. The framework also proves that a three-point carrier admits at least two marked pairs whose induced Boolean projections differ. Non-singletonness alone, having more than one element, does not select a unique two-valued shadow. The mark is the missing ingredient that turns a merely possible projection into the canonical one.

In Recognition Science, this result is the T-1 Boolean floor: the first step in building a discrete ledger, a record of events, out of a carrier set. The theorem establishes that the floor is canonical only relative to a chosen mark, and that the mark itself is not derived from the carrier alone. What the theorem does not claim is that the mark is unique, that a carrier chooses its own distinguished points, or that any particular physical system supplies a mark. Those questions remain open and are not settled by this declaration.

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

The theorem does not claim that a carrier set chooses its own mark. The theorem does not claim that the Boolean projection is unique without a mark. The theorem does not claim that any specific physical system supplies a marked pair.

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: