Foundation Pair Kernel Gap2a Noether Symplectic Cotangent Residual Noether Packa

The Noether dead end

In the Recognition Science framework, a ledger (a discrete record of recognition events) must assign a cost to each event. The framework's library, a machine-checked collection of formal theorems, has already proved that this cost function must be J(x) = (x + 1/x)/2 - 1. But the framework also needs to know the scale of the elementary source: the fundamental unit of charge or magnitude that feeds into that cost. Two candidate scales, called A and B, both satisfy the basic premises. The question is whether deeper physical principles can select one.

The theorem named noetherPackage_admits_A_but_dualDecoy_rejects_A answers that question with a precise negative result. It shows, first, that adding a full package of Noether-style conservation laws and symplectic geometry to the basic premises still admits both candidates: the package cannot distinguish A from B. This is not a failure of the proof; it is a proved fact about the mathematics. The theorem then shows that a separate, independently named law, the native-action dual product law, rejects candidate A while leaving B standing. The dual law is used here only as a discriminator, a test to tell the candidates apart, not as a derived consequence of the Noether package.

The result is a theorem in the strict sense: it is proved in the framework's machine-checked library with no gaps and no extra axioms. Its content is that the Noether/symplectic route alone cannot break the scale degeneracy. Any law forced uniformly by that package must be scale-blind, meaning it cannot prefer one magnitude over another. The dual law, by contrast, is not forced by the package; it is an additional assumption that happens to eliminate A. The theorem does not say that A is physically wrong in any absolute sense, only that the dual law rejects it.

What the theorem does not claim is equally important. It does not prove that the dual law is true, only that it discriminates. It does not identify the conserved charge of an elementary posting orbit with the source covector, a missing momentum-map theorem that the library explicitly flags as open. And it does not say that B is the correct scale, only that B survives this particular test. The framework's own documentation calls the dual law a decoy: a named discriminator, not a derived premise. The theorem is a boundary marker, showing exactly where the Noether route stops and where a different kind of argument would be needed.

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

/-- Physical discrimination against the wrong banked unit: under the named
dual decoy (used only as a discriminator, never as a derived premise),
Candidate A is rejected while Candidate B survives. -/
theorem noetherPackage_admits_A_but_dualDecoy_rejects_A :
    CurrentPremisesWithNoetherSymplectic
        candidateA_sourceMagnitudeExpr.eval ∧
      ¬ NativeActionDualSourceLaw
        candidateA_sourceMagnitudeExpr.eval :=
  ⟨candidateA_satisfies_currentPremisesWithNoetherSymplectic,
    nativeActionDualSourceLaw_rejects_candidateA⟩

/-- 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 theorem does not prove that candidate B is the correct physical scale. The theorem does not prove the native-action dual product law is true, only that it discriminates between the two candidates. The theorem does not identify the conserved charge of an elementary posting orbit with the Gauss source covector.

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: