Encyclopedia Foundation Foundation Pair Kernel Physical Source Scale No Go

ARTICLE 5 claims 5 theorems

Foundation Pair Kernel Physical Source Scale No Go

The framework's own axioms admit two different physical source scales, so no amount of cleverness within them can pick a single one.

Verify this page

The source-scale obstruction

The recognition framework, which models reality as a discrete ledger of events, needs a physical source scale: a number that sets the size of the fundamental unit of action. The current package of primitive assumptions, which include positivity, a pi-free scale, elementary posting, symmetric pair action, and stationarity, turns out to be too weak. It admits every positive pi-free real number as a valid source scale.

Two specific candidates illustrate the problem. The first has magnitude 1, and the second is the reciprocal of the native action quantum. Both are positive, pi-free, and satisfy every current premise. They are distinct magnitudes, so the package does not attach a unique physical source. This is not a bug in the code; it is a proved theorem in the framework's machine-checked library of formal theorems. The theorem currentRecognitionSourcePremises_do_not_select_unique_scale states that no unique scale exists under the current premises.

In Recognition Science, this obstruction has a name: the source-side scale torsor. A torsor is a set where any two points can be compared but no point is naturally privileged. The two candidates are the banked points, and the current premises cannot tell them apart.

The module then defines what a genuine attachment law would be: an additional source-side law that, together with the current premises, selects exactly one magnitude. The key result is that any such law must reject at least one of the two currently admitted candidates. It cannot be a consequence of the current premises alone. The theorem scaleBreakingAttachmentLaw_rejects_current_candidate proves this disjunction, and currentPremisesCannotForceScaleBreakingAttachment shows that no law implied by the current package can break the tie.

The consequence is plain: if the framework is to name a single physical source scale, it must add a new physical premise, one that is not derivable from action, posting, positivity, pi-freeness, or stationarity. The module does not say what that premise is. It only draws the boundary line, and that boundary is itself a theorem.

THEOREM currentRecognitionSourcePremises_of_positive_piFree · IndisputableMonolith/Foundation/PairKernelPhysicalSourceScaleNoGo.lean
currentRecognitionSourcePremises_of_positive_piFree · IndisputableMonolith/Foundation/PairKernelPhysicalSourceScaleNoGo.lean:39 
/-- Every positive pi-free scale satisfies the current action, posting, and
stationarity package. -/
theorem currentRecognitionSourcePremises_of_positive_piFree
    (sourceScale : ℝ)
    (hpos : 0 < sourceScale)
    (hpiFree : PiFree sourceScale) :
    CurrentRecognitionSourcePremises sourceScale :=
  ⟨hpos, hpiFree, namedPremises_all_couplings sourceScale⟩
THEOREM currentRecognitionSourcePremises_admit_distinct_candidates · IndisputableMonolith/Foundation/PairKernelPhysicalSourceScaleNoGo.lean
currentRecognitionSourcePremises_admit_distinct_candidates · IndisputableMonolith/Foundation/PairKernelPhysicalSourceScaleNoGo.lean:67 
/-- The present primitive package has two distinct positive pi-free source
models. This is the source-side scale torsor stated on the banked candidates. -/
theorem currentRecognitionSourcePremises_admit_distinct_candidates :
    ∃ sourceScale₁ sourceScale₂ : ℝ,
      sourceScale₁ ≠ sourceScale₂ ∧
        CurrentRecognitionSourcePremises sourceScale₁ ∧
        CurrentRecognitionSourcePremises sourceScale₂ :=
  ⟨candidateA_sourceMagnitudeExpr.eval,
    candidateB_sourceMagnitudeExpr.eval,
    candidates_select_distinct_magnitudes,
    candidateA_satisfies_currentRecognitionSourcePremises,
    candidateB_satisfies_currentRecognitionSourcePremises⟩
THEOREM currentRecognitionSourcePremises_do_not_select_unique_scale · IndisputableMonolith/Foundation/PairKernelPhysicalSourceScaleNoGo.lean
currentRecognitionSourcePremises_do_not_select_unique_scale · IndisputableMonolith/Foundation/PairKernelPhysicalSourceScaleNoGo.lean:80 
/-- Action, posting, positivity, pi-freeness, and stationarity do not attach a
unique source magnitude. -/
theorem currentRecognitionSourcePremises_do_not_select_unique_scale :
    ¬ ∃! sourceScale : ℝ,
      CurrentRecognitionSourcePremises sourceScale := by
  intro hunique
  rcases hunique with ⟨selected, _hselected, honly⟩
  have hA :
      candidateA_sourceMagnitudeExpr.eval = selected :=
    honly _ candidateA_satisfies_currentRecognitionSourcePremises
  have hB :
      candidateB_sourceMagnitudeExpr.eval = selected :=
    honly _ candidateB_satisfies_currentRecognitionSourcePremises
  exact candidates_select_distinct_magnitudes (hA.trans hB.symm)
THEOREM scaleBreakingAttachmentLaw_rejects_current_candidate · IndisputableMonolith/Foundation/PairKernelPhysicalSourceScaleNoGo.lean
scaleBreakingAttachmentLaw_rejects_current_candidate · IndisputableMonolith/Foundation/PairKernelPhysicalSourceScaleNoGo.lean:102 
/-- Every genuine attachment law must reject at least one of the two source
scales currently admitted by action, posting, and stationarity. -/
theorem scaleBreakingAttachmentLaw_rejects_current_candidate
    (law : ℝ → Prop)
    (hbreaking : IsScaleBreakingAttachmentLaw law) :
    ¬ law candidateA_sourceMagnitudeExpr.eval ∨
      ¬ law candidateB_sourceMagnitudeExpr.eval := by
  by_cases hA : law candidateA_sourceMagnitudeExpr.eval
  · right
    intro hB
    rcases hbreaking with ⟨selected, _hselected, honly⟩
    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)
  · exact Or.inl hA
THEOREM currentPremisesCannotForceScaleBreakingAttachment · IndisputableMonolith/Foundation/PairKernelPhysicalSourceScaleNoGo.lean
currentPremisesCannotForceScaleBreakingAttachment · IndisputableMonolith/Foundation/PairKernelPhysicalSourceScaleNoGo.lean:126 
/-- No law implied by the current primitive package can be a scale-breaking
attachment. The remaining residual must add a new physical premise. -/
theorem currentPremisesCannotForceScaleBreakingAttachment
    (law : ℝ → Prop)
    (hforced :
      ∀ sourceScale : ℝ,
        CurrentRecognitionSourcePremises sourceScale →
          law sourceScale) :
    ¬ IsScaleBreakingAttachmentLaw law := by
  intro hbreaking
  rcases
      scaleBreakingAttachmentLaw_rejects_current_candidate
        law hbreaking with hA | hB
  · exact hA
      (hforced _
        candidateA_satisfies_currentRecognitionSourcePremises)
  · exact hB
      (hforced _
        candidateB_satisfies_currentRecognitionSourcePremises)

What this page does not claim

This module does not identify which of the two candidates is the correct physical source scale. This module does not propose a specific scale-breaking attachment law.

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