Foundation Pair Kernel Owner Channel Occurrence Bridge Occurrence Bridged Source

Two readings, one remaining question

The declaration occurrenceBridgedSourceNormalization_iff_remainingPhysicalEquality is a theorem in the framework's machine-checked library of formal theorems. It states that two conditions are equivalent: the occurrence-bridged-source normalization, a proposed rule that would fix the scale of every bridged occurrence, and the remaining physical equality, a separate condition already known to hold without being forced by current premises. In plain terms, the theorem says that if you assume one of these conditions, you get the other for free, and vice versa.

What makes this useful is that the two conditions live on different sides of the framework. The normalization is a definitional choice, a way of pricing each bridged occurrence by matching its source covector against a unit potential drop. The remaining physical equality is a target, a relation that the framework's current axioms do not yet force. The equivalence does not prove the normalization; it proves that the normalization and the equality stand or fall together. If one is ever established, the other follows.

The theorem also carries a sharp negative result. The framework proves that the normalization is not forced by the current premises: there exists a candidate scale that satisfies every current premise yet fails the normalization. That candidate is rejected by the remaining physical equality, which is already proved to hold unforced. So the equivalence does not close the gap; it names the gap precisely. The normalization remains an open target, awaiting one new physical parent, a law to be adjudicated, not a theorem available from today's package.

What the declaration does not claim is just as important. It does not claim that the normalization is true, only that it is equivalent to the remaining physical equality. It does not claim that the remaining physical equality is forced by current premises; the pack explicitly says it is proved unforced. And it does not claim that the framework has derived the fine-structure constant or any other physical constant from this bridge. The bridge is a structural result about how occurrences and sources relate, not a derivation of any measured value.

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]

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

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

What this page does not claim

The normalization is not proved true, only equivalent to the remaining physical equality. The remaining physical equality is not forced by current premises. The framework does not derive the fine-structure constant from this bridge.

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: