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

The admitted candidate

The declaration candidateA_satisfies_currentRecognitionSourcePremises is a machine-checked theorem in the framework's library of formal theorems. It proves that a specific numerical candidate, called candidate A, meets every condition the framework currently imposes on a physical source scale. Those conditions, bundled into the predicate CurrentRecognitionSourcePremises, are that the scale is positive, contains no factor of pi, and satisfies the package of elementary posting, symmetric pair action, and stationarity at that scale.

The theorem's proof is short and direct. It first shows candidate A equals one, then verifies that one is positive and pi-free, and finally applies a general theorem stating that every positive pi-free scale satisfies the full premise package. The declaration itself does not compute the candidate's value from deeper principles; it takes the candidate's magnitude as given and confirms it is admissible under the current rules.

The significance lies in what the theorem does alongside its companion, candidateB_satisfies_currentRecognitionSourcePremises. Both candidates pass the same primitive package, yet they have distinct magnitudes. A separate theorem, currentRecognitionSourcePremises_admit_distinct_candidates, packages this fact: there exist two different real numbers, both satisfying all current premises. Consequently, the current premises do not select a unique physical source scale, a conclusion stated by the theorem currentRecognitionSourcePremises_do_not_select_unique_scale.

In Recognition Science, this is a deliberate no-go result. The framework's current action, posting, and stationarity conditions are too weak to pin down the source magnitude. Any future law that successfully attaches a unique scale must therefore add new scale-breaking content that rejects at least one of the two admitted candidates. The theorem scaleBreakingAttachmentLaw_rejects_current_candidate makes this explicit: a genuine attachment law cannot be a consequence of the current premises alone.

What the declaration does not claim is equally important. It does not assert that candidate A is the correct physical source scale, nor that it is preferred over candidate B. It does not derive the candidate's value from the framework's forcing chain; the value one is supplied as part of the candidate definition. The theorem only establishes admissibility under the current, incomplete premise set, leaving the question of which scale nature actually uses as an open target for future work.

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

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

/-- 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 A is the actual physical source scale. The framework derives the value one for candidate A from deeper principles. The current premises are complete enough to determine a unique source magnitude.

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: