Foundation Pair Kernel Gap2a Noether Momentum Map Carrier Legal Atomic Tick Mome

The unique charge

In physics, a momentum map assigns a conserved quantity to a motion that respects a symmetry. The Recognition Science framework builds the same idea for its most basic unit of bookkeeping: the ledger, a discrete record of events. Its declaration legalAtomicTickMomentumMap_exists_unique proves that every legal atomic tick, one indivisible posting step in the ledger, carries exactly one such quantity. The theorem is machine-checked in the framework's library of formal theorems.

The construction starts with a legal atomic tick and its action, the cost of making that posting. The framework's symplectic structure, a geometric setting for classical mechanics, already provides the rules for how actions combine. The momentum-map covector is the unique real-linear functional, a map from numbers to numbers that respects addition and scaling, that pairs the action generator to the primitive character, a basic unit of measurement. In plainer terms: the framework finds the one price that makes the posting's own cost consistent with its motion.

The theorem's force is twofold. It proves existence, there is at least one such quantity, and uniqueness, there is exactly one. The same quantity works for every legal atomic tick, independent of the particular ledger state before and after the posting. It also coincides numerically with the already-derived unique action-lattice cotangent coordinate, a separate coordinate system in the framework, confirming the construction is not a renaming but a genuine match. The quantity is conserved along the posting's action orbit, the continuous path generated by its action, and it is not the trivial unpriced covector, which would simply map everything to itself and fails the required pairing.

In Recognition Science, this result fills a specific gap: it supplies the missing real covector carrier for a legal atomic tick as a Noether charge, a conserved quantity associated with a symmetry. It does not claim that this carrier is the physical pair-kernel source, the independently constructed physical source covector. It does not assume the source times action equals unit, the native action dual source law, the Green-sum continuum, or endpoint data. The equality to an independent physical source remains open, recorded as a schema for a future theorem.

theorem legalAtomicTickMomentumMap_exists_unique
    {d : Nat} {L L' : LedgerPostingAdjacency.LedgerState d}
    (tick : LedgerPostingAdjacency.LegalAtomicTick (d := d) L L') :
    ∃! μ : PostingDual, IsNoetherMomentumMapCovector μ := by
  refine ⟨noetherMomentumMapCovector tick,
    noetherMomentumMapCovector_isOperational tick, ?_⟩
  intro μ hμ
  exact (legalAtomicTickMomentumMap_unique tick μ).1 hμ

/-- Uniqueness: any operational momentum-map covector equals the constructed
carrier. -/
theorem noetherMomentumMapCovector_unique
    (μ : PostingDual) (hμ : IsNoetherMomentumMapCovector μ) :
    μ = noetherMomentumMapCovectorLinear := by
  have hExt : ExtendsPrimitiveCharacterAlongAction μ := hμ.2
  have hCanon : μ = canonicalRealCharacterExtension :=
    uniqueRealCharacterExtension μ hExt
  exact hCanon.trans noetherMomentumMapCovectorLinear_eq_canonical.symm

/-- All realized LedgerPostingAdjacency.LegalAtomicTicks share the same momentum-map covector. -/
theorem noetherMomentumMapCovector_independent_of_tick
    {d₁ d₂ : Nat}
    {L₁ L₁' : LedgerPostingAdjacency.LedgerState d₁} {L₂ L₂' : LedgerPostingAdjacency.LedgerState d₂}
    (tick₁ : LedgerPostingAdjacency.LegalAtomicTick (d := d₁) L₁ L₁')
    (tick₂ : LedgerPostingAdjacency.LegalAtomicTick (d := d₂) L₂ L₂') :
    noetherMomentumMapCovector tick₁ = noetherMomentumMapCovector tick₂ :=
  rfl

theorem noetherMomentumMapCoordinate_eq_uniqueCotangent :
    noetherMomentumMapCoordinate = uniqueCotangentCoordinate := by
  simp [noetherMomentumMapCoordinate, uniqueCotangentCoordinate,
    atomicTickActionGenerator_eq_nativeActionQuantum]

theorem atomicTickOrbitNoetherCharge_conserved :
    IsConservedAlong atomicTickOrbitNoetherCharge atomicTickActionOrbit.flow :=
  noether_core (G := atomicTickActionOrbit)
    (J := atomicTickOrbitNoetherCharge) (fun _t _a => rfl)

What this page does not claim

The carrier is not identified with the physical pair-kernel source. The theorem does not assume the source times action equals unit. The equality to an independent physical source is not proved here.

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