Encyclopedia Foundation Foundation Universal Instantiation From Distinction Exists Named Logic Realizati

ARTICLE 5 claims 5 theorems

Foundation Universal Instantiation From Distinction Exists Named Logic Realizati

Any collection with at least two different things in it can be made to carry the framework's basic logical structure, with no extra assumptions.

Verify this page

The bare distinction theorem

In the Recognition Science framework, a ledger is a discrete record of events, and a recognition is the act of comparing two entries in that record. The declaration exists_named_logicRealization_of_distinction is a machine-checked theorem stating that any non-empty collection with at least two distinguishable elements can be given the structure of a LogicRealization, the framework's basic logical object. The proof is constructive: it names the two distinct points, defines a two-valued equality cost (zero when entries match, one when they differ), and builds the required step map as the constant function sending every state to the second distinguished point.

This theorem repairs a skeptical objection to the framework's starting point. A bare distinction should not merely sit beside an already-existing reality certificate; it should first instantiate the Law-of-Logic interface on its own carrier. The construction is intentionally minimal. It does not assert that every carrier has a native smooth real-valued J-cost, the framework's central cost function. It proves the first universal step that is actually true: every non-singleton carrier instantiates the Law-of-Logic interface, therefore Universal Forcing applies to that carrier, therefore the carrier has the same forced arithmetic object as the canonical recognition realization.

The theorem also proves that the three law-slots carried by the minimal realization are genuine, not vacuous. The excluded-middle content holds: every pair on the carrier is same-or-different. The additive composition law, the triangle inequality, holds for the two-valued equality cost. The action is invariant because the step map is constant. The one law the equality cost provably cannot satisfy, multiplicative composition consistency, is explicitly declined. The realization makes named, true claims appropriate to a single distinction and no more.

What this establishes is a bridge. Any two non-singleton carriers, with chosen distinctions, have canonically equivalent forced arithmetic, meaning the same natural-number structure emerges regardless of the carrier's native content. The continuous J/spacetime layer is then reached through canonical realization-invariance, not by pretending an arbitrary carrier is itself the positive real line. The theorem does not claim that every carrier is a full recognition space, nor that the two-valued cost is the J-cost, nor that the construction works for a singleton carrier. It claims exactly the universal instantiation step, and it proves that step in the machine-checked library.

THEOREM exists_named_logicRealization_of_distinction · IndisputableMonolith/Foundation/UniversalInstantiationFromDistinction.lean
exists_named_logicRealization_of_distinction · IndisputableMonolith/Foundation/UniversalInstantiationFromDistinction.lean:222 
/-- A more precise version retaining the chosen points. -/
theorem exists_named_logicRealization_of_distinction
    (K : Type u) [Nonempty K] (h : ∃ x y : K, x ≠ y) :
    ∃ x y : K, ∃ hxy : x ≠ y,
      Nonempty (LogicRealization.{u, 0}) := by
  classical
  rcases h with ⟨x, y, hxy⟩
  exact ⟨x, y, hxy, ⟨logicRealizationOfDistinction K x y hxy⟩⟩
THEOREM logicRealizationOfDistinction · IndisputableMonolith/Foundation/UniversalInstantiationFromDistinction.lean
logicRealizationOfDistinction · IndisputableMonolith/Foundation/UniversalInstantiationFromDistinction.lean:90 
/-- **Universal instantiation theorem.**

Any carrier with a named distinction `x ≠ y` is a `LogicRealization` on
that very carrier. -/
noncomputable def logicRealizationOfDistinction
    (K : Type u) [DecidableEq K] (x y : K) (hxy : x ≠ y) :
    LogicRealization.{u, 0} where
  Carrier := K
  Cost := Nat
  zeroCost := inferInstance
  compare := eqCost
  zero := x
  step := distinctionStep x y
  Orbit := ULift.{u} LogicNat
  orbitZero := ULift.up LogicNat.zero
  orbitStep := fun n => ULift.up (LogicNat.succ n.down)
  interpret := distinctionInterpret x y
  interpret_zero := rfl
  interpret_step := by
    intro n
    exact distinctionInterpret_step x y n
  orbit_no_confusion := by
    intro n h
    exact LogicNat.zero_ne_succ n.down (congrArg ULift.down h)
  orbit_step_injective := by
    intro a b h
    apply ULift.ext
    exact LogicNat.succ_injective (congrArg ULift.down h)
  orbit_induction := by
    intro P h0 hs n
    cases n with
    | up n =>
      induction n with
      | identity => exact h0
      | step n ih => exact hs (ULift.up n) ih
  orbitEquivLogicNat :=
    { toFun := fun n => n.down
      invFun := fun n => ULift.up n
      left_inv := by intro n; cases n; rfl
      right_inv := by intro n; rfl }
  orbitEquiv_zero := rfl
  orbitEquiv_step := by intro n; rfl
  identity := by
    intro a
    exact eqCost_self a
  nonContradiction := by
    intro a b
    exact eqCost_symm a b
  -- The three slots below are *carried* propositions, not proof obligations:
  -- `LogicRealization` stores a `Prop` in each (`excludedMiddle`, `composition`,
  -- `actionInvariant`) and never forces it to hold. We therefore store the
  -- genuine, setting-appropriate statements that DO hold for the two-valued
  -- equality cost, and discharge each below (`logicRealizationOfDistinction_*`).
  --
  -- We deliberately do NOT store a multiplicative composition law: equality cost
  -- provably fails (L4) multiplicative composition consistency
  -- (`PrimitiveDistinction.equality_cost_insufficient_for_recognition`). That
  -- failure is exactly why this realization is minimal and the continuous J/φ
  -- layer is reached by realization-invariance, not by pretending an arbitrary
  -- `K` is the positive real line. The `composition` slot therefore carries the
  -- additive triangle inequality that the equality cost DOES satisfy.
  excludedMiddle := ∀ a b : K, a = b ∨ a ≠ b
  composition := ∀ a b c : K, eqCost a c ≤ eqCost a b + eqCost b c
  actionInvariant := ∀ a b : K, distinctionStep x y a = distinctionStep x y b
  nontrivial := by
    refine ⟨y, ?_⟩
    have hyx : y ≠ x := fun hy => hxy hy.symm
    simp [eqCost, hyx]
THEOREM universalInstantiationCert · IndisputableMonolith/Foundation/UniversalInstantiationFromDistinction.lean
universalInstantiationCert · IndisputableMonolith/Foundation/UniversalInstantiationFromDistinction.lean:263 
theorem universalInstantiationCert
    (K : Type u) [Nonempty K] :
    UniversalInstantiationCert K where
  instantiate := exists_logicRealization_of_distinction K
  named := exists_named_logicRealization_of_distinction K
THEOREM logicRealizationOfDistinction_excludedMiddle · logicRealizationOfDistinction_composition · logicRealizationOfDistinction_actionInvariant · IndisputableMonolith/Foundation/UniversalInstantiationFromDistinction.lean
logicRealizationOfDistinction_excludedMiddle · IndisputableMonolith/Foundation/UniversalInstantiationFromDistinction.lean:168 
/-- The minimal distinction realization genuinely satisfies the excluded-middle
content it carries: every pair on the carrier is same-or-different. -/
theorem logicRealizationOfDistinction_excludedMiddle
    {K : Type u} [DecidableEq K] (x y : K) (hxy : x ≠ y) :
    (logicRealizationOfDistinction K x y hxy).excludedMiddle := by
  show ∀ a b : K, a = b ∨ a ≠ b
  exact fun a b => eq_or_ne a b
logicRealizationOfDistinction_composition · IndisputableMonolith/Foundation/UniversalInstantiationFromDistinction.lean:176 
/-- The minimal distinction realization satisfies the *additive* composition law
(the triangle inequality) of its two-valued equality cost. This is NOT the
multiplicative composition consistency (L4), which equality cost provably fails
(`PrimitiveDistinction.equality_cost_insufficient_for_recognition`); the slot
deliberately carries only the additive law that does hold. -/
theorem logicRealizationOfDistinction_composition
    {K : Type u} [DecidableEq K] (x y : K) (hxy : x ≠ y) :
    (logicRealizationOfDistinction K x y hxy).composition := by
  show ∀ a b c : K, eqCost a c ≤ eqCost a b + eqCost b c
  intro a b c
  by_cases hac : a = c
  · have h0 : eqCost a c = 0 := by simp [eqCost, hac]
    rw [h0]; exact Nat.zero_le _
  · have hac1 : eqCost a c = 1 := eqCost_ne_one hac
    have hsplit : a ≠ b ∨ b ≠ c := by
      by_contra hcon
      push_neg at hcon
      exact hac (hcon.1.trans hcon.2)
    rw [hac1]
    rcases hsplit with hab | hbc
    · have h1 : eqCost a b = 1 := eqCost_ne_one hab
      have h2 : 0 ≤ eqCost b c := Nat.zero_le _
      omega
    · have h1 : eqCost b c = 1 := eqCost_ne_one hbc
      have h2 : 0 ≤ eqCost a b := Nat.zero_le _
      omega
logicRealizationOfDistinction_actionInvariant · IndisputableMonolith/Foundation/UniversalInstantiationFromDistinction.lean:203 
/-- The distinction step action is invariant across inputs: it is the constant
map onto the marked second point. -/
theorem logicRealizationOfDistinction_actionInvariant
    {K : Type u} [DecidableEq K] (x y : K) (hxy : x ≠ y) :
    (logicRealizationOfDistinction K x y hxy).actionInvariant := by
  show ∀ a b : K, distinctionStep x y a = distinctionStep x y b
  intro _ _; rfl
THEOREM distinction_realizations_have_same_arithmetic · IndisputableMonolith/Foundation/UniversalInstantiationFromDistinction.lean
distinction_realizations_have_same_arithmetic · IndisputableMonolith/Foundation/UniversalInstantiationFromDistinction.lean:241 
/-- Any two non-singleton carriers, with chosen distinctions, have
canonically equivalent forced arithmetic. -/
noncomputable def distinction_realizations_have_same_arithmetic
    {K L : Type u} [DecidableEq K] [DecidableEq L]
    {x y : K} {a b : L} (hxy : x ≠ y) (hab : a ≠ b) :
    (UniversalForcing.arithmeticOf
      (logicRealizationOfDistinction K x y hxy)).peano.carrier ≃
    (UniversalForcing.arithmeticOf
      (logicRealizationOfDistinction L a b hab)).peano.carrier :=
  (logicRealizationOfDistinction K x y hxy).orbitEquivLogicNat.trans
    (logicRealizationOfDistinction L a b hab).orbitEquivLogicNat.symm

What this page does not claim

The theorem does not assert that every carrier has a native smooth real-valued J-cost. The theorem does not claim that the two-valued equality cost is the J-cost. The theorem does not claim the construction works for a singleton carrier.

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

MACHINE LAYER · GROUNDED CLAIM TABLE · CLICK TO EXPAND