Foundation Pair Kernel Gap2a Remaining Physical Equality Residual Remaining Phys

The unforced equality

In Recognition Science, recognition (a discrete record of events) and cost (the forced price of that record) lead to a chain of theorems. Part of that chain tries to identify a physical source by a unique coordinate. The declaration remainingPhysicalEquality_does_not_force_nativeActionDual_from_package states a precise negative result: the current premises, even after a common-type bridge is available, do not force the equality RemainingPhysicalEquality to imply the NativeActionDualSourceLaw.

To understand what this means, consider two candidate source scales, A and B, that both satisfy the post-bridge premises. The theorem shows that RemainingPhysicalEquality holds for candidate B but not for candidate A. Since both candidates satisfy the premises, the premises cannot force the equality to pick a unique scale. The declaration proves this by exhibiting candidate A as a counterexample: if the premises forced the equality, then candidate A would have to satisfy it, but it does not.

This result is not a failure of the framework. It is a precise map of what remains open. The framework's library proves that RemainingPhysicalEquality, IdentifiesPhysicalSourceWithUniqueCotangent, and NativeActionDualSourceLaw are all equivalent to each other. So the gap is not about which statement is true, but about whether the current premises alone can force any of them. The declaration shows they cannot. It also proves that any law forced uniformly by the post-bridge package cannot be scale-breaking, meaning it cannot depend on the specific value of the source scale.

The smallest missing physical primitive is exactly this equality. The framework names it as the atom that must be added to close the gap. The declaration does not claim that the equality is false, nor that it is unprovable. It only claims that the current premises do not force it. This is a theorem, checked by the machine, with no unproved assumptions. It banks the residual as an open problem, not a dead end.

theorem remainingPhysicalEquality_does_not_force_nativeActionDual_from_package :
    ¬ (∀ sourceScale : ℝ,
      CurrentPremisesAfterCommonTypeBridge sourceScale →
        NativeActionDualSourceLaw sourceScale) := by
  intro hforce
  exact nativeActionDualSourceLaw_rejects_candidateA
    (hforce _ candidateA_satisfies_currentPremisesAfterCommonTypeBridge)

theorem remainingPhysicalEquality_selects_candidateB :
    RemainingPhysicalEquality candidateB_sourceMagnitudeExpr.eval :=
  identifiesPhysicalSource_selects_candidateB

theorem remainingPhysicalEquality_rejects_candidateA :
    ¬ RemainingPhysicalEquality candidateA_sourceMagnitudeExpr.eval :=
  identifiesPhysicalSource_rejects_candidateA

theorem candidateA_satisfies_currentPremisesAfterCommonTypeBridge :
    CurrentPremisesAfterCommonTypeBridge
      candidateA_sourceMagnitudeExpr.eval :=
  candidateA_satisfies_currentPremisesWithUniqueRealCotangent

theorem candidateB_satisfies_currentPremisesAfterCommonTypeBridge :
    CurrentPremisesAfterCommonTypeBridge
      candidateB_sourceMagnitudeExpr.eval :=
  candidateB_satisfies_currentPremisesWithUniqueRealCotangent

theorem remainingPhysicalEquality_iff_nativeActionDual
    (sourceScale : ℝ) :
    RemainingPhysicalEquality sourceScale ↔
      NativeActionDualSourceLaw sourceScale :=
  identifiesPhysicalSource_iff_nativeActionDual sourceScale

theorem remainingPhysicalEquality_iff_identifies :
    ∀ sourceScale : ℝ,
      RemainingPhysicalEquality sourceScale ↔
        IdentifiesPhysicalSourceWithUniqueCotangent sourceScale := by
  intro sourceScale
  rfl

/-- Any law forced uniformly by the post-bridge package cannot select a unique
scale among the banked candidates. -/
theorem afterBridgeForcedLaw_cannot_be_scaleBreaking
    (law : ℝ → Prop)
    (hforced :
      ∀ sourceScale : ℝ,
        CurrentPremisesAfterCommonTypeBridge sourceScale →
          law sourceScale) :
    ¬ IsScaleBreakingAttachmentLaw law := by
  intro hbreaking
  rcases hbreaking with ⟨selected, ⟨_hselPrem, _hselLaw⟩, honly⟩
  have hA := hforced _
    candidateA_satisfies_currentPremisesAfterCommonTypeBridge
  have hB := hforced _
    candidateB_satisfies_currentPremisesAfterCommonTypeBridge
  have hAselected :
      candidateA_sourceMagnitudeExpr.eval = selected :=
    honly _
      ⟨candidateA_satisfies_currentRecognitionSourcePremises, hA⟩
  have hBselected :
      candidateB_sourceMagnitudeExpr.eval = selected :=
    honly _
      ⟨candidateB_satisfies_currentRecognitionSourcePremises, hB⟩
  exact
    candidates_select_distinct_magnitudes
      (hAselected.trans hBselected.symm)

What this page does not claim

The declaration does not claim that RemainingPhysicalEquality is false or unprovable, only that the current premises do not force it. It does not claim that the framework is incomplete in a way that invalidates its other theorems. It does not claim that the equality is the only missing primitive in the framework.

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