AbsoluteFloorWitness
Why this theorem is linked from On the local Langlands conjectures for disconnected groups unclear
Pith linked this Lean declaration because the review connected a specific passage in the paper to this theorem. The relation tag says how strong that connection is; it is not a generic placeholder.
normalized twisted transfer factor Δ_KS... absolute invariant inv(γ,(z,δ)) ∈ H^1_a(Γ,S⇒S)
Relation between the paper passage and the cited Recognition theorem.
plain-language theorem explainer
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.
Claim. Let $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
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.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.
papers checked against this theorem (showing 1 of 1)
-
Langlands conjecture holds for disconnected groups with toral core
"normalized twisted transfer factor Δ_KS... absolute invariant inv(γ,(z,δ)) ∈ H^1_a(Γ,S⇒S)"