Foundation Pair Kernel Physical Source Scale No Go Current Premises Cannot Force

The source-scale obstruction

The Recognition Science framework keeps a discrete record of recognition events, and from that record it derives constants and dimensions. One open problem is the physical source scale: the magnitude that anchors how these events map onto measured physics. The framework's library, a machine-checked collection of formal theorems, now contains a precise statement about this problem. The declaration currentPremisesCannotForceScaleBreakingAttachment proves that the current package of premises cannot force a unique source magnitude.

The theorem works by exhibiting two distinct candidates that both satisfy every current premise. One candidate has magnitude one; the other is the reciprocal of the native action quantum. Both are positive and free of the constant pi, and both satisfy the action, posting, and stationarity conditions. Because the two magnitudes differ, the premises admit at least two distinct scales. The theorem then shows that no law implied by those premises can select exactly one scale. Any law that does select a unique scale must reject at least one of the two admitted candidates, and that rejection cannot be a consequence of the current premises alone.

In plain terms, the framework's current rules are underdetermined on this point. They do not fail; they simply do not reach far enough. The result is a no-go theorem in the formal library, proved without any unproved assumptions. It does not say which candidate is correct, and it does not say what new premise is needed. It says only that a new physical premise is required, one that breaks the symmetry between the two admitted scales. This is a target for future work, not a dead end.

The declaration also does not claim that the framework is inconsistent, nor that the two candidates are physically meaningful. It treats them as formal objects that satisfy the current rules. The obstruction is structural: the rules as written cannot distinguish them. A reader should take away that the framework has identified a precise gap in its own foundations, and that filling that gap is a stated problem, not a hidden assumption.

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

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

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

What this page does not claim

The theorem does not claim that the two candidate scales are physically meaningful. The theorem does not claim that the framework is inconsistent or that the current premises are wrong. The theorem does not claim that any specific new premise will resolve the obstruction.

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: