bare_distinguishability_of_absolute_floor
plain-language theorem explainer
The absolute-floor witness on a nonempty carrier K entails the existence of distinct elements x and y in K. Foundational work in Recognition Science cites this to confirm that the absolute-floor precondition delivers bare distinguishability without additional postulates. The proof is a one-line wrapper applying the right-to-left direction of the equivalence between distinguishability and nontrivial specifiability to the witness structure.
Claim. Let $K$ be a nonempty type. If $h$ is an absolute-floor witness for $K$ (requiring meta-distinguishability of propositions and nonempty nontrivial specification on $K$), then there exist $x, y : K$ with $x ≠ y$.
background
The module AbsoluteFloorClosure supplies a joint certificate that distinguishability is equivalent to non-trivial specifiability on an inhabited carrier. The absolute-floor witness is the structure requiring both meta-language distinguishability of propositions and the existence of a non-trivial specification on $K$. This theorem extracts the object-level distinguishability from the specifiability component of the witness.
proof idea
This is a one-line wrapper that applies the mpr direction of distinguishability_iff_nontrivial_specifiability to the nontrivial_specifiable field of the absolute-floor witness.
why it matters
This result supplies one direction of the equivalence absolute_floor_iff_bare_distinguishability, establishing that the absolute-floor witness is equivalent to bare distinguishability. It closes a foundational precondition: the universe of discourse must be non-singleton for any non-vacuous specification. The module notes that this floor is the logical precondition for stating specifications rather than an RS-specific physical postulate.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.
papers checked against this theorem (showing 19 of 19)
-
Attention filter detects poisoned passages in RAG
"Stealth Attack Distinguishability Game (SADG)... The attack is said to be τ-stealthy if, for all PPT defenders D, the advantage is at most τ"
-
Bipolar ramp loss beats MRT on weak seq2seq tasks
"MRT NEG (assign −1 to bad parses) improves MRT; bipolar ramp still superior"
-
Three views explain information flow and loss in distributed systems
"based on elementary distinguishability of observations, and classical causality, with history. Three distinct views of a system are sought... how information is transmitted (and lost)"
-
Subtraction of features beats addition for medical segmentation
"the SU highlights the useful difference information between the features and eliminates the interference from the redundant parts"
-
Weisfeiler-Leman turns graph datasets into XAI benchmarks
"Our approach leverages the Weisfeiler-Leman color refinement algorithm to efficiently perform approximate subgraph matching and mine class-discriminating motifs, which serve as proxy ground-truth class explanations. At the same time, we ensure that these motifs can be learned by GNNs because their discriminating power aligns with WL expressiveness."
-
ToaST cuts tokens over 11% vs BPE at large vocabularies
"ToaST greedily splits each pretoken into a full binary tree using precomputed byte n-gram counts, independent of any vocabulary."
-
Short Resolution proofs of Ref(φ) extract satisfying assignments
"block-width lower bound via Prover-Delayer game on Ref formulas"
-
Background interference, not size, limits high-res MLLMs
"performance increases monotonically with mask ratio on both single and multi-object tasks. This demonstrates that complex background semantics significantly distract MLLMs."
-
Hypothesis test picks samples to unlearn data domains
"We formalize this using a hypothesis test of the edited data with the desired and unwanted domains... trade-off function T(P,Q)(α) := inf ..."
-
Multimodal LLMs let robots recognize themselves from sensory streams
"differentiation, discriminating self-generated from external events through sensorimotor contingencies"
-
Symmetrization of Dirac neutrino amplitudes violates lepton number
"A Dirac neutrino is distinguishable from the corresponding antineutrino. Therefore, for a final state containing a pair of Dirac neutrino and antineutrino there is no need to do any symmetrization with respect to their momentum exchange."
-
Anchored bridges encode inputs into noisy diffusion states
"We show theoretically that process-level anchoring induces pathwise input distinguishability, injects information about x into noisy states, and creates a direct gradient pathway unavailable to NDPs."
-
ACQ reuses QITE unitaries and compresses circuits to cut optimizations
"ITE is a gradient flow on the complex projective plane CP^N... distinguishability measure S"
-
Asymmetry bounds speed of quantum observable change
"the upper bound ... is a bonafide measure of the asymmetry ... of the state ϱ(t) relative to the group of unitary translations {U_θ = e^{-iKθ}}"
-
Efficient Sparse Selective-Update RNNs for Long-Range Sequence Modeling
"the effective credit-assignment depth scales with the number of informative updates |Uon_i(s,t)| rather than sequence length"
-
Expert fusion model lifts microbial operon accuracy
"hconf_ij = E_conf [|zp_ij − zb_ij|; zp_ij − zb_ij]"
-
Affine recurrent nets cannot correct state errors
"Theorem 1 (Affine neutrality on the symbolic subspace). ... As|U = I"
-
Token selector approximates full video compute at lower cost
"We propose 'top1-distance', which ranks each token by its distance to its nearest neighbor in feature space... U_{x,y,t}=1−max_{(x',y',t')≠(x,y,t)} cos(z^{DINOv3}_{x,y,t}, z^{DINOv3}_{x',y',t'})"
-
Stochastic models yield free-boundary equations for trait extinction
"only paths fs such that Fs(f)>0 for all s∈[0,t] are admissible: the population gets extinct on the way otherwise"