Foundation Pair Kernel Exact Jnonlinear Gauss S13 Native Curvature Signed Postin

The native curvature response

The declaration nativeCurvatureSignedPostingAttachment3_realGreen is a theorem in the Recognition Science framework's machine-checked library. It concerns a discrete model where a field on a torus interacts through a nonlinear Gauss law. The theorem states that a particular field, constructed by scaling a known solution, satisfies the required equation when the background curvature is set to the value 1 + hbar, where hbar is a framework constant. This is a purely mathematical statement about a specific construction, verified by the Lean proof assistant with no unproven assumptions.

The setting is a finite graph, a weighted ledger graph, where each edge carries a weight and the field values live on the vertices. The nonlinear Gauss law here is derived from an action, a sum over edges of the form cosh(field_i - field_j) - 1. The theorem shows that the field defined by constantCurvatureSignedGreenField3, which scales a known Green's function by the source magnitude divided by the curvature, satisfies the equation ScaledSourceEquation for this specific curvature. This is a concrete existence result: it demonstrates that a valid response exists for this particular background.

The theorem is careful about its scope. It does not claim that the constant curvature background is physically realized. The docstring explicitly states that realizing this curvature by a global native-drop background remains a separate predicate, a separate open question. It also does not assert anything about the event action hbar, its electromagnetic interpretation, SI conversion, or length. These are all explicitly left out of the theorem's scope. The theorem is a piece of pure mathematics within the framework, not a physical claim.

What this establishes, in plain terms, is that within the Recognition Science framework, a particular mathematical construction works. It provides a valid Green's function response for a nonlinear Gauss law at a specific background curvature. This is a building block, a tool that can be used in further derivations, but it is not itself a statement about the physical world. It is a theorem about a mathematical model, verified to be internally consistent.

theorem nativeCurvatureSignedPostingAttachment3_realGreen
    {N : ℕ} [NeZero N]
    (hN : 2 ≤ N)
    (event : PostingPair3 N)
    (hevent : event ∈ realizedPrimitivePostingPairs3 N)
    (σ : Equiv.Perm (Fin 3)) :
    ConstantCurvatureSignedPostingAttachment3
      (1 + Constants.hbar) nativeCurvature_pos.le
      nativeOrderedExactJSource event σ
      (constantCurvatureSignedGreenField3
        (1 + Constants.hbar)
        nativeOrderedExactJSource event) :=
  constantCurvatureSignedPostingAttachment3_realGreen
    hN (1 + Constants.hbar) nativeCurvature_pos
      nativeOrderedExactJSource event hevent σ

theorem nativeCurvatureSignedPostingAttachment3_realGreen
    {N : ℕ} [NeZero N]
    (hN : 2 ≤ N)
    (event : PostingPair3 N)
    (hevent : event ∈ realizedPrimitivePostingPairs3 N)
    (σ : Equiv.Perm (Fin 3)) :
    ConstantCurvatureSignedPostingAttachment3
      (1 + Constants.hbar) nativeCurvature_pos.le
      nativeOrderedExactJSource event σ
      (constantCurvatureSignedGreenField3
        (1 + Constants.hbar)
        nativeOrderedExactJSource event) :=
  constantCurvatureSignedPostingAttachment3_realGreen
    hN (1 + Constants.hbar) nativeCurvature_pos
      nativeOrderedExactJSource event hevent σ

What this page does not claim

The theorem does not claim the constant curvature background is physically realized. It does not assert any electromagnetic interpretation or SI conversion for the framework constants. It does not claim the event action hbar has a specific physical meaning.

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