Foundation Pair Kernel Gap2a Real Cotangent Normalization Residual Candidate A S

What candidate A proves

In the Recognition Science framework, the physical world is described by a discrete record of events called a ledger, and the framework's library, a machine-checked collection of formal theorems, tests which mathematical structures can consistently describe it. The declaration candidateA_satisfies_currentPremisesWithUniqueRealCotangent is a theorem proving that one specific candidate value for a fundamental physical scale, called candidate A, satisfies all the currently accepted structural premises. These premises include the existence of a unique real-linear functional that extends the ledger's primitive character along a canonical embedding into the real numbers, a mathematical object whose coordinate is the reciprocal of the framework's native action quantum.

The theorem is a proof of consistency, not a proof of uniqueness. The library also proves that candidate B, a different positive real number, satisfies the exact same premises. Because both candidates pass every current test, the premises do not select a single scale; the framework's own theorem currentPremisesWithUniqueRealCotangent_do_not_select_unique_scale states this explicitly. The identification of the physical source scale with the unique cotangent coordinate, which would select candidate B, is a separate law that the current premises do not force. The theorem exactJConjugate_ne_uniqueCotangentCoordinate further shows that the variational conjugate from the exact cost function J is a different real number, so that path also does not resolve the choice.

What the declaration does not claim is that candidate A is the correct physical scale. It only claims that candidate A is admissible under the current premises. The missing piece is an independently physical law, named UniqueCotangentNormalizationByActionUnit, that would identify the unique cotangent with the pair-kernel source without inserting the identification as a definition. Until such a law is found, the selection between candidate A and candidate B remains an open problem, not a solved one.

theorem candidateA_satisfies_currentPremisesWithUniqueRealCotangent :
    CurrentPremisesWithUniqueRealCotangent
      candidateA_sourceMagnitudeExpr.eval := by
  apply currentPremisesWithUniqueRealCotangent_of_positive_piFree
  · rw [candidateA_sourceMagnitude_eq_one]
    norm_num
  · exact candidateA_sourceMagnitude_piFree

theorem candidateB_satisfies_currentPremisesWithUniqueRealCotangent :
    CurrentPremisesWithUniqueRealCotangent
      candidateB_sourceMagnitudeExpr.eval := by
  apply currentPremisesWithUniqueRealCotangent_of_positive_piFree
  · change 0 < nativeActionQuantumInv
    exact nativeActionQuantumInv_pos
  · exact candidateB_sourceMagnitude_piFree

theorem currentPremisesWithUniqueRealCotangent_do_not_select_unique_scale :
    ¬ ∃! sourceScale : ℝ,
      CurrentPremisesWithUniqueRealCotangent sourceScale := by
  intro hunique
  rcases hunique with ⟨selected, _hselected, honly⟩
  have hA :
      candidateA_sourceMagnitudeExpr.eval = selected :=
    honly _ candidateA_satisfies_currentPremisesWithUniqueRealCotangent
  have hB :
      candidateB_sourceMagnitudeExpr.eval = selected :=
    honly _ candidateB_satisfies_currentPremisesWithUniqueRealCotangent
  exact candidates_select_distinct_magnitudes (hA.trans hB.symm)

/-- The scalar-extension package does not force the physical identification. -/
theorem uniqueRealCotangent_does_not_force_identification :
    ¬ (∀ sourceScale : ℝ,
      CurrentPremisesWithUniqueRealCotangent sourceScale →
        IdentifiesPhysicalSourceWithUniqueCotangent sourceScale) := by
  intro hforce
  exact identifiesPhysicalSource_rejects_candidateA
    (hforce _
      candidateA_satisfies_currentPremisesWithUniqueRealCotangent)

/-- Exact-J variational conjugate is not the unique character-extension
cotangent coordinate, so first-variation of the exact one-edge action does not
supply the physical identification. -/
theorem exactJConjugate_ne_uniqueCotangentCoordinate :
    nativeExactJConjugateSource ≠ uniqueCotangentCoordinate := by
  rw [uniqueCotangentCoordinate_eq_nativeActionQuantumInv]
  exact nativeExactJConjugateSource_ne_nativeActionQuantumInv

What this page does not claim

Candidate A is the correct physical scale. The current premises force a unique scale. The framework has derived the fine-structure constant or any other specific coupling constant.

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