Foundation Pair Kernel Gap2a Noether Symplectic Cotangent Residual

The Noether gap

Noether's theorem is one of the most successful links between symmetry and physics: it says that for every continuous symmetry of a system, there is a conserved quantity, a charge that does not change as the system evolves. In classical mechanics, time translation symmetry gives energy, and space translation symmetry gives momentum. The module named foundation pair kernel gap2a noether symplectic cotangent residual tests whether this same logic, applied to the Recognition Science framework's own structures, can determine a specific numerical value for a fundamental source scale, the magnitude of a basic charge in the ledger, a discrete record of recognition events.

The framework's library, a machine-checked collection of formal theorems, already contains the ingredients one might expect to do this job. It has a theorem that area preservation, the condition that a flow does not change the size of a region, is equivalent to a certain symplectic condition, a geometric structure used in Hamiltonian mechanics. It identifies the recognition cost functional, the forced cost of registering a recognition event, with a trace cost in the special linear group SL(2). It also has a general Noether core, the abstract statement that symmetry implies a conserved charge, specialized to space and time translation flows. The module assembles these existing results into a single certificate, a package of statements that are all proved and scale-free, meaning they do not depend on the numerical value of the source scale.

The central finding is that this package, despite its power, is not enough. The library proves that both of the two banked candidate source magnitudes, the two possible values for the fundamental charge that the framework has identified elsewhere, satisfy all the premises of the enriched package. This is a theorem: currentPremisesWithNoetherSymplectic_admit_distinct_candidates establishes that there exist two distinct real numbers, both positive and both free of factors of pi, that each satisfy the current recognition source premises together with the Noether and symplectic certificate. Consequently, the package does not select a unique scale. The theorem currentPremisesWithNoetherSymplectic_do_not_select_unique_scale proves that there is no unique source scale satisfying the enriched premises.

Why does this matter? It means that a law forced uniformly by the Noether and symplectic package cannot be scale-breaking, cannot pick out one magnitude over another. The library proves this directly: noetherForcedLaw_cannot_be_scaleBreaking states that any law which holds for all source scales satisfying the enriched premises cannot be a law that uniquely selects a scale. In addition, the module shows that the native-action dual product law, a separate constraint that the framework uses elsewhere, is not a corollary of the Noether package. The theorem noetherSymplectic_does_not_force_nativeActionDualSourceLaw proves this by exhibiting candidate A, which satisfies the Noether package but fails the dual law. The dual law is used only as a discriminator, a decoy to reject the wrong candidate, not as a derived premise.

The module ends by naming the exact missing piece: a momentum-map theorem, a result that would identify the conserved charge of an elementary posting unit orbit with the Gauss source covector, the geometric object representing the source in the cotangent space, normalized by the physical action unit. This missing identification is stated as an open target, a structure named MissingMomentumMapSourceIdentification that records the insufficiency of the Noether package alone. The practical consequence is clear: symmetry and area preservation, however elegant, cannot by themselves force the numerical value of the fundamental source scale. The framework must look elsewhere, to a different kind of constraint, to close this gap.

/-- The defined Noether/symplectic enrichment still admits both banked
positive pi-free source models. -/
theorem currentPremisesWithNoetherSymplectic_admit_distinct_candidates :
    ∃ sourceScale₁ sourceScale₂ : ℝ,
      sourceScale₁ ≠ sourceScale₂ ∧
        CurrentPremisesWithNoetherSymplectic sourceScale₁ ∧
        CurrentPremisesWithNoetherSymplectic sourceScale₂ :=
  ⟨candidateA_sourceMagnitudeExpr.eval,
    candidateB_sourceMagnitudeExpr.eval,
    candidates_select_distinct_magnitudes,
    candidateA_satisfies_currentPremisesWithNoetherSymplectic,
    candidateB_satisfies_currentPremisesWithNoetherSymplectic⟩

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

/-- Any law forced uniformly by the defined Noether/symplectic package cannot
be scale-breaking: both banked candidates satisfy that package. -/
theorem noetherForcedLaw_cannot_be_scaleBreaking
    (law : ℝ → Prop)
    (hforced :
      ∀ sourceScale : ℝ,
        CurrentPremisesWithNoetherSymplectic sourceScale →
          law sourceScale) :
    ¬ NoetherForcedSourceLaw law := by
  intro hbreaking
  rcases hbreaking with ⟨selected, ⟨_hselPrem, _hselLaw⟩, honly⟩
  have hA := hforced _
    candidateA_satisfies_currentPremisesWithNoetherSymplectic
  have hB := hforced _
    candidateB_satisfies_currentPremisesWithNoetherSymplectic
  have hAselected :
      candidateA_sourceMagnitudeExpr.eval = selected :=
    honly _
      ⟨candidateA_satisfies_currentPremisesWithNoetherSymplectic, hA⟩
  have hBselected :
      candidateB_sourceMagnitudeExpr.eval = selected :=
    honly _
      ⟨candidateB_satisfies_currentPremisesWithNoetherSymplectic, hB⟩
  exact
    candidates_select_distinct_magnitudes
      (hAselected.trans hBselected.symm)

/-- The Noether/symplectic package does not force the native-action dual
product law.  Candidate A inhabits the package while failing the dual. -/
theorem noetherSymplectic_does_not_force_nativeActionDualSourceLaw :
    ¬ (∀ sourceScale : ℝ,
      CurrentPremisesWithNoetherSymplectic sourceScale →
        NativeActionDualSourceLaw sourceScale) := by
  intro hforce
  exact nativeActionDualSourceLaw_rejects_candidateA
    (hforce _
      candidateA_satisfies_currentPremisesWithNoetherSymplectic)

What this page does not claim

The module does not prove that no momentum-map theorem can exist, only that the Noether and symplectic package alone does not provide one. The module does not establish which of the two candidate source magnitudes is physically correct. The module does not use or derive the value of the gravitational constant G or any Planck-scale target.

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