Foundation Pair Kernel Physical Source Scale No Go Candidate B Satisfies Current

The admitted candidate

The declaration candidateB_satisfies_currentRecognitionSourcePremises is a machine-checked proof that a specific positive real number, called candidate B, meets every premise the framework currently imposes on a physical source scale. Those premises are: the scale is positive, it contains no factor of pi, it satisfies the named action, posting, and stationarity conditions, and it is admitted by the symmetric pair-kernel package. The theorem does not say candidate B is the correct scale, only that nothing in the present package rules it out.

The proof itself is short. It first invokes a general theorem that every positive pi-free scale satisfies the current package, then verifies that candidate B is positive and pi-free. Candidate B is defined as the reciprocal of a quantity called the native action quantum, and its positivity follows from that quantity being positive. The pi-freeness is a separate proved fact. No continuum coefficient, integration target, or new axiom enters the argument.

The important consequence is negative. A companion theorem shows that candidate A, a different positive pi-free scale, also satisfies the same premises. Since the two candidates have distinct magnitudes, the package cannot attach a unique physical source. A further theorem states formally that no law implied by the current premises can select exactly one scale. Any successful attachment law must add new scale-breaking content that rejects at least one of the two admitted candidates.

In Recognition Science, this result is a no-go statement about the present state of the framework, not a failure of it. The framework models the physical source scale as an open parameter at this layer; the theorems map the boundary of what the current premises can and cannot decide. The practical upshot is that the framework's library has proved a precise gap: the source scale is underdetermined, and closing the gap requires a new physical premise, not a mathematical consequence of the existing ones.

/-- The reciprocal native-action candidate is also admitted by the same
primitive package. -/
theorem candidateB_satisfies_currentRecognitionSourcePremises :
    CurrentRecognitionSourcePremises
      candidateB_sourceMagnitudeExpr.eval := by
  apply currentRecognitionSourcePremises_of_positive_piFree
  · change 0 < nativeActionQuantumInv
    exact nativeActionQuantumInv_pos
  · exact candidateB_sourceMagnitude_piFree

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

/-- The one-act candidate is admitted by the current primitive package. -/
theorem candidateA_satisfies_currentRecognitionSourcePremises :
    CurrentRecognitionSourcePremises
      candidateA_sourceMagnitudeExpr.eval := by
  apply currentRecognitionSourcePremises_of_positive_piFree
  · rw [candidateA_sourceMagnitude_eq_one]
    norm_num
  · exact candidateA_sourceMagnitude_piFree

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

Candidate B is the unique or correct physical source scale. The current premises are sufficient to determine any source scale. The theorem assigns a numerical value to candidate B or compares it with measured physics.

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: