pith. machine review for the scientific record. sign in
abbrev definition def or abbrev high

RRF

show as:
view Lean formalization →

The Recognition Reality Field is defined as a real scalar function on four-dimensional spacetime. It forms the core field variable in the Recognition Hamiltonian module, enabling derivations of energy conservation from time-translation invariance. The declaration is a direct type abbreviation with no computational content or lemmas.

claimThe recognition reality field is a scalar map from four-dimensional spacetime coordinates to the reals, written as a function of type $(x^0,x^1,x^2,x^3)mapsto$ real value.

background

The module establishes the Recognition Hamiltonian formalism whose goal is to obtain the Hamiltonian for the Recognition Reality Field and to prove energy conservation follows from time-translation symmetry of the ledger. The field acts as the scalar potential whose values enter the Hamiltonian density via partial derivatives. Time-translation invariance is defined to require that both the field and the metric remain unchanged when the time coordinate is shifted while spatial indices are held fixed.

proof idea

The declaration is a direct abbreviation of the function type from four-dimensional real vectors to the reals. No lemmas or tactics are invoked; the body simply names the type.

why it matters in Recognition Science

This type declaration supplies the field variable used in the energy conservation theorem (if the ledger is time-translation invariant then total Hamiltonian is constant) and in the Hamiltonian density definition. It also supports the small-deviation equivalence result that recovers the standard quadratic Hamiltonian. The definition therefore anchors the Noether argument that converts time-translation symmetry into energy conservation inside the Recognition framework.

scope and limits

formal statement (Lean)

  15abbrev RRF := (Fin 4 → ℝ) → ℝ

proof body

Definition body.

  16
  17/-- Local non-sealed metric interface. -/

used by (40)

From the project-wide theorem graph. These declarations reference this one in their body.

… and 10 more