docs(slot): list only reachable justifiable-slot examples (#1125)

The inline comments for the perfect-square and pronic rules listed
delta values (1, 2, 4) that the immediate-window early return catches
first, so they never reach those checks. Annotate that the small
values are handled by Rule 1 and show the first delta that actually
reaches each rule (square 9, pronic 6).

Co-authored-by: Claude Opus 4.8 (1M context) <noreply@anthropic.com>

Author: tcoratger

src/lean_spec/spec/forks/lstar/slot.py

@@ -60,14 +60,17 @@ def is_justifiable_after(self, finalized_slot: "Slot") -> bool:
 
         # Rule 2: Slots at perfect square distances are justifiable.
         #
-        # Examples: delta = 1, 4, 9, 16, 25, 36, 49, 64, ...
+        # Smaller squares 1 and 4 already returned under Rule 1.
+        # First square that reaches here is 9: delta = 9, 16, 25, 36, 49, 64, ...
         # Check: integer square root squared equals delta
         if math.isqrt(delta) ** 2 == delta:
             return True
 
         # Rule 3: Slots at pronic number distances are justifiable.
         #
         # Pronic numbers have the form n(n+1): 2, 6, 12, 20, 30, 42, 56, ...
+        # The smallest pronic 2 already returned under Rule 1.
+        # First pronic that reaches here is 6: delta = 6, 12, 20, 30, 42, 56, ...
         # Mathematical insight: For pronic delta = n(n+1), we have:
         #   4*delta + 1 = 4n(n+1) + 1 = (2n+1)^2
         # Check: 4*delta+1 is an odd perfect square