Foundation Seam Bridge Bridge

The derivation bridge

A derivation bridge is a formal translation device. It pairs each element of one system with an element of another, and it requires that a single operation on the first system always corresponds to a single operation on the second. The map must respect that operation perfectly: apply the operation before the translation, or after it, and the result is the same. This is the property mathematicians call a homomorphism, and it is the load-bearing idea behind the structure.

The purpose of the bridge is to let theorems travel. If a theory proves something about repeated applications of its operation, the bridge guarantees the same statement holds for the corresponding repeated applications on the primitive side. The formal theorem transport_iterate states exactly this for every natural number of iterations. A corollary handles the special case of a fixed point: if an operation leaves an object unchanged on the primitive side, its translated image is a fixed point on the theory side. These are not new physical assumptions; they are consequences of the bridge's defining property.

The bridge is part of a broader accounting system in Recognition Science. The framework's coverage ledger classifies every module by how its results are obtained. A module marked transported means its theorems follow from a bridge rooted in distinction, the primitive starting point. A module marked posited means it rests on a named extra commitment beyond that starting point. The third tag, unclassified, is forbidden at completion, so every module must eventually declare which kind of support it has.

The bridge itself is a structure with four parts: a carrier map between the two systems, an operation on the primitive side, an operation on the theory side, and a proof that the map intertwines them. The theory-side operation must be the genuine one from the theory. Mapping to a trivial operation proves nothing and is explicitly forbidden by the structure's commitment. This rule keeps the bridge honest: it only transports real structure, not convenient fictions.

In plain language, the bridge establishes a reliable route for moving theorems from a minimal foundation into a richer theory. It does not invent new physics. It certifies that whatever the primitive side can prove about its own dynamics, the theory side inherits through the bridge. This is a formal guarantee, checked by a machine, that the theory's dynamical results are not free-floating assumptions but consequences of the primitive structure.

/-- A single-operation derivation bridge: a map from a delta-side carrier `Src`
to a theory carrier `Tgt` that intertwines a source operation `srcOp` with a
target (theory) operation `tgtOp`. This is the homomorphism whose existence lets
the theory's dynamical theorems transport from the delta side. A faithful bridge
must use the genuine theory operation as `tgtOp`; mapping to a trivial operation
proves nothing and is forbidden by the commitment. -/
structure OpBridge (Src Tgt : Type*) where
  /-- The carrier map from the delta-rooted object to the theory carrier. -/
  carrier : Src → Tgt
  /-- The delta-side operation (built from distinction). -/
  srcOp : Src → Src
  /-- The genuine theory operation the bridge must preserve. -/
  tgtOp : Tgt → Tgt
  /-- Primitive preservation: the bridge intertwines the two operations. -/
  preserves : ∀ s, carrier (srcOp s) = tgtOp (carrier s)

/-- 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

/-- The honest per-module classification used by the coverage ledger.
`transported` means the module's theorems follow from a derivation bridge rooted
in distinction; `posited name` means the module rests on the named extra
commitment beyond delta; `unclassified` is the only state the standing commitment
forbids at completion. -/
inductive CoverageTag where
  /-- Theorems follow from a delta-rooted bridge. -/
  | transported
  /-- Rests on a named extra commitment beyond distinction. -/
  | posited (name : String)
  /-- Not yet classified (forbidden at completion). -/
  | unclassified
  deriving DecidableEq, Repr

/-- A single-operation derivation bridge: a map from a delta-side carrier `Src`
to a theory carrier `Tgt` that intertwines a source operation `srcOp` with a
target (theory) operation `tgtOp`. This is the homomorphism whose existence lets
the theory's dynamical theorems transport from the delta side. A faithful bridge
must use the genuine theory operation as `tgtOp`; mapping to a trivial operation
proves nothing and is forbidden by the commitment. -/
structure OpBridge (Src Tgt : Type*) where
  /-- The carrier map from the delta-rooted object to the theory carrier. -/
  carrier : Src → Tgt
  /-- The delta-side operation (built from distinction). -/
  srcOp : Src → Src
  /-- The genuine theory operation the bridge must preserve. -/
  tgtOp : Tgt → Tgt
  /-- Primitive preservation: the bridge intertwines the two operations. -/
  preserves : ∀ s, carrier (srcOp s) = tgtOp (carrier s)

What this page does not claim

No specific physical theory is named as having been transported in this module. No claim that the bridge itself derives new physics; it only transports existing theorems. No claim about which modules are currently marked transported versus posited.

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: