Foundation Pair Kernel Canonical Generator Source S9 Canonical Generator Source

The canonical source

The declaration canonicalGeneratorSource_consumer_exists is a theorem in the framework's machine-checked library of formal theorems. In plain language it proves that for any allowed posting event in the framework's discrete ledger, a record of events where each posting moves one unit from a source to a sink, there exists a canonical source attached to that event. The theorem is conditional: it holds for any torus of size at least two, and for any of the three possible permutations of the spatial axes. It also requires the event to be one of the realized primitive posting pairs, the basic allowed moves in the ledger.

The content of the theorem is that such a canonical source exists, not that it is unique or that it has a particular magnitude. The existence is established together with a certificate, a structure that witnesses the source's defining property. The proof is constructive in the sense that the library defines the source explicitly: for a posting of magnitude q, the source is a scaled dipole with coefficient q divided by two. For the primitive posting, where q equals one, the canonical Green source scale is exactly one half. This scale is not fitted to any data; it follows from the normalization of the ledger action, where one posting has divergence plus one at its source and minus one at its sink, and the fixed pair action has first variation twice the Laplacian.

The theorem does not claim that the source is unique. The library proves that two candidate scales, one half and another value, are distinct, but it does not prove that only one canonical source exists for a given event. The theorem also does not assign any physical dimension to the posting magnitude. The magnitude q remains an explicit parameter, and the same theorem divides it by two. No hydrogen benchmark or other empirical datum appears in the statement or its proof. The result is relative to the ledger action unit, and a later physical conversion may assign a dimensional magnitude to one posting; that conversion is not part of this theorem.

What the theorem changes is the status of the source side in the framework's production graph. Before this result, the source side was constructed from the finite set of witnessed minimum-cost posting pairs. This theorem attaches the canonical source without fitting a number, and it does so with a proof that contains no unproved assumptions and no new axioms. The reader can now see that the one-half scale is a consequence of the ledger's own normalization, not an input.

/-- A witnessed primitive posting exists, so the canonical package has a
closed downstream consumer with neither a free graph nor a free ledger source
scale. The physical posting-magnitude attachment remains the explicit residual
above. -/
theorem canonicalGeneratorSource_consumer_exists
    {N : ℕ} [NeZero N]
    (hN : 2 ≤ N)
    (σ : Equiv.Perm (Fin 3)) :
    ∃ event : PostingPair3 N,
      event ∈ realizedPrimitivePostingPairs3 N ∧
        CanonicalGeneratorSourceCert3 event σ := by
  let p : TorusSite3 N := fun _ => 0
  let q : TorusSite3 N := torusShift p 0 1
  let event : PostingPair3 N :=
    (torusSiteEquivFin N p, torusSiteEquivFin N q)
  have hstep :
      FramedAxisStep (Equiv.refl (Fin 3)) p q :=
    ⟨0, Or.inl rfl⟩
  have hgenerated :
      JMinimalGeneratedStep (Equiv.refl (Fin 3)) p q :=
    (jMinimalGeneratedStep_iff_framedAxisStep
      (Equiv.refl (Fin 3)) p q).mpr hstep
  have hevent :
      event ∈ realizedPrimitivePostingPairs3 N := by
    rw [mem_realizedPrimitivePostingPairs3_iff]
    unfold encodedMinimumJRelation3 event
    simpa using hgenerated
  exact
    ⟨event, hevent,
      canonicalGeneratorSourceCert3 hN event hevent σ⟩

/-- Candidate A agrees algebraically with the primitive ledger magnitude.
This does not derive Candidate A's physical instrument attachment. -/
theorem candidateA_greenScale_eq_half :
    realGreenScaleFromPostingMagnitude
        candidateA_sourceMagnitudeExpr.eval =
      1 / 2 := by
  rw [candidateA_sourceMagnitude_eq_one]
  rfl

/-- The two still-open physical magnitude attachments remain distinct after
the theorem-backed action/Gauss normalization. -/
theorem candidate_greenScales_distinct :
    realGreenScaleFromPostingMagnitude
        candidateA_sourceMagnitudeExpr.eval ≠
      realGreenScaleFromPostingMagnitude
        candidateB_sourceMagnitudeExpr.eval := by
  intro h
  unfold realGreenScaleFromPostingMagnitude at h
  have hmul := congrArg (fun x : ℝ => x * 2) h
  have heq :
      candidateA_sourceMagnitudeExpr.eval =
        candidateB_sourceMagnitudeExpr.eval := by
    linarith
  exact candidates_select_distinct_magnitudes heq

What this page does not claim

The theorem does not prove that the canonical source is unique for a given event. The theorem does not assign a dimensional magnitude to one ledger posting. The theorem does not use any hydrogen or benchmark datum.

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