Gravity Conditional Slot

ConditionalSlot

A conditional slot, in the framework's machine-checked library of formal theorems, is a named place where a proof's assumption is stored. The library is a collection of theorems whose correctness a computer has verified step by step. The slot's job is to make plain, at a glance, what a given result depends on. Before the fix, a proof could carry an assumption invisibly, so two theorems with completely different hidden premises looked identical from the outside. The conditional slot changes that by putting the assumption directly into the type, the formal signature that names what the theorem is about.

The problem this solves is a subtle one. An older style of proof used a shell, a container that held a proposition and a proof of it. That shell was always fillable, even with the proposition set to True, the trivially true statement. So a theorem that consumed such a shell could be built no matter what the intended assumption was. The shell carried no information. The conditional slot replaces that container with one where the proposition is a parameter, not a hidden field. A slot for True is visibly trivial; a slot for a hard convergence theorem is visibly that theorem. The computer now enforces the visibility that a naming convention could not.

The module proves four things. First, the old shell is always inhabited, meaning it can always be constructed and therefore proves nothing specific. Second, the lifted slot is inhabited if and only if its parameter holds, so it carries exactly the information of the assumption. Third, a slot for False is not inhabited, making a false assumption visibly unconstructable. Fourth, a two-field migration example shows the lift preserves content while exposing both assumptions in the type. These are formal theorems, checked by the kernel with zero unproved axioms.

In Recognition Science, this fix was applied across the quantum gravity claim surface on 2026-07-04. The flagship master surface was retyped, and a large coordination module that used the old shell was retired, its endpoint restated over explicit parameters. The practical consequence: when a reader encounters a theorem in the framework, they can now see exactly what it assumes. The conditional slot is the difference between a proof that says it depends on something and a proof that shows you what it depends on.

/-- **The shell is always inhabited**, by `⟨True, trivial⟩`. Hence its type
carries no information about what was assumed: every such shell can be
constructed, whether the intended `P` is a deep theorem or `True`. This is
exactly why a "theorem" consuming a shell hides its contingency. -/
theorem vacuousWitnessShell_always_inhabited : Nonempty VacuousWitnessShell :=
  ⟨{ P := True, holds := trivial }⟩

/-- **The slot is inhabited iff its parameter holds.** Unlike the vacuous shell,
the slot type carries exactly the information of `P`: you can build it precisely
when `P` is true. -/
theorem conditionalSlot_nonempty_iff (P : Prop) :
    Nonempty (ConditionalSlot P) ↔ P := by
  constructor
  · rintro ⟨s⟩; exact s.holds
  · intro hp; exact ⟨{ holds := hp }⟩

/-- `ConditionalSlot False` is **not** inhabited. The contrast with
`vacuousWitnessShell_always_inhabited` is the whole point: a false assumption is
now visibly unconstructable, whereas the vacuous shell would have been
constructed anyway with `P := True`. -/
theorem conditionalSlot_false_not_inhabited : ¬ Nonempty (ConditionalSlot False) := by
  rw [conditionalSlot_nonempty_iff]
  exact not_false

/-- Current Pattern-A status: the target type, its formal justification, and
the QG-surface application are all landed. -/
def patternALiftStatus : PatternALiftStatus where
  target_type_and_justification_landed := true
  repo_wide_lift_applied := true

What this page does not claim

The conditional slot does not itself prove any quantum gravity result; it only makes the assumptions of such proofs explicit. The fix does not change which theorems are true, only how their assumptions are represented.

Verify this page

Every tagged claim above names its theorem. To check one yourself rather than trust this page, elaborate the source module with Lean 4 and audit its axiom basis:

$ lake env lean IndisputableMonolith/Gravity/ConditionalSlot.lean
expected axiom basis: [propext, Classical.choice, Quot.sound] (the Lean kernel's standard three; no RS-specific axioms)

A page whose claims cannot be reproduced this way does not ship. In production, every anchor links to the exact declaration in the public source release, and this block carries the build receipt for the page itself.

Derived articles

This page is generated by a question-recursion engine: the questions its answers raise become the next pages. The current agenda, with open targets marked red: