Encyclopedia Foundation Foundation Pair Kernel Owner Channel Occurrence Bridge

ARTICLE 4 claims 4 theorems

Foundation Pair Kernel Owner Channel Occurrence Bridge

How a single ledger entry becomes a unique, oriented pair of poles, with the machinery that proves no two entries can collide.

Verify this page

The occurrence bridge

In the Recognition Science framework, a ledger is a discrete record of events, and each event is a tick: a debit or a credit on one account. The foundation pair kernel owner channel occurrence bridge is the part of the framework's machine-checked library of formal theorems that takes one such tick and turns it into a precise geometric object. The object is an oriented pair of poles, two distinct points on a doubled account index space, with an order that records which side is which. A debit on account k becomes the ordered pair (debit pole, credit pole); a credit becomes the reverse order. That reversal is the whole content of the orientation.

The bridge proves this reading is canonical, meaning it makes zero free choices. For every tick (k, side), there is exactly one oriented pair of poles, and distinct ticks give distinct pairs. The theorem orientedPolesOfOwner_injective states this injectivity directly. The framework also proves the orientation is compatible with the boundary record: a debit produces a forward boundary record of +1, a credit produces a reversed flow with -1. These signs are not imposed by hand; they fall out of the definitions. The module further shows that when a legal tick is posted to a ledger state, the profiles of the before and after states recover exactly the same oriented poles as the tick itself, with no ambiguity.

The bridge also attaches a physical source covector to each occurrence. This covector, when evaluated on a probe, returns the boundary record times a scale factor. The sign of this evaluation flips under orientation reversal, matching the boundary record's sign. This is the occurrence half of the bridge, and it is fully theorem-backed. The normalization half, which would fix the scale factor, remains open. The module proves that the normalization statement is equivalent to a separate equality, RemainingPhysicalEquality, which is already shown to be unforced by current premises. This means the scale factor is not derivable from what is known today; it requires a new physical parent, a LAW to be adjudicated, not a theorem.

One notable negative result is that the module never uses equality of unit heat with unit Gauss flux as a join. Occurrence identity is carried entirely by oriented poles and profile recovery. The theorem heat_flux_scalar_join_not_occurrence_identity shows that two different occurrences can share the same boundary record value, so the scalar alone cannot identify an occurrence. This is a deliberate design choice, and the audit note confirms no premise assumes the residual physical equality. The bridge therefore stands on its own combinatorial and orientational content, with the normalization question cleanly separated as a target for future work.

THEOREM orientedPolesOfOwner_injective · IndisputableMonolith/Foundation/PairKernelOwnerChannelOccurrenceBridge.lean
orientedPolesOfOwner_injective · IndisputableMonolith/Foundation/PairKernelOwnerChannelOccurrenceBridge.lean:135 
/-- (a) Injectivity: distinct owner addresses give distinct oriented poles. -/
theorem orientedPolesOfOwner_injective {d : Nat} :
    Function.Injective (fun p : Fin d × Side => orientedPolesOfOwner p.1 p.2) := by
  intro ⟨k₁, s₁⟩ ⟨k₂, s₂⟩ h
  apply Prod.ext
  · -- accounts equal
    cases s₁ with
    | debit =>
      cases s₂ with
      | debit =>
        have hs :=
          (orientedPostingBoundaryRecord_eq_iff_same_poles
            (orientedPolesOfOwner k₁ Side.debit)
            (orientedPolesOfOwner k₂ Side.debit)).1 h
        exact debitPole_injective hs.1
      | credit =>
        have hs :=
          (orientedPostingBoundaryRecord_eq_iff_same_poles
            (orientedPolesOfOwner k₁ Side.debit)
            (orientedPolesOfOwner k₂ Side.credit)).1 h
        exact False.elim (debitPole_ne_creditPole_of k₁ k₂ hs.1)
    | credit =>
      cases s₂ with
      | debit =>
        have hs :=
          (orientedPostingBoundaryRecord_eq_iff_same_poles
            (orientedPolesOfOwner k₁ Side.credit)
            (orientedPolesOfOwner k₂ Side.debit)).1 h
        exact False.elim (debitPole_ne_creditPole_of k₂ k₁ hs.1.symm)
      | credit =>
        have hs :=
          (orientedPostingBoundaryRecord_eq_iff_same_poles
            (orientedPolesOfOwner k₁ Side.credit)
            (orientedPolesOfOwner k₂ Side.credit)).1 h
        exact creditPole_injective hs.1
  · -- sides equal
    cases s₁ with
    | debit =>
      cases s₂ with
      | debit => rfl
      | credit =>
        have hs :=
          (orientedPostingBoundaryRecord_eq_iff_same_poles
            (orientedPolesOfOwner k₁ Side.debit)
            (orientedPolesOfOwner k₂ Side.credit)).1 h
        exact False.elim (debitPole_ne_creditPole_of k₁ k₂ hs.1)
    | credit =>
      cases s₂ with
      | debit =>
        have hs :=
          (orientedPostingBoundaryRecord_eq_iff_same_poles
            (orientedPolesOfOwner k₁ Side.credit)
            (orientedPolesOfOwner k₂ Side.debit)).1 h
        exact False.elim (debitPole_ne_creditPole_of k₂ k₁ hs.1.symm)
      | credit => rfl
THEOREM occurrenceBoundaryRecord_debit · occurrenceBoundaryRecord_credit · IndisputableMonolith/Foundation/PairKernelOwnerChannelOccurrenceBridge.lean
occurrenceBoundaryRecord_debit · IndisputableMonolith/Foundation/PairKernelOwnerChannelOccurrenceBridge.lean:218 
theorem occurrenceBoundaryRecord_debit {d : Nat} (k : Fin d) :
    occurrenceBoundaryRecord k Side.debit = 1 :=
  occurrenceBoundaryRecord_eq_orientationSign k Side.debit
occurrenceBoundaryRecord_credit · IndisputableMonolith/Foundation/PairKernelOwnerChannelOccurrenceBridge.lean:222 
theorem occurrenceBoundaryRecord_credit {d : Nat} (k : Fin d) :
    occurrenceBoundaryRecord k Side.credit = -1 :=
  occurrenceBoundaryRecord_eq_orientationSign k Side.credit
THEOREM occurrenceBridgedSourceNormalization_iff_remainingPhysicalEquality · occurrenceBridgedSourceNormalization_unforced · IndisputableMonolith/Foundation/PairKernelOwnerChannelOccurrenceBridge.lean
occurrenceBridgedSourceNormalization_iff_remainingPhysicalEquality · IndisputableMonolith/Foundation/PairKernelOwnerChannelOccurrenceBridge.lean:345 
theorem occurrenceBridgedSourceNormalization_iff_remainingPhysicalEquality
    (sourceScale : ℝ) :
    OccurrenceBridgedSourceNormalization sourceScale ↔
      RemainingPhysicalEquality sourceScale := by
  constructor
  · intro hnorm
    -- Specialize to a single debit occurrence on d = 1.
    haveI : NeZero (1 : Nat) := ⟨by decide⟩
    haveI : DecidableEq (Fin (2 * 1)) := inferInstance
    let k : Fin 1 := ⟨0, by decide⟩
    have h := hnorm (d := 1) k Side.debit
    have hdrop :=
      unitPotentialDropProbe_drop (debitPole k) (creditPole k)
        (debitPole_ne_creditPole k)
    have hrec : occurrenceBoundaryRecord k Side.debit = 1 :=
      occurrenceBoundaryRecord_debit k
    -- LHS = sourceScale
    have hlhs :
        bridgedOccurrenceSourceCovector sourceScale k Side.debit
            (unitPotentialDropProbe (debitPole k) (creditPole k)) =
          sourceScale := by
      simp [bridgedOccurrenceSourceCovector, orientedPolesOfOwner,
        pairKernelPhysicalSourceCovector_apply, hdrop]
    -- Reduce to sourceScale = uniqueCotangentCoordinate
    have : sourceScale = uniqueCotangentCoordinate := by
      calc
        sourceScale =
            bridgedOccurrenceSourceCovector sourceScale k Side.debit
              (unitPotentialDropProbe (debitPole k) (creditPole k)) := hlhs.symm
        _ = occurrenceBoundaryRecord k Side.debit * uniqueCotangentCoordinate := h
        _ = (1 : ℝ) * uniqueCotangentCoordinate := by rw [hrec]
        _ = uniqueCotangentCoordinate := one_mul _
    exact this
  · intro hrem d _ _ k side
    have hmatch :=
      bridgedOccurrenceSource_matches_boundarySign sourceScale k side
    -- RemainingPhysicalEquality is sourceScale = uniqueCotangentCoordinate
    change sourceScale = uniqueCotangentCoordinate at hrem
    calc
      bridgedOccurrenceSourceCovector sourceScale k side
          (unitPotentialDropProbe (debitPole k) (creditPole k)) =
          occurrenceBoundaryRecord k side * sourceScale := hmatch
      _ = occurrenceBoundaryRecord k side * uniqueCotangentCoordinate := by
            rw [hrem]
occurrenceBridgedSourceNormalization_unforced · IndisputableMonolith/Foundation/PairKernelOwnerChannelOccurrenceBridge.lean:407 
/-- The residual remains unforced after the occurrence bridge: current premises
still do not select the normalization. -/
theorem occurrenceBridgedSourceNormalization_unforced :
    ¬ (∀ sourceScale : ℝ,
      CurrentPremisesAfterCommonTypeBridge sourceScale →
        OccurrenceBridgedSourceNormalization sourceScale) := by
  intro hforce
  exact remainingPhysicalEquality_rejects_candidateA <|
    (occurrenceBridgedSourceNormalization_iff_remainingPhysicalEquality _).1 <|
      hforce _ candidateA_satisfies_currentPremisesAfterCommonTypeBridge
THEOREM heat_flux_scalar_join_not_occurrence_identity · IndisputableMonolith/Foundation/PairKernelOwnerChannelOccurrenceBridge.lean
heat_flux_scalar_join_not_occurrence_identity · IndisputableMonolith/Foundation/PairKernelOwnerChannelOccurrenceBridge.lean:445 
/-- (iii) Heat=flux scalar join is absent from the occurrence identity.
Equal unit boundary fluxes do not identify oriented poles (inherited
scalar-coincidence decoy); the bridge uses poles, not heat. -/
theorem heat_flux_scalar_join_not_occurrence_identity {d : Nat}
    (hd : 2 ≤ d) :
    ∃ k₁ k₂ : Fin d,
      occurrenceBoundaryRecord k₁ Side.debit =
          occurrenceBoundaryRecord k₂ Side.debit ∧
        orientedPolesOfOwner k₁ Side.debit ≠
          orientedPolesOfOwner k₂ Side.debit := by
  have hpos : 0 < d := lt_of_lt_of_le (by decide : (0 : Nat) < 2) hd
  have h1 : 1 < d := lt_of_lt_of_le (by decide : (1 : Nat) < 2) hd
  let k₁ : Fin d := ⟨0, hpos⟩
  let k₂ : Fin d := ⟨1, h1⟩
  refine ⟨k₁, k₂, ?_, ?_⟩
  · rw [occurrenceBoundaryRecord_debit, occurrenceBoundaryRecord_debit]
  · intro h
    have hs :=
      (orientedPostingBoundaryRecord_eq_iff_same_poles _ _).1 h
    have hk := debitPole_injective hs.1
    exact (by decide : (0 : Nat) ≠ 1) (congrArg Fin.val hk)

What this page does not claim

The module does not derive the scale factor for the source covector; that normalization remains open. The module does not use equality of unit heat with unit Gauss flux as a join for occurrence identity. The bridge does not establish any result about the fine-structure constant or other physical constants.

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:

MACHINE LAYER · GROUNDED CLAIM TABLE · CLICK TO EXPAND