Foundation Pair Kernel Gap2a Integral Lattice Dual Residual Primitive Positive C

The integer character

In Recognition Science, a ledger is a discrete record of events. The simplest such record is a line of whole numbers, one tick for each posting. A character is a way of assigning a number to each tick that respects addition: the value at two ticks together is the sum of the values at each tick alone. The declaration primitivePositiveCharacter_eval_primitivePosting proves, in the machine-checked library of formal theorems, that the unique positive primitive character sends the first tick to the integer 1, and sends every other tick to its own whole number.

That uniqueness is a theorem, not a choice. Any additive character that sends the first tick to 1 must be the identity map, the one that returns each number to itself. The proof is short: the value at any whole number is forced by repeated addition of the value at 1, which is 1. The negation character, sending every tick to its negative, is the unique primitive negative dual. These are facts about the integers alone, with no physical input.

The framework then asks whether this integer uniqueness can select a real number, a source scale for the pair-kernel equation. It cannot. The theorem currentPremisesWithIntegralDual_do_not_select_unique_scale proves that adding the integer dual and its uniqueness still admits two distinct positive real source models, both free of pi. The two banked candidates, A and B, both satisfy every premise, and they differ. No additional premise drawn from the integer character can break the tie.

In Recognition Science, the integer character fixes only the lattice generator, the first tick. It does not fix a real cotangent or Green source. Transporting the integer character into a real scale requires an additional physical identification law, and that law is not supplied by the defined package. The declaration does not claim to classify every possible integral-dual formalization, and it does not smuggle in a source as one over action. It states a negative result: integrality, primitivity, and unique positive character do not attach a unique real source magnitude.

/-- The unique positive primitive character evaluates the elementary posting to
the integer `1`, not to a real source coupling. -/
theorem primitivePositiveCharacter_eval_primitivePosting :
    (primitivePositiveCharacter : ℤ → ℤ) primitivePosting = 1 := by
  simp [primitivePositiveCharacter, primitivePosting]

/-- Uniqueness: any additive character with `χ 1 = 1` is the identity. -/
theorem primitivePositiveCharacter_unique
    (χ : IntegralDual) (hχ : IsPrimitivePositiveCharacter χ) :
    χ = primitivePositiveCharacter := by
  apply AddMonoidHom.ext_int
  simpa [IsPrimitivePositiveCharacter, primitivePositiveCharacter] using hχ

/-- The defined Hom-enriched package still admits both banked positive pi-free
source models. -/
theorem currentPremisesWithIntegralDual_admit_distinct_candidates :
    ∃ sourceScale₁ sourceScale₂ : ℝ,
      sourceScale₁ ≠ sourceScale₂ ∧
        CurrentPremisesWithIntegralDual sourceScale₁ ∧
        CurrentPremisesWithIntegralDual sourceScale₂ :=
  ⟨candidateA_sourceMagnitudeExpr.eval,
    candidateB_sourceMagnitudeExpr.eval,
    candidates_select_distinct_magnitudes,
    candidateA_satisfies_currentPremisesWithIntegralDual,
    candidateB_satisfies_currentPremisesWithIntegralDual⟩

/-- Integrality, primitivity, and unique positive Hom character do not attach a
unique real source magnitude. -/
theorem currentPremisesWithIntegralDual_do_not_select_unique_scale :
    ¬ ∃! sourceScale : ℝ,
      CurrentPremisesWithIntegralDual sourceScale := by
  intro hunique
  rcases hunique with ⟨selected, _hselected, honly⟩
  have hA :
      candidateA_sourceMagnitudeExpr.eval = selected :=
    honly _ candidateA_satisfies_currentPremisesWithIntegralDual
  have hB :
      candidateB_sourceMagnitudeExpr.eval = selected :=
    honly _ candidateB_satisfies_currentPremisesWithIntegralDual
  exact candidates_select_distinct_magnitudes (hA.trans hB.symm)

What this page does not claim

The declaration does not claim that the integer character fixes a real cotangent or Green source. It does not claim that a source can be set as one over action without additional premises. It does not claim to classify every possible integral-dual formalization or real transport.

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