reality_from_one_distinction
From ∃ x y, x ≠ y the structure of reality is forced.
plain-language theorem explainer
Any inhabited carrier K admitting a non-trivial distinction forces the complete Recognition Science chain: absolute floor on K and on Bool, spacetime emergence with Lorentzian signature, time as orbit, and the algebraic derivations of c=1, ℏ and G from φ. Researchers deriving physics from bare distinguishability cite this as the master bundling result. The term-mode proof assembles the RealityCertificate by direct application of the upstream lemmas for each field.
Claim. Let $K$ be an inhabited type admitting a distinction $h : ∃ x,y : K, x ≠ y$. Then a RealityCertificate $K$ exists whose fields are the distinction $h$, the absolute-floor witness supplied by bare distinguishability, the native logic-realization instance, the absolute floor on Bool, the spacetime-emergence certificate, the light-cone condition, the time-as-orbit certificate, and the constant derivations $c=1$, $ℏ$ algebraic in $φ$, $G$ algebraic in $φ$.
background
RealityCertificate is the structure packaging the deliverables of the forcing chain for a carrier $K$. Its fields record the distinction hypothesis, the absolute-floor witness (Nonempty (AbsoluteFloorWitness $K$)), the logic-realization instance, the unconditional Bool absolute floor, spacetime emergence with Lorentzian signature, light-cone condition, time-as-orbit certificate, and the algebraic expressions for the constants. The module supplies the master theorem that threads absolute-floor closure, universal instantiation from distinction, time-as-orbit, spacetime emergence, and constant derivations into one deliverable. Upstream, absolute_floor_of_bare_distinguishability states that bare distinguishability supplies the nontrivial specification part of the absolute-floor witness, while bool_absolute_floor realizes it on the minimal carrier Bool.
proof idea
The proof is a term that constructs the RealityCertificate by supplying each field from an upstream result. The absolute_floor field is filled by absolute_floor_of_bare_distinguishability applied to $h$; native_realization by UniversalInstantiationFromDistinction.exists_logicRealization_of_distinction $K$ $h$; bool_floor by bool_absolute_floor; spacetime by spacetime_emergence_cert_nonempty; light_cone by lightlike_iff_speed_c; time_orbit by timeAsOrbitCert_inhabited; and the constants by c_rs_eq_one, ℏ_algebraic_in_φ, G_algebraic_in_φ respectively.
why it matters
This declaration bundles the forcing chain from one distinction into a single named theorem. It is invoked by reality_from_bool to produce the certificate on Bool and by terminalArrow_exists to obtain the terminal arrow for any distinguished carrier. Within the framework it completes the master forcing chain from the bare hypothesis of distinguishability through absolute-floor closure, spacetime emergence, and φ-derived constants, as described in the module documentation.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.
papers checked against this theorem (showing 30 of 8442)
-
iMiGUE-3K: A Large-Scale Benchmark for Micro-Gesture Analysis with Self-Supervised Learning
"Using a model-based crowd-sourcing data collection strategy, we construct iMiGUE-3K... 32 micro-gesture classes... MG-FMs... five comprehensive evaluation tasks: MG recognition... MG emotion recognition."
-
Persistence orders feature removal to control topology in generation
"PFlow-T does not fit the GenPhys template... substrate is a filtered chain complex... time parameter is a persistence threshold, not a clock."
-
VLMs match traditional face quality scores zero-shot
"Our results show biometric utility performance depends significantly on architecture, not merely on parameter count."
-
Tool converts violin sheet music photos to fingerboard videos
"The only part built from scratch is the lookup table that maps each musical note to a string and finger position on the violin."
-
Hardware search produces edge LLMs tuned to each device's bottlenecks
"Across four different hardware substrates, the searches converge to visibly different architectures whose shapes track each substrate's cost bottleneck"
-
KL-minimal principle corrects biases in visual feature visualization
"We establish a theoretical distributional view for visual MI, which models the influence of a feature activation on the natural image distribution"
-
Axion production bounds reheating temperature from both above and below
"The decay contribution falls as T_rh^{-2}, whereas the annihilation contribution grows approximately as T_rh^{4/3}"
-
Dense two-dimensional QCD behaves as a Luttinger liquid
"the infrared behavior is consistent with a Tomonaga–Luttinger liquid: the central charge is determined to be c=1, and the two-point function of the baryon-number density exhibits spatial modulation with the wavenumber predicted by Tomonaga–Luttinger liquid theory. The Luttinger parameter varies smoothly from K≃1 … to K≃1/2"
-
Activation steering cuts VLM age errors by up to 25%
"We propose an activation steering method that suppresses the shortcut by intervening on the hidden states of the VLM... f(x|¬k) ≈ a(x, t(x,p) + α·(t¬k − tk))"
-
Simulations replicate 23-Hz oscillations from Texas electronic load
"EMT simulations successfully reproduce the real-world event... simulated results closely matching the fault recorder data"
-
AI presence can be designed without personhood claims
"Presence is reframed as a designable interaction quality that can be tuned, constrained, and deliberately withdrawn... principles... emphasize relational coherence, honesty of limits, and accountable withdrawal."
-
State transitions keep recovering agents alive in LLM teams
"Agent states are divided into “Active”, “Standby”, and “Terminated” states... risk estimator to optimize agent state transitions by assessing hallucination risk"
-
First segmented 4H-SiC LGADs show charge separation with gain
"TPA-TCT measurements ... demonstrate clear charge separation between adjacent strips with internal gain, confirming functional segmentation."
-
Diffusion models generate controllable alternative streetscapes
"Quantitative evaluations show that incorporating visual controls can improve semantic consistency, reducing the LPIPS index by approximately 6%..."
-
Generic metrics fail to predict success in grounded presentation tasks
"We present UniPPTBench, a unified benchmark for presentation generation across four representative input settings: vague-prompt, long-document, multimodal-document, and multi-source generation. We further introduce UniPPTEval, a scenario-aware evaluation protocol that combines shared metrics... with scenario-specific metrics tailored to each setting’s core requirements."
-
Control loop raises LLM self-correction accuracy by 6.2 points
"We model LLM self-correction as a discrete-time closed-loop control system... yt+1 = G(x, yt, ut) ... ut = C(τ(et), s(et), ℓ(et))"
-
Multi-LLM systems converge semantically in closed loops
"Data Processing Inequality... exponential entropy contraction law... Algorithmic Lovelace Bound"
-
General mass matrix parameterization fits neutrino mixing data
"systematic and detailed study of the fermion flavor masses and mixings"
-
Duplex MLLMs top at 39.6% on real-time interaction benchmark
"Omni-DuplexEval contains 660 videos with fine-grained, human-annotated labels and precise temporal metadata, spanning 9 tasks... automatic evaluation framework based on LLM-as-a-Judge... jointly evaluating response-content alignment and response timing through timestamp-aware and sequential reasoning"
-
Offline priors initialize better multi-agent LLM graphs
"conditional variational graph framework to capture reusable structural regularities across domains in a latent space"
-
Four reasoning stages improve ECG diagnosis accuracy
"CardioThink ... explicitly models the diagnostic reasoning process through human-interpretable intermediate stages (rhythm, conduction, morphology, and impression) ... Structured Set Policy Optimization (SSPO) to jointly optimize adherence to this structured reasoning format"
-
Benchmark adds 1000 Lean proof targets from applied math
"We develop a dependency-recovery pipeline that reconstructs the local textbook context... semantic block decomposition... frozen-context block-wise construction."
-
Selective layers raise utility in private LLM fine-tuning
"Theorem 1 decomposes the effect of a noisy private update into a descent term and a perturbation-induced error term... dΛσ²C² captures the DP noise damage, which decreases with the number of trainable parameters."
-
Global coarse guidance stabilizes long video outpainting
"We first construct Global Coarse Guidance (GCG), a low-resolution representation that captures global structure and dominant motion across the video... via a novel global-local frame swapping mechanism that couples sparse global keyframes with local temporal windows"
-
LLM agent runs ROOT physics analyses from plain English prompts
"We present RooAgent as a natural-language interface for Root-based high energy physics data analysis. The package provides physics analysis functions as tools that an LLM agent invokes in response to plain-language prompts."
-
VLA driving explanations match scenes less than half the time
"We formalize faithfulness information-theoretically, define entity and action fidelity with verification criteria... I(R;T|X)≈0"
-
Hypergraph links text levels for stronger personality prediction
"Experiments on the Big Five personality dimensions show that... HyperPersona effectively integrates multi-level linguistic cues"
-
Sobel edges match finger knuckles at 17% rate
"After preprocessing an input finger it is compared to all the images of fingers in the dataset, one by one. We have obtained up to 17.02% of successful recognitions"
-
Weather data at U-Net bottleneck improves aerial thermal translation
"conditional U-Net that incorporates weather data at the bottleneck layer, complemented by targeted preprocessing and post-processing techniques... PSNR of 14.5485, SSIM of 0.8095, LPIPS of 0.1666"
-
High noisy-label accuracy fails to ensure OOD reliability
"We term this pathology uncertainty collapse... low-confidence ID-wrong samples occupy score and feature regions shared with OOD inputs"