Foundation Seam Bridge Bridge Transport Iterate

The transport guarantee

A ledger, a discrete record of events, can be built from a single primitive act of distinction: marking one thing as different from another. The framework's recognition cost, the forced price of marking such an event, then drives a chain of theorems about dynamics. The declaration transport_iterate guarantees that this chain is not a leap but a step-by-step translation.

Formally, the declaration proves a homomorphism property. If a bridge maps a source object (built from distinction) into a target theory, and the bridge preserves a single operation, then it preserves every repeated application of that operation. For any natural number n, applying the source operation n times and then mapping the result equals mapping first and applying the target operation n times. The proof is an induction on n, with the zero case trivial and the successor case following from the preservation property.

The consequence is a transport theorem: any statement about the theory's iterated dynamics, such as a stationary state after many steps, holds for the image of the corresponding source object. A fixed point of the source operation maps to a fixed point of the target operation. This is what lets the framework claim that its derived physics is genuinely carried over from the primitive distinction, rather than assumed separately.

What the declaration does not claim is just as important. It does not assert that any particular bridge exists; that is a separate construction. It does not claim that the target operation is the genuine theory operation, only that the bridge preserves whatever operation it is given. And it does not prove that the source operation itself is physically meaningful. The theorem is a conditional guarantee: if a faithful bridge exists, then iterated dynamics transport. The existence of such bridges, and their physical interpretation, remains a separate question.

/-- The transport core. A derivation bridge carries every iterate of the
delta-side operation to the matching iterate of the theory operation. Any theorem
of the theory phrased about iterated dynamics therefore transports to a statement
about the delta-rooted object: it suffices to read the theory's `tgtOp^[n]`
behaviour off the delta side's `srcOp^[n]`. -/
theorem transport_iterate (s : Src) :
    ∀ n : ℕ, B.carrier (B.srcOp^[n] s) = B.tgtOp^[n] (B.carrier s) := by
  intro n
  induction n generalizing s with
  | zero => simp
  | succ k ih =>
    rw [Function.iterate_succ_apply, Function.iterate_succ_apply, ih (B.srcOp s),
        B.preserves s]

/-- Corollary: a fixed point of the delta-side operation maps to a fixed point of
the theory operation. (A representative transported theorem: any "stationary
state" result of the theory holds for the delta image of a delta-side fixed
point.) -/
theorem transport_fixedPoint (s : Src) (hs : B.srcOp s = s) :
    B.tgtOp (B.carrier s) = B.carrier s := by
  have := B.preserves s
  rw [hs] at this
  exact this.symm

What this page does not claim

The declaration does not construct any specific bridge. The declaration does not prove that the source operation is physically meaningful. The declaration does not assert that the target operation is the genuine theory operation.

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/Foundation/SeamBridge/Bridge.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: