distinguishability_from_specification
Specifiability of a non-trivial sub-ontology on a type K forces the existence of at least two distinct elements in K. Researchers tracing Route B of the absolute-floor program cite this result to ground the Law-of-Logic chain in basic distinguishability. The proof extracts the predicate and its inside/outside witnesses from the NontrivialSpecification structure then derives a contradiction from the assumption that those witnesses coincide.
claimLet $K$ be a type. Suppose there exists a predicate $P : K → Prop$ together with witnesses $x, y : K$ such that $P(x)$ and $¬P(y)$. Then there exist distinct elements $a, b ∈ K$.
background
The module DistinguishabilityFromSpecifiability implements Route B for the absolute-floor program. Its central structure NontrivialSpecification K packages a predicate inOntology : K → Prop with two existential witnesses: someInside asserting that the predicate holds for at least one element and someOutside asserting that it fails for at least one element. The module documentation states that such a specification already supplies the distinction needed by the Law-of-Logic chain.
proof idea
The tactic proof obtains the components ⟨P, ⟨x, hx⟩, ⟨y, hy⟩⟩ directly from the NontrivialSpecification hypothesis S. It refines the goal to the pair x, y together with a proof of inequality. Assuming x = y, the simpa tactic substitutes to produce P y from hx, which contradicts the witness hy : ¬P y.
why it matters in Recognition Science
This theorem supplies the forward direction of the equivalence proved in the downstream result distinguishability_iff_nontrivial_specifiability. It fills the key step in Route B of the absolute-floor program, showing that specifiability forces distinguishability as required by the Law-of-Logic chain. The parent equivalence then equates non-singleton carriers with the existence of NontrivialSpecification instances.
scope and limits
- Does not assume K is inhabited independently of the given specification.
- Does not construct the distinct elements beyond the supplied witnesses.
- Does not apply when the predicate is trivial (always true or always false).
- Does not address computational or metric notions of distinguishability.
- Does not depend on numerical constants such as phi or the bridge ratio K.
Lean usage
example {K : Type*} (S : NontrivialSpecification K) : ∃ x y : K, x ≠ y := distinguishability_from_specification Sformal statement (Lean)
27theorem distinguishability_from_specification
28 {K : Type*} (S : NontrivialSpecification K) :
29 ∃ x y : K, x ≠ y := by
proof body
Tactic-mode proof.
30 obtain ⟨P, ⟨x, hx⟩, ⟨y, hy⟩⟩ := S
31 refine ⟨x, y, ?_⟩
32 intro hxy
33 have hyx : P y := by
34 simpa [hxy] using hx
35 exact hy hyx
36
37/-- Any non-empty proper subtype is a non-trivial specification. -/