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

IsTimeTranslationInvariant

show as:
view Lean formalization →

The predicate requires that a recognition field and its metric take identical values at four-vectors differing only in the time coordinate. Researchers deriving Noether-type conservation laws from the Recognition Hamiltonian cite this predicate when establishing time-independent energy. It is introduced directly by universal quantification over all real times and fixed integer spatial indices.

claimA recognition field $ψ : (ℝ^4 → ℝ)$ and metric tensor $g$ are time-translation invariant if $ψ(x_1) = ψ(x_2)$ and $g(x_1) = g(x_2)$ whenever the four-vectors $x_1, x_2$ differ only in their time component, for all $t_1, t_2 ∈ ℝ$ and all spatial indices $ijk ∈ ℤ^3$.

background

The Recognition Hamiltonian Formalism module derives the Hamiltonian for the Recognition Reality Field with the explicit objective of proving energy conservation as a consequence of time-translation symmetry in the ledger. The RRF is the local interface given by functions from four-dimensional coordinates to the reals. The MetricTensor is the structure supplying the metric components on those coordinates. TotalHamiltonian is defined as the spatial integral of the Hamiltonian density over the cubic voxel lattice at fixed time.

proof idea

As a definition the predicate is introduced directly by the displayed universal quantification over times and spatial indices together with the pointwise equality conditions on the field and metric.

why it matters in Recognition Science

This definition supplies the antecedent hypothesis for the energy conservation theorem, which concludes that the total recognition energy is independent of time whenever the invariance holds. It thereby implements the Noether correspondence between time-translation symmetry and energy conservation inside the Recognition framework, linking the Hamiltonian construction to the forcing chain steps that fix D = 3 and the eight-tick octave.

scope and limits

Lean usage

theorem energy_conservation (h : H_EnergyConservation psi g) (psi : RRF) (g : MetricTensor) : IsTimeTranslationInvariant psi g → (∀ t, TotalHamiltonian psi g t = TotalHamiltonian psi g 0) := h

formal statement (Lean)

  80def IsTimeTranslationInvariant (psi : RRF) (g : MetricTensor) : Prop :=

proof body

Definition body.

  81  ∀ t₁ t₂ : ℝ, ∀ ijk : Fin 3 → ℤ,
  82    let x₁ : Fin 4 → ℝ := fun i => if i.val = 0 then t₁ else (ijk (match i.val with | 1 => 0 | 2 => 1 | _ => 2) : ℝ)
  83    let x₂ : Fin 4 → ℝ := fun i => if i.val = 0 then t₂ else (ijk (match i.val with | 1 => 0 | 2 => 1 | _ => 2) : ℝ)
  84    psi x₁ = psi x₂ ∧ g.g x₁ = g.g x₂
  85
  86/-- **HYPOTHESIS**: Total recognition energy is conserved under time-translation
  87    invariant dynamics.
  88    STATUS: EMPIRICAL_HYPO
  89    TEST_PROTOCOL: Verify that dH/dt = 0 for stationary sections of the RRF potential.
  90    FALSIFIER: Discovery of a time-translation invariant system where TotalHamiltonian
  91    is not conserved. -/

used by (2)

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

depends on (17)

Lean names referenced from this declaration's body.