Foundation Pair Kernel Gap2a Noether Symplectic Cotangent Residual Candidate A S

What the certificate shows

The declaration candidateA_satisfies_currentPremisesWithNoetherSymplectic is a theorem in the framework's machine-checked library of formal theorems. It proves that Candidate A, one of two banked real source magnitudes, satisfies the current recognition source premises enriched with an independently existing Noether/symplectic certificate. The certificate packages area preservation, the symplectic identification of the cost functional with a calibrated SL(2) trace, and abstract Noether conservation specialized to time and space translation flows. The theorem shows Candidate A is a positive, pi-free source model that meets every conjunct of this enriched premise set.

The theorem's real content is negative. The machine-checked library also proves currentPremisesWithNoetherSymplectic_admit_distinct_candidates: both Candidate A and Candidate B satisfy the enriched premises, and they select distinct magnitudes. A companion theorem, currentPremisesWithNoetherSymplectic_do_not_select_unique_scale, shows no unique source scale exists under this package. Any law forced uniformly by the Noether/symplectic package cannot be scale-breaking, because both banked candidates satisfy it. The package does not identify the conserved charge of an elementary posting unit orbit with the Gauss source covector, and it does not force the native-action dual product law. Candidate A inhabits the package while failing that dual law, which is used only as a decoy discriminator, never as a derived premise.

What the theorem does not claim is as important as what it proves. It does not claim Candidate A is the physical source scale. It does not claim the Noether/symplectic package selects a unique scale, and it does not claim the package forces the dual product law. The exact missing parent after this route is a momentum-map identification equating the Noether charge of the elementary posting unit orbit with the real Gauss source cotangent covector, without assuming source times action equals unit and without Green aggregation. That identification remains open. The certificate is a terminal residual: it records that the Noether/symplectic cotangent route does not close the gap, not that it does.

theorem candidateA_satisfies_currentPremisesWithNoetherSymplectic :
    CurrentPremisesWithNoetherSymplectic
      candidateA_sourceMagnitudeExpr.eval := by
  apply currentPremisesWithNoetherSymplectic_of_positive_piFree
  · rw [candidateA_sourceMagnitude_eq_one]
    norm_num
  · exact candidateA_sourceMagnitude_piFree

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

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

What this page does not claim

Candidate A is the physical source scale. The Noether/symplectic package alone forces a unique source scale. The native-action dual product law follows from the Noether/symplectic package.

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: