pith. machine review for the scientific record. sign in
theorem

reality_from_one_distinction

proved
show as:
view math explainer →

From ∃ x y, x ≠ y the structure of reality is forced.

module
IndisputableMonolith.Foundation.RealityFromDistinction
domain
Foundation
line
88 · github
papers citing
3051 papers (below)

open explainer

Generate a durable explainer page for this declaration.

open lean source

IndisputableMonolith.Foundation.RealityFromDistinction on GitHub at line 88.

browse module

All declarations in this module, on Recognition.

explainer page

Tracked in the explainer inventory; generation is lazy so crawlers do not trigger LLM jobs.

open explainer

depends on

used by

formal source

  85Every right-hand-side conclusion is an existing theorem in the repository.
  86This theorem is the named place where they are bundled into one
  87deliverable from the bare hypothesis `∃ x y : K, x ≠ y`. -/
  88theorem reality_from_one_distinction
  89    (K : Type) [Nonempty K]
  90    (h : ∃ x y : K, x ≠ y) :
  91    RealityCertificate K where
  92  distinction := h
  93  absolute_floor := ⟨absolute_floor_of_bare_distinguishability h⟩
  94  native_realization :=
  95    UniversalInstantiationFromDistinction.exists_logicRealization_of_distinction K h
  96  bool_floor := bool_absolute_floor
  97  spacetime := spacetime_emergence_cert_nonempty
  98  light_cone := lightlike_iff_speed_c
  99  time_orbit := timeAsOrbitCert_inhabited
 100  c_unit := ConstantDerivations.c_rs_eq_one
 101  hbar_from_phi := ConstantDerivations.ℏ_algebraic_in_φ
 102  G_from_phi := ConstantDerivations.G_algebraic_in_φ
 103
 104/-! ## Specialised forms -/
 105
 106/-- The minimal concrete instance: `Bool` is inhabited and admits the
 107distinction `false ≠ true`, so the master theorem applies and produces
 108the full chain on the smallest possible carrier. -/
 109theorem reality_from_bool : RealityCertificate Bool :=
 110  reality_from_one_distinction Bool ⟨false, true, SelfBootstrap.bool_distinguishable⟩
 111
 112/-- The master theorem in propositional form (no carrier needed in the
 113output, only the witness that *some* inhabited carrier admits a
 114distinction). -/
 115theorem reality_forced_by_any_distinction :
 116    (∃ K : Type, Nonempty K ∧ ∃ x y : K, x ≠ y) →
 117    Nonempty SpacetimeEmergenceCert ∧
 118    Nonempty TimeAsOrbitCert ∧