Foundation Pair Kernel Gap2a Noether Symplectic Cotangent Residual Noether Sympl

A limit on symmetry arguments

In physics, symmetry arguments are powerful: if a system looks the same under a transformation, something is conserved. Noether's theorem, proved by Emmy Noether in 1918, makes this precise: continuous symmetries yield conserved quantities. The Recognition Science framework builds on this idea, using a ledger, a discrete record of recognition events, to model physical structure. The question at issue is whether such symmetry reasoning can also fix the numerical value of a fundamental source scale, the magnitude attached to an elementary posting in the ledger.

The framework's machine-checked library of formal theorems contains a declaration, noetherSymplectic_does_not_force_nativeActionDualSourceLaw, which answers this question in the negative. In plain language, it establishes that the existing Noether and symplectic structure, a package of results about conserved charges and area preservation, does not force the native-action dual source law. That law would be a specific relation between the source magnitude and the action unit. The theorem shows that this law is not a corollary of the symmetry principles alone.

The proof works by exhibiting a concrete counterexample. The framework considers two candidate values for the source scale, called Candidate A and Candidate B. Both satisfy the enriched premises, which combine the current recognition source premises with the Noether/symplectic certificate. The theorem shows that Candidate A satisfies all these premises yet fails the native-action dual source law. Therefore, if the law were forced by the premises, Candidate A would have to satisfy it, which it does not. This is a direct contradiction, so the law cannot be forced.

What the theorem does not claim is equally important. It does not say the native-action dual source law is false; it only says the Noether/symplectic package does not prove it. The framework explicitly lists this as a missing piece: a momentum-map theorem that would identify the conserved charge of an elementary posting orbit with the source covector. That identification remains open. The theorem also does not reject Candidate B, which survives the dual law as a discriminator. The result is a precise boundary marker, showing exactly where symmetry arguments stop and further structure is needed.

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

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

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)

What this page does not claim

The native-action dual source law is false or unphysical. Candidate B is the correct source scale. The Noether and symplectic package is inconsistent or incomplete in itself.

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: