absolute_floor_iff_bare_distinguishability
plain-language theorem explainer
The equivalence shows that for any nonempty type K the absolute-floor witness holds exactly when K contains at least two distinct elements. Foundational work on Recognition Science cites this result to close the absolute-floor program by reducing it to bare distinguishability without extra physical assumptions. The proof is a direct term-mode pairing of the two one-directional lemmas already proved in the same module.
Claim. For any nonempty type $K$, the absolute-floor witness on $K$ (the conjunction of meta-language distinction of propositions and existence of a nontrivial specification on $K$) holds if and only if there exist distinct $x, y : K$.
background
The module AbsoluteFloorClosure supplies a joint certificate that the absolute floor reduces to bare distinguishability. The structure AbsoluteFloorWitness $K$ on a nonempty carrier $K$ requires two components: meta_distinguishes asserting existence of distinct propositions $P, Q$ and nontrivial_specifiable asserting Nonempty(NontrivialSpecification $K$). Module documentation states that the closure is modest because distinguishability equates to non-trivial specifiability on an inhabited carrier while the meta-language already distinguishes propositions, so the floor is merely the precondition of a non-singleton universe of discourse.
proof idea
The proof is a term-mode construction returning the pair of bare_distinguishability_of_absolute_floor and absolute_floor_of_bare_distinguishability. This directly assembles the biconditional from the two directional results already established in the module.
why it matters
This theorem completes the absolute-floor closure by showing equivalence to bare distinguishability, confirming that the floor is a logical precondition rather than an RS-specific postulate as stated in the module documentation. No downstream uses appear, so the result functions as a terminal foundational fact. It touches the question of whether meta-language distinction of propositions needs further justification beyond standard logic.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.
papers checked against this theorem (showing 30 of 1559)
-
Wavelet multiscale method converges O(H) for Helmholtz in perforations
"The sesquilinear form a satisfies boundedness and Gårding’s inequality; well-posedness via Cap(k)."
-
Disentangled reps reveal which proxies drive model decisions
"adversarial autoencoders... LEnc = MSE(x, x̂) − β MSE(p, p̂)... f disentangles p from the other features"
-
Statistical tests compare sentiment algorithms without human labels
"We will motivate the use of marginal homogeneity tests, as well as log linear models within the framework of maximum likelihood estimation"
-
Lagrangian yields analytical gradients for hybrid quantum methods
"the Lagrangian formalism of Helgaker for analytical derivatives of approximate wavefunctions"
-
Unique solutions exist for mean-field FBSDEs with jumps
"The functions b,h,σ and β are Lipschitz in (x,y,z,k) ... W₂(ν,ν′)"
-
Indistinguishability across contexts models quantum contextuality
"properties describing the same physical quantity, but belonging to different measurement contexts, are indistinguishable in a strong sense... quasi-set theory, which is a set-theoretical framework built to describe collections of elements that violate Leibnitz’s principle of identity of indiscernibles"
-
Maximal 3-independent set yields FPT domination on nowhere dense graphs
"For r = 3, the problem is W[2]-hard for general graphs but in FPT for nowhere dense classes and it admits a linear kernel for bounded expansion classes."
-
Focal adhesion growth explains why cells spread on stiff substrates
"No mention of reciprocal cost, golden-ratio identities, or parameter-free constant derivation"
-
Only one inertial frame can be isotropic without contradictions
"the equivalence of inertial frames under the constancy of the speed of light is mathematically infeasible. If two velocities are non-collinear, the Mocanu paradox... is caused"
-
Finite volume method handles battery voltage jumps at interfaces
"We use a simple analytical test case to validate our model... The simulated electric potential... fits perfectly to the analytical solution."
-
DC algorithm solves IRS-NOMA power minimization
"rank(X) = 1 ⇔ Tr(X)−∥X∥₂ = 0"
-
Direction constraints speed Bayesian optimization under budgets
"Vmf(g|θ,κ)=Cd(κ)exp(κθ^T g) ... posterior p(gt+1|xt+1) via VMF update rules"
-
Stress-driven model equates nonlocal thermoelastic nanobeams to differential equations
"stress-driven nonlocal integral theory recently proposed by G. Romano and R. Barretta"
-
Exchange term mixes only triplet excitons in TMD monolayers
"excitons are first defined in the subspace of electron- and hole states, including the lowest conduction band (LCB) and the uppermost valence band (UVB). Both bands are spin degenerate at the Gamma-point. All other states are neglected."
-
Raman-μSFA detects single water monolayer at confined interfaces
"independent optical paths for (i) the illumination and imaging of Newton's Rings and (ii) Raman-mode excitation"
-
Variance reduction matches optimal complexity for composite nonconvex problems
"Assumption 1... f and g_ξ Lipschitz and smooth... LF = ℓ_g² Lf + ℓf Lg"
-
POD Riccati feedback stabilizes infinite-dimensional system
"Assumptions (H1)–(H3) on the orthogonal decomposition H = E_ℓ ⊥ F_ℓ with A-invariant subspaces and exponential stability on F_ℓ"
-
Poincaré generators get explicit Euclidean representations
"The identification of the complex Euclidean group with the complex Poincaré group relates the infinitesimal generators"
-
Convex hull of upload-download pairs achieved for secure matrix mult
"secure encoding ˜An = sum Ai x^{i-1} + R x^{K-1} (MDS polynomial sharing)"
-
Smart contracts generate public random numbers no one can control
"The only way to influence the RL values then is for all producers to collaborate with each other and also with a group of miners."
-
Empathic DQN cuts collateral harms by swapping agent positions
"We assume a setting where a learning agent coexists with other independent agents (who receive unknown rewards), where some types of reward (e.g. negative rewards from physical harm) may generalize across agents."
-
VAE-compressed review vectors improve multi-criteria recommendations
"the proposed latent multi-criteria rating approach outperforms several baselines significantly and consistently"
-
Uncertainty reward in scene completion yields transferable look-around policies
"sidekick policy learning, which exploits the asymmetry in observability between training and test time"
-
Scalar-field CSL model collapses two clumps to one
"It is shown that, with high probability, the solution for Ĥ=0 favors collapse toward eigenstates of the scalar field whose eigenvalues are close to ∼χi(x)."
-
Overlapping coefficient finds minimum coverage for optimal localization
"The calibration procedure works under the assumption that the similarity of the normal distributions... diverges as sensor coverage... changes."
-
Lyapunov function yields ionization freeze-out in supernovae
"the system completely recombines in the equilibrium approximation on long time scales, which does not occur in reality"
-
Stricter points-to logic requires non-overlapping heap vertices
"A heap graph is a directed connected simple graph... must be pointed by at least one variable from the local stack"
-
Quasi-holes account for perturbations in Laughlin states
"incompressibility estimate... ρF ≤ B/(2πℓ) (1+oN(1))"
-
Lumping reduces network epidemics to Markov population models
"we demonstrate that lumping can be used to reduce any epidemic model to a Markov Population Model (MPM). Therefore, we propose a novel lumping scheme based on a partitioning of the nodes. By imposing different types of counting abstractions..."
-
Elementary method yields axially symmetric processes on sphere
"As product of two valid covariances, K is a valid covariance (see Schur product theorem in Zhang [16])."