Foundation Pair Kernel Owner Channel Occurrence Bridge Bridged Occurrence Source

The orientation rule

In the Recognition Science framework, a ledger is a discrete record of events, and each event is an atomic posting that moves value between two accounts. The framework's library of machine-checked formal theorems proves a precise symmetry about these postings: the source covector, the object that assigns a signed weight to a posting, flips sign when the side flips. The declaration bridgedOccurrenceSourceCovector_orientation_equivariant states that for any account k and any probe vector v, the value assigned to a credit equals the negative of the value assigned to a debit on the same account. A debit and a credit are mirror images, and the framework proves the mirror exactly.

The proof is a short chain of definitions. A debit posting on account k is represented by an ordered pair of poles, a source and a sink, in a doubled account space. A credit reverses that order. The source covector evaluates a probe by subtracting the value at the sink from the value at the source, then scaling by a real parameter sourceScale. Reversing the pole order swaps the subtraction, which changes the sign. The theorem is a direct consequence of these definitions, and the library records it as a proved theorem with no axioms beyond the kernel's standard three.

The theorem also connects to the boundary record, a scalar that tracks flow across a boundary. The library proves that the covector evaluated on a unit potential drop probe equals the boundary record times the scale, and that the boundary record is +1 for a debit and -1 for a credit. The orientation equivariance theorem is the covector-level statement of that same sign flip, before any scalar projection is taken.

In Recognition Science, this theorem is one half of a bridge. The other half, the normalization of the source scale, remains open: the library proves that a proposed normalization is equivalent to a remaining physical equality, and that this equality is not forced by current premises. The orientation symmetry is settled; the scale is not.

/-- Source evaluation transforms under orientation reversal by the boundary
record sign (pole-swap antisymmetry). Occurrence-level compatibility only;
not normalization. -/
theorem bridgedOccurrenceSourceCovector_orientation_equivariant {d : Nat}
    (sourceScale : ℝ) (k : Fin d) (v : Fin (2 * d) → ℝ) :
    bridgedOccurrenceSourceCovector sourceScale k Side.credit v =
      - bridgedOccurrenceSourceCovector sourceScale k Side.debit v := by
  simp [bridgedOccurrenceSourceCovector, orientedPolesOfOwner,
    pairKernelPhysicalSourceCovector_apply]
  ring

/-- Forward convention: debit side posts source at the account's debit pole
and sink at its credit pole. Credit side is the reversed orientation
(swapped poles). Zero free choices. -/
def orientedPolesOfOwner {d : Nat} (k : Fin d) (side : Side) :
    OrientedPostingBoundaryRecord (2 * d) :=
  match side with
  | Side.debit =>
      ⟨debitPole k, creditPole k, debitPole_ne_creditPole k⟩
  | Side.credit =>
      ⟨creditPole k, debitPole k, Ne.symm (debitPole_ne_creditPole k)⟩

theorem occurrenceBoundaryRecord_debit {d : Nat} (k : Fin d) :
    occurrenceBoundaryRecord k Side.debit = 1 :=
  occurrenceBoundaryRecord_eq_orientationSign k Side.debit

theorem occurrenceBoundaryRecord_credit {d : Nat} (k : Fin d) :
    occurrenceBoundaryRecord k Side.credit = -1 :=
  occurrenceBoundaryRecord_eq_orientationSign k Side.credit

What this page does not claim

The theorem does not determine the numerical value of the source scale. The theorem does not assert that a debit and a credit are physically identical, only that their source covectors are negatives. The theorem does not prove that the normalization half of the bridge is forced; that remains open.

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/PairKernelOwnerChannelOccurrenceBridge.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: