theorem
proved
reality_from_one_distinction
show as:
view math explainer →
From ∃ x y, x ≠ y the structure of reality is forced.
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
depends on
-
K -
K -
carrier -
carrier -
absolute_floor_of_bare_distinguishability -
bool_absolute_floor -
c_rs_eq_one -
G_algebraic_in_φ -
is -
RealityCertificate -
is -
timeAsOrbitCert_inhabited -
exists_logicRealization_of_distinction -
is -
is -
and -
lightlike_iff_speed_c -
spacetime_emergence_cert_nonempty
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 ∧
papers checked against this theorem (showing 30 of 2803)
-
Coordination types trade robustness for scalability in agent scheduling
"We focus on four representative coordination paradigms: centralized, hierarchical, heterarchical, and holonic... Our controlled evaluations reveal clear coordination trade-offs"
-
Spike forecasting ranks brain regions consistently across models
"ANCOVA model (model_r ~ log_rate + fano + region) reaches R²=0.275... region ΔR²=0.018 above firing-statistics covariates"
-
Early low progress raises dropout by 25 points in engineering
"We employ G-estimation of structural nested mean models ... complemented by marginal structural models with inverse probability weighting ... low early academic capital increases dropout probability by 25.3 percentage points"
-
Benchmark shows top multimodal models lag on e-commerce
"OxyEcomBench ... 29 tasks ... four-level P0–P3 rubric ... visually salient multimodal cases"
-
Diffusion model ranks beams from geometry to cut training overhead
"We recast beam alignment as a generative task and propose a conditional diffusion model that learns a probabilistic beam prior from compact geometric and multipath features... Using a ray-traced DeepMIMO scenario with an 8-beam DFT codebook"
-
Left ideals give representation-free quantum graph morphisms
"A notion of categorical (co)limit of quantum graphs follows"
-
Any particle action made invariant under gauged Galilean transformations
"any action for N interacting particles can be made invariant under gauged Galilean transformations"
-
MoSe2/PdSe2 stack lifts A-exciton emission sixfold
"DFT calculations... valence band alignment... hybridization... B-exciton quenching"
-
Signal precision can lower screening accuracy when high
"V(ρ) non-monotone ... pitfall when ρ large because strategic effect on extensive margin dominates"
-
Single LISA-like detector measures gravitational-wave memory at SNR 10+
"TDI response... X1(t)=(y13+D13y31+...)−(3↔2); optimal SNR ρ²=⟨a|a⟩"
-
Multislot 5G NR meets UAV sensing accuracy targets
"The CRLB for the estimation of d and vϕ can then be expressed as... det(I(τd,vϕ,ψ))"
-
Plectic Heegner classes control higher-rank elliptic curves
"We produce these functions through the uniformization of Shimura curves – rather than higher dimensional quaternionic Shimura varieties – our results are compatible with a plectic refinement of Tate's conjectures."
-
Multi-virtual twin groups admit exactly eight 2-local representation types
"We classify all homogeneous 2-local representations of M_kVT_n into GL_n(C) for all k >= 1 and n >= 3, and show that they fall into exactly eight distinct types."
-
Infinitesimals formalized without axiom of choice
"A ringinal is a concept of infinite number, arithmetic in nature, different from Cantor's transfinite ordinals and cardinals... Analysis with unlimited numbers (via the predicate standard) is possible in a conservative extension of Zermelo-Fraenkel set theory"
-
Four-face SiPM readout hits 68 ps timing resolution
"measured cosmic muon velocity of (2.887±0.006)×10^8 m/s"
-
Diffusion model downscales weather forecasts to 30 km with added skill
"We introduce a probabilistic diffusion-based method for global atmospheric downscaling"
-
Efficiency turns video generators into world simulators
"The rapid evolution of video generation has enabled models to simulate complex physical dynamics and long-horizon causalities, positioning them as potential world simulators."
-
Mechanical feedback alone creates active growth layers at cell colony edges
"An emergent mechanical length scale, denoted by χ, sets the extent of the proliferative region"
-
No TeV emission found from spider millisecond pulsars
"We employ five quasi-differential energy bins... stacking technique to assess the statistical evidence of the cumulative emission... TS≡2 ln(L(K)/L(K=0))"
-
Enriched Zr-96 sets new limit on double beta decay
"The most stringent limit... T1/2(0ν+2ν)>3.9×10^19 yr (90% C.L.)... using three low-background HPGe detectors... Geant4.10.04.p03"
-
Text prompts let ChatGPT team with vision experts for image tasks
"We propose MM-REACT, a system paradigm that integrates ChatGPT with a pool of vision experts to achieve multimodal reasoning and action... MM-REACT introduces a textual prompt design that can represent text descriptions, textualized spatial coordinates, and aligned file names for dense visual signals such as images and videos."
-
Speckle imaging finds companions around 12 percent of RR Lyrae stars
"From these observations we can estimate an RRL binary fraction higher than 12%, ruling out a binary fraction higher than 25% at the 99% confidence level."
-
Births deviate slightly from random coin tosses
"beta-binomial ... Markovian children ... simulated log-likelihoods"
-
Extended SBA adds two-layer architecture for strategic scenarios
"SBA occupies a semiformal position between these paradigms by combining qualitative content with checkable structural constraints."
-
Full OA aligns closer to patents than hybrid OA
"Figure 2... log2 enrichment... hybrid and bronze OA... diamond OA sharply under-represented"
-
Bayesian co-evolution of code and tests lifts LLM accuracy
"By anchoring this search on minimal public examples, BACE prevents the co-evolutionary drift typical of self-validating loops."
-
Cyclic division algebras have no abelian maximal subgroups
"We prove that no cyclic division algebra (in the sense of Dickson) admits an abelian maximal subgroup in its multiplicative group."
-
Roman microlensing may detect 20x drop in planets near isolation mass
"We perform 1D pebble-accretion population synthesis simulations... combined effects of planetary migration and runaway gas accretion create an occurrence break."
-
Memory system reuses agent plans across unrelated tasks
"APEX-EM introduces a Procedural Knowledge Graph (PKG) ... structural signature—an abstract operation sequence (e.g. [entity_resolution → temporal_filter → aggregation])"
-
Memory coherence caps how many qubits can be teleported
"Results show that memory coherence is the main scalability bottleneck under stringent fidelity targets"