AbsoluteFloorWitness
AbsoluteFloorWitness K packages the conditions that the meta-language distinguishes propositions and that K admits a non-trivial specification. It is referenced in the absolute-floor closure certificate and in equivalence theorems linking it to bare distinguishability on nonempty carriers. The structure definition introduces no additional proof obligations beyond naming the two fields.
claimLet $K$ be a nonempty type. An absolute floor witness on $K$ is a structure asserting the existence of distinct propositions $P, Q$ and the nonemptiness of the type of non-trivial specifications on $K$.
background
AbsoluteFloorClosure establishes a joint certificate for the absolute-floor program. The key definitions are NontrivialSpecification, which requires a predicate on $K$ that is true for some elements and false for others, and the absolute-floor witness itself. Upstream results include the definition of $K$ as the square root of phi from Constants and the forces structure providing mismatch detection.
proof idea
As a structure definition, AbsoluteFloorWitness directly declares the two fields meta_distinguishes and nontrivial_specifiable without invoking any lemmas or tactics. It is used as a hypothesis in the surrounding theorems that establish equivalence to bare distinguishability.
why it matters in Recognition Science
The witness appears in AbsoluteFloorClosureCert to certify the joint closure and in bool_absolute_floor to realize it on Bool. It supports the reduction of the forcing-chain floor to meta-language distinguishability plus a non-singleton universe, as described in the module doc. This step precedes the introduction of the J-function and the phi fixed point in the Recognition Science chain.
scope and limits
- Does not derive physical laws or constants from the witness.
- Does not specify a concrete model for $K$ beyond the Bool example in downstream theorems.
- Does not address the J-uniqueness or eight-tick octave steps.
formal statement (Lean)
25structure AbsoluteFloorWitness (K : Type*) [Nonempty K] : Prop where
26 meta_distinguishes : ∃ P Q : Prop, P ≠ Q
27 nontrivial_specifiable : Nonempty (NontrivialSpecification K)
28
29/-- The absolute-floor witness forces bare distinguishability. -/