Encyclopedia Foundation Foundation Universal Instantiation From Distinction Exists Logic Realization Of
ARTICLE 5 claims 5 theorems
Foundation Universal Instantiation From Distinction Exists Logic Realization Of
Any collection with at least two different things in it can run the framework's basic logical machinery, with no extra structure assumed.
The distinction theorem
In mathematics, a carrier is just the set of objects a structure lives on. The theorem exists_logicRealization_of_distinction says: if a carrier has at least two distinct elements, it can support a recognition structure, a way of marking some pairs as the same and others as different. The construction uses the simplest possible rule: two elements cost 0 if they are identical, and cost 1 if they are not. This two-valued equality cost is symmetric, returns 0 exactly on equal inputs, and satisfies the triangle inequality.
The theorem builds a full logic realization, a package that includes a base point, a step map, and three law-slots that must hold. The base point is the first distinguished element; the step map sends every element to the second distinguished one. The three slots are genuine: excluded middle holds because any two elements are either equal or not, the additive composition law holds as the triangle inequality, and the step action is invariant because it is constant. The construction deliberately declines the multiplicative composition law, which equality cost provably cannot satisfy.
The payoff is universal: any non-singleton carrier, with no metric, topology, or algebraic structure assumed, instantiates the framework's Law-of-Logic interface. Its forced arithmetic object is canonically equivalent to the natural numbers, and any two such carriers have the same forced arithmetic. The continuous J/spacetime layer is reached later through canonical realization-invariance, not by pretending an arbitrary carrier is the positive real line.
What the theorem does not claim is as important as what it proves. It does not assert that every carrier has a native smooth real-valued J-cost. It does not derive the golden ratio, the eight-tick cycle, or three spatial dimensions for an arbitrary carrier. It proves the first universal step that is actually true: distinction alone is enough to instantiate the logical interface, and that is all.
THEOREM exists_logicRealization_of_distinction · IndisputableMonolith/Foundation/UniversalInstantiationFromDistinction.lean
/-- Every inhabited carrier with some distinction admits a native
`LogicRealization`. The `DecidableEq K` instance is obtained classically. -/
theorem exists_logicRealization_of_distinction
(K : Type u) [Nonempty K] (h : ∃ x y : K, x ≠ y) :
Nonempty (LogicRealization.{u, 0}) := by
classical
rcases h with ⟨x, y, hxy⟩
exact ⟨logicRealizationOfDistinction K x y hxy⟩
THEOREM eqCost · IndisputableMonolith/Foundation/UniversalInstantiationFromDistinction.lean
/-- Two-valued equality cost: zero on equal inputs, one on distinct inputs. -/
def eqCost {K : Type u} [DecidableEq K] (a b : K) : Nat :=
if a = b then 0 else 1
THEOREM logicRealizationOfDistinction_excludedMiddle · logicRealizationOfDistinction_composition · logicRealizationOfDistinction_actionInvariant · IndisputableMonolith/Foundation/UniversalInstantiationFromDistinction.lean
/-- 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
/-- 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
/-- 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 universalInstantiationCert · IndisputableMonolith/Foundation/UniversalInstantiationFromDistinction.lean
theorem universalInstantiationCert
(K : Type u) [Nonempty K] :
UniversalInstantiationCert K where
instantiate := exists_logicRealization_of_distinction K
named := exists_named_logicRealization_of_distinction K
THEOREM distinction_arithmetic_equiv_logicNat · distinction_realizations_have_same_arithmetic · IndisputableMonolith/Foundation/UniversalInstantiationFromDistinction.lean
/-- The forced arithmetic of the `K`-native realization is canonically
`LogicNat`. -/
noncomputable def distinction_arithmetic_equiv_logicNat
{K : Type u} [DecidableEq K] (x y : K) (hxy : x ≠ y) :
(UniversalForcing.arithmeticOf
(logicRealizationOfDistinction K x y hxy)).peano.carrier ≃ LogicNat :=
(logicRealizationOfDistinction K x y hxy).orbitEquivLogicNat
/-- 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 derive the golden ratio, the eight-tick cycle, or three spatial dimensions for an arbitrary carrier. The theorem does not assert that every carrier has a native smooth real-valued J-cost. The theorem does not claim that distinction alone produces the full continuous spacetime structure.
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:
- What is the Law-of-Logic interface, and what does instantiating it commit a carrier to?
- How does the canonical realization-invariance step reach the continuous J/spacetime layer from a discrete carrier?
- Which carriers fail to be non-singleton, and what does the framework say about them?
- What is the multiplicative composition law that equality cost cannot satisfy, and why does it matter?
MACHINE LAYER · GROUNDED CLAIM TABLE · CLICK TO EXPAND
THEOREM exists_logicRealization_of_distinction · IndisputableMonolith/Foundation/UniversalInstantiationFromDistinction.lean
/-- Every inhabited carrier with some distinction admits a native `LogicRealization`. The `DecidableEq K` instance is obtained classically. -/ theorem exists_logicRealization_of_distinction (K : Type u) [Nonempty K] (h : ∃ x y : K, x ≠ y) : Nonempty (LogicRealization.{u, 0}) := by classical rcases h with ⟨x, y, hxy⟩ exact ⟨logicRealizationOfDistinction K x y hxy⟩If a carrier has at least two distinct elements, it can support a recognition structure. exists_logicRealization_of_distinction · IndisputableMonolith/Foundation/UniversalInstantiationFromDistinction.leanTHEOREM eqCost · IndisputableMonolith/Foundation/UniversalInstantiationFromDistinction.lean
/-- Two-valued equality cost: zero on equal inputs, one on distinct inputs. -/ def eqCost {K : Type u} [DecidableEq K] (a b : K) : Nat := if a = b then 0 else 1The construction uses the simplest possible rule: two elements cost 0 if they are identical, and cost 1 if they are not. eqCost · IndisputableMonolith/Foundation/UniversalInstantiationFromDistinction.leanTHEOREM logicRealizationOfDistinction_excludedMiddle · logicRealizationOfDistinction_composition · logicRealizationOfDistinction_actionInvariant · IndisputableMonolith/Foundation/UniversalInstantiationFromDistinction.lean
/-- 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/-- 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/-- 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 _ _; rflThe three slots are genuine: excluded middle holds because any two elements are either equal or not, the additive composition law holds as the triangle inequality, and the step action is invariant because it is constant. logicRealizationOfDistinction_excludedMiddle · logicRealizationOfDistinction_composition · logicRealizationOfDistinction_actionInvariant · IndisputableMonolith/Foundation/UniversalInstantiationFromDistinction.leanTHEOREM universalInstantiationCert · IndisputableMonolith/Foundation/UniversalInstantiationFromDistinction.lean
theorem universalInstantiationCert (K : Type u) [Nonempty K] : UniversalInstantiationCert K where instantiate := exists_logicRealization_of_distinction K named := exists_named_logicRealization_of_distinction KAny non-singleton carrier, with no metric, topology, or algebraic structure assumed, instantiates the framework's Law-of-Logic interface. universalInstantiationCert · IndisputableMonolith/Foundation/UniversalInstantiationFromDistinction.leanTHEOREM distinction_arithmetic_equiv_logicNat · distinction_realizations_have_same_arithmetic · IndisputableMonolith/Foundation/UniversalInstantiationFromDistinction.lean
/-- The forced arithmetic of the `K`-native realization is canonically `LogicNat`. -/ noncomputable def distinction_arithmetic_equiv_logicNat {K : Type u} [DecidableEq K] (x y : K) (hxy : x ≠ y) : (UniversalForcing.arithmeticOf (logicRealizationOfDistinction K x y hxy)).peano.carrier ≃ LogicNat := (logicRealizationOfDistinction K x y hxy).orbitEquivLogicNat/-- 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.symmIts forced arithmetic object is canonically equivalent to the natural numbers, and any two such carriers have the same forced arithmetic. distinction_arithmetic_equiv_logicNat · distinction_realizations_have_same_arithmetic · IndisputableMonolith/Foundation/UniversalInstantiationFromDistinction.lean