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 3051)
-
NNLO calculation gives positive J/ψ three-photon width matching data
"The dominant theoretical uncertainty originates from the renormalization scale variation"
-
RRT planner reaches visual goals via robot rendering gradients
"inertial gradient tree expansion that inherits optimization states across tree branches"
-
Ontology encodes EU Data Act rules for SPARQL compliance checks
"The DAOnt ontology reuses elements from three established ontologies, LKIF-Core, ODRL, and DPV, to capture the normative structure of the Data Act... supports compliance checking through SPARQL queries that return obligations, permissions, and prohibitions"
-
Ensemble checks catch wrong code better than single-model repeats
"Experiments on LiveCodeBench demonstrate that ESE correlates more strongly with program correctness than single-model semantic entropy"
-
SFT beats DPO and KTO for spoken pedagogical feedback
"We introduce SPFG... human-verified teacher-style feedback, including preferred/rejected feedback pairs for preference learning... comparing supervised fine-tuning (SFT) with preference-based alignment (using DPO and KTO)"
-
GFL stability bound set by GFM current-limit switching
"The findings reveal that the switched system's stability boundary coincides with that of the CLC subsystem... Lyapunov function V = ½Tϖ² + ∫(P_E - P_M)dθ"
-
Uniform vector minimizes spectral gap in biased transposition chains
"We decompose the transition matrix as K = 1/(n-1) ∑ E_r where each E_r is an elementary transition matrix... each E_r acts as an orthogonal projection... smallest positive eigenvalue of E_r + E_{r+1} is 1-m_p"
-
Voting across queries and answers fixes RAG double hallucinations
"simple, reliable ensemble voting is a superior and more efficient method for mitigating RAG hallucinations"
-
Multi-agent system reaches 83.8% success on cross-physics microstructure tasks
"83.8% success rate on 17 cross-physics tasks"
-
Quantum vacuum induces coherent states enabling new superconductivity
"integrates Keppler’s zero-point field resonance theory, the discrete causal structure... and the latest advancements in holographic superconductivity models"
-
LLMs identify top articles with over 80% accuracy
"Results show that LLMs perform well in coarse grained evaluation tasks, achieving accuracy above 0.8 in identifying highly recommended articles."
-
DMI scaling selects atomic 3q textures in Fe3GeXTe
"the frustrated out-of-plane DMI tends to favor atomic-scale 3q magnetic textures at the edge of the Brillouin zone"
-
Persistent pool scales max-ent synthesis to 50 attributes
"pλ(x) = 1/Z(λ) exp(∑ λj fj(x))"
-
Smartphone cameras match lab tools on sample concentrations
"A designated optical setup combined with image processing and data analyzing techniques was implemented... G/B ratio and grey scale value... database which converts data from the imaging device to concentrations"
-
LLM RAG framework predicts ESG scores with 0.48 correlation
"GRI-guided extraction module retrieves and synthesizes information aligned with specific standards"
-
Surrogates make EIG adjoint-compatible for experimental design
"the Gaussian tilting surrogate is exact in the linear-Gaussian setting"
-
Learned attention matches skip connections in medical scans
"XAttnRes maintains a global feature history pool... lightweight pseudo-query attention... spatial alignment and channel projection steps"
-
Galois cohomology rings arise as colimits of finite Koszul subalgebras
"Under a natural cohomological colimit hypothesis... H•(G,Fp) is asymptotically universally Koszul"
-
Domain wall fermions restore exact chiral symmetry at infinite fifth length
"We prove the recovery of exact chiral symmetry in the limit of an infinite fifth direction, and derive the effective four-dimensional operator satisfying the Ginsparg-Wilson relation obtained in this limit."
-
Switching involutions unify unstable graphs and shared double covers
"We unify both via lifting and guided folding, showing that they are governed by conjugacy classes of strongly switching involutions in Aut(CDC(G))."
-
Fake news detection works on new users by borrowing signals from others
"We construct an undirected global interaction-based graph G(UG, EG) ... node2vec ... GNN module"
-
Physical priors let one Retinex model fix multiple UHD degradations
"RetinexDualV2... secured 4th place in the NTIRE 2026 Day and Night Raindrop Removal Challenge"
-
Symmetries extend from Einstein-Maxwell to higher curvature spacetimes
"We will prove in this paper that we can extend these symmetries to spacetimes with higher curvature terms... the metric tensor invariance... implies that the left hand side of the differential equations is manifestly invariant"
-
LLM hidden states warp at digit-count boundaries
"structural input-format discontinuities (tokenisation, digit-count) sufficient for CP geometry"
-
EEG decoder adapts to any electrode setup and noise
"cross-modality knowledge transfer... skeleton decoder as teacher... KL divergence loss"
-
Taxonomy organizes embodied AI safety from perception to action
"We introduce a multi-level taxonomy that unifies fragmented lines of work... across the full embodied pipeline, from perception and cognition to planning, action & interaction, and agentic system."
-
Modal exchangeability decomposes Kripke frames into orbit-directed credal measures
"Theorem 3.1 (General modal de Finetti)... Ergodic decomposition... Conditional i.i.d. on O_∞."
-
Rewarding reasoning paths beats final-answer RL
"SARL constructs a per-response Reasoning Map from intermediate thinking steps and rewards its small-world topology... SR(G) = ½ C(G) + 1/(1+L(G))"
-
Disk buildup boosts outer CO ice over water
"CO-rich pebbles can be formed at the CO snow line due to the cold finger effect"
-
Regularity lowers black hole ringdown frequencies
"Using the Padé-improved WKB method... we compute representative quasinormal frequencies and find that larger regularity shifts the spectrum toward smaller oscillation frequencies and damping rates"