Foundation Pair Kernel Gap2a Common Type Bridge Pulled Back Gauss Eq Noether Iff

The bridge and its limit

In mathematics, two objects that live in different spaces cannot be compared directly. The Recognition Science framework faced exactly this problem. One object, the Noether momentum map, is a linear map on a single scalar line. The other, the Gauss source covector, is a linear map on a space of field variations, which are functions from a finite set of points to real numbers. These are different types, so a direct equality is not even a well-formed question.

The framework's library of machine-checked theorems builds a bridge between the two. It constructs a specific linear map that pulls the Gauss source covector back to the scalar line. This is a definitional choice, a piece of scaffolding. The key theorem about this bridge, named pulledBackGauss_eq_noether_iff_sourceScale_eq_uniqueCotangent, then states a precise equivalence: the pulled-back Gauss source equals the Noether momentum map if and only if a certain real number, the source scale, equals a specific constant called the unique cotangent coordinate. This is a proved theorem, not a conjecture.

The theorem does not claim that this equality holds. It claims only that the equality is equivalent to a separate condition. The framework's library explicitly proves that this condition is not forced by the framework's own premises. The physical equality between the two objects remains an unforced premise, a typed residual that must be added from outside. The theorem isolates this residual cleanly, showing exactly what would have to be true for the two objects to coincide.

This is a lesson in intellectual honesty. The theorem does not manufacture a desired result. It does not choose the source scale to be the unique cotangent coordinate. It proves that if the two objects are equal, then the scale must be that value, and conversely. The framework also proves that a naive candidate, the unit source scale, is rejected: it does not make the two objects equal. The bridge is a tool for comparison, not a proof of identity.

What this means for a reader is that the framework can state exactly where its own derivation stops. The equality between the Noether momentum map and the Gauss source is not a theorem; it is a premise. The theorem's value is in making that premise precise and isolated. It tells you the single condition you would need to accept to make the identification, and it does not pretend that the framework forces that condition on its own.

theorem pulledBackGauss_eq_noether_iff_sourceScale_eq_uniqueCotangent
    {n : ℕ} [DecidableEq (Fin n)]
    (sourceScale : ℝ) (a b : Fin n) (hab : a ≠ b) :
    PulledBackGaussEqualsNoetherMomentumMap sourceScale a b ↔
      sourceScale = uniqueCotangentCoordinate := by
  have hpull := pulledBackGaussSource_eq_scale_smul_id sourceScale a b hab
  have hnoeth := noetherMomentumMapCovectorLinear_eq_uniqueCotangent_smul_id
  constructor
  · intro heq
    have hfun :
        sourceScale • (LinearMap.id : ℝ →ₗ[ℝ] ℝ) =
          uniqueCotangentCoordinate • (LinearMap.id : ℝ →ₗ[ℝ] ℝ) := by
      calc
        sourceScale • (LinearMap.id : ℝ →ₗ[ℝ] ℝ) =
            pulledBackGaussSource sourceScale a b := hpull.symm
        _ = noetherMomentumMapCovectorLinear := heq
        _ = uniqueCotangentCoordinate • (LinearMap.id : ℝ →ₗ[ℝ] ℝ) := hnoeth
    have h1 :=
      congrArg (fun φ : PostingDual => φ (1 : ℝ)) hfun
    simpa using h1
  · intro hs
    -- Rewrite both sides to the same `s • id` form.
    calc
      pulledBackGaussSource sourceScale a b =
          sourceScale • (LinearMap.id : ℝ →ₗ[ℝ] ℝ) := hpull
      _ = uniqueCotangentCoordinate • (LinearMap.id : ℝ →ₗ[ℝ] ℝ) := by
            rw [hs]
      _ = noetherMomentumMapCovectorLinear := hnoeth.symm

theorem remainingPhysicalEquality_unforced :
    ¬ (∀ sourceScale : ℝ,
      CurrentPremisesWithUniqueRealCotangent sourceScale →
        RemainingPhysicalEquality sourceScale) :=
  uniqueRealCotangent_does_not_force_identification

theorem decoyUnitSourceScale_rejected {n : ℕ} [DecidableEq (Fin n)]
    (a b : Fin n) (hab : a ≠ b) :
    ¬ PulledBackGaussEqualsNoetherMomentumMap decoyUnitSourceScale a b := by
  intro heq
  exact decoyUnitSourceScale_ne_uniqueCotangent
    ((pulledBackGauss_eq_noether_iff_sourceScale_eq_uniqueCotangent
        decoyUnitSourceScale a b hab).1 heq)

/-- **MODEL.** Gauss physical source covector pulled back to the Noether dual
type along the canonical unit-drop embedding. -/
def pulledBackGaussSource {n : ℕ} [DecidableEq (Fin n)]
    (sourceScale : ℝ) (a b : Fin n) : PostingDual :=
  pullbackToPostingDual
    (pairKernelPhysicalSourceCovector sourceScale a b)
    (scalarLineToUnitDropVariation a b)

What this page does not claim

The theorem does not prove that the physical equality between the Noether momentum map and the Gauss source holds. The theorem does not derive the value of the unique cotangent coordinate from the bridge construction itself. The theorem does not identify the physical source with the unique cotangent.

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