Foundation Pair Kernel Gap2a Noether Symplectic Cotangent Residual Current Premi

The scale remains free

In physics, a conservation law often seems like a powerful selector: if a quantity is conserved along every motion, it feels like nature is telling you something fundamental. The Recognition Science framework formalizes this intuition in a machine-checked library of formal theorems, and then tests how far it goes. The theorem recognition (a discrete record of events) cost functional and its conserved charges are built from symmetry principles, the question is whether those principles alone can select a unique numerical scale for the source, the underlying magnitude that drives the recognition process.

The answer, proved in the framework's library, is no. The theorem currentPremisesWithNoetherSymplectic_do_not_select_unique_scale establishes that the current premises, enriched with the full Noether and symplectic structure, still admit two distinct positive source scales. Both candidates satisfy every condition in the package, and they are provably different. Noether's theorem, which in its classical form says every symmetry implies a conserved charge, and the symplectic identification of the cost with a calibrated trace cost, do not break the scale symmetry. The conservation of a scale-blind charge, such as the constant cost functional, does not freeze the source coordinate. The framework proves that any law forced uniformly by this package alone cannot be scale-breaking.

What the theorem does not claim is just as important. It does not say that no selection is possible, only that this particular route, the Noether and symplectic certificate package, does not achieve it. It does not claim that the native-action dual product law, a separate constraint, is derivable from Noether. In fact, the framework shows that candidate A, one of the two banked scales, satisfies the Noether package but fails the dual law, so the dual law is not a corollary. The theorem also does not assert that the conserved charge of an elementary posting unit orbit equals the Gauss source covector; that identification remains an open target, explicitly marked as missing in the library.

The practical consequence is a sharpened map of the theory. Symmetry and conservation arguments are necessary ingredients, but they are not sufficient to pin down the source scale. The framework's honesty about this gap is what makes the larger derivation credible: the scale selection, when it comes, must come from a different, more specific physical principle, not from a generic appeal to Noether.

/-- 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 claim that no selection of the source scale is possible, only that the Noether and symplectic package does not achieve it. The theorem does not claim that the native-action dual product law is derivable from Noether; in fact, it shows the opposite. The theorem does not claim that the conserved charge of an elementary posting unit equals the Gauss source covector; that identification remains an open 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: