Fractal.lean

View source on GitHub

passthrough / theorem passthrough_preserves

At zero bits, Consolidate cannot select: it returns the input policy unchanged (pure pol). This is the budget floor. Passthrough trivially preserves any contract because the output equals the input.

def passthrough [Monad M] (pol : α) (_ : β) : M α := pure pol

Budget termination

The bit budget at depth d is initial - d. Each level costs at least 1 bit (Filter is strictly lossy). The budget reaches zero at depth = initial, and stays zero beyond. Tower height is bounded by the initial bit count.

theorem budget_strictly_decreases (initial d : Nat) (hd : d < initial) :
    bits_at_depth initial (d + 1) < bits_at_depth initial d

tower_consolidate

The recursive construction. At depth 0: passthrough. At depth d+1: encode (policy, persisted) as raw input, run the inner pipeline's cycle, extract the updated policy. The inner pipeline shares forward stages with the base but uses depth-d consolidation. This self-similarity is what makes the six roles appear at every scale.

def tower_consolidate [Monad M] [LawfulMonad M]
    {I : InterfaceTypes}
    (base : Pipeline M I)
    (encode : I.policy → I.persisted → I.raw)
    : Nat → I.policy → I.persisted → M I.policy
  | 0, pol, _ => pure pol
  | d + 1, pol, per =>
    let inner : Pipeline M I :=
      { base with consolidate := tower_consolidate base encode d }
    inner.cycle (encode pol per) pol >>= fun result =>
    pure result.1

; Fractal tower: recursive consolidation with budget
; At depth 0 => passthrough (return input unchanged)
; Each level costs 1 bit; at 0 bits, recursion stops.

(define (tower-consolidate depth policy persisted)
  (if (= depth 0)
    policy  ; passthrough — no bits left
    (let* ((inner-policy
             (tower-consolidate (- depth 1) policy persisted))
           (updated (string-append inner-policy "+")))
      updated)))

(define (bits-at-depth initial d)
  (max 0 (- initial d)))

; Tower with 3-bit budget
(display "depth 0 (0 bits): ")
(display (tower-consolidate 0 "p0" "data"))
(newline)
(display "depth 1 (2 bits): ")
(display (tower-consolidate 1 "p0" "data"))
(newline)
(display "depth 3 (0 bits): ")
(display (tower-consolidate 3 "p0" "data"))
(newline)
(display "budget: ")
(do ((d 0 (+ d 1))) ((> d 4))
  (display (bits-at-depth 3 d))
  (display " "))
(newline)
(display "Terminates: budget hits 0 at depth=initial")

# Fractal tower: recursive consolidation with budget
# At depth 0 => passthrough (return input unchanged)
# Each level costs 1 bit; at 0 bits, recursion stops.

def tower_consolidate(depth, policy, persisted):
    if depth == 0:
        return policy  # passthrough — no bits left
    inner_policy = tower_consolidate(depth - 1, policy, persisted)
    return inner_policy + "+"

def bits_at_depth(initial, d):
    return max(0, initial - d)

# Tower with 3-bit budget
print(f"depth 0 (0 bits): {tower_consolidate(0, 'p0', 'data')}")
print(f"depth 1 (2 bits): {tower_consolidate(1, 'p0', 'data')}")
print(f"depth 3 (0 bits): {tower_consolidate(3, 'p0', 'data')}")
print("budget:", " ".join(str(bits_at_depth(3, d)) for d in range(5)))
print("Terminates: budget hits 0 at depth=initial")

tower_preserves_up

Up-induction (the life_at_zero path). Start at passthrough (depth 0): output = input, trivially preserves the postcondition. Build upward: if depth d preserves for a given policy, depth d+1 does too. This is the constructive path — observe life, build the mechanism step by step.

The proof uses induction on d. Base case: support of pure pol is {pol}, so the postcondition holds. Inductive step: decompose the cycle, extract that the output policy came from tower(n) applied to the same input policy, apply the induction hypothesis.

tower_preserves_down

Down-induction (the god_is_real path). If the postcondition holds for all policies universally (because purpose guarantees it), the tower preserves at every depth. No step-by-step construction needed — the premise gives the conclusion immediately.

tower_satisfies_hcon

The combined result. The coupling lemma's hypothesis (hcon) is satisfied at every tower depth under either reading of the foundation axiom. The left branch (life_at_zero) feeds the weak form of cycle_preserves_policy; the right branch (god_is_real) feeds the strong form. Both converge on the same conclusion.

Connections

• Handshake.lean — imported; provides cycle_preserves_policy and PipelineHandshake
• Induction.lean — the foundation axiom's disjunction is mirrored in the two tower directions
• Contracts.lean — passthrough preserves any Contract