NontrivialSpecification
plain-language theorem explainer
A structure encoding a predicate on carrier type K that holds for some elements and fails for others, thereby capturing a non-trivial sub-ontology. Researchers closing the absolute-floor program cite it when converting specifiability into object-level distinguishability. The definition is supplied directly as a record whose three fields are the predicate together with the two existential witnesses.
Claim. A non-trivial specification on a carrier $K$ is a predicate $P : K → Prop$ such that there exists at least one $x ∈ K$ with $P(x)$ and at least one $y ∈ K$ with $¬P(y)$.
background
The DistinguishabilityFromSpecifiability module implements Route B of the absolute-floor program. Its central observation is that a non-trivial specification is equivalent to the carrier being non-singleton, supplying the distinction required by the Law-of-Logic chain. The upstream MagnitudeOfMismatch.forces structure supplies the symmetry comparison used in related mismatch arguments, while Constants.K defines the dimensionless bridge ratio $K = ϕ^{1/2}$.
proof idea
Direct structure definition. The three fields (predicate and two witnesses) are supplied at construction time; no further lemmas or tactics are applied.
why it matters
The structure is the key object in AbsoluteFloorClosureCert.routeB and AbsoluteFloorWitness.nontrivial_specifiable. It completes the Route B step that converts a proper ontology into bare distinguishability, feeding the equivalence theorems distinguishability_iff_nontrivial_specifiability and at_most_one_of_no_nontrivial_specification. It thereby supplies the object-level distinction presupposed by the T0–T8 forcing chain.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.