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

ProcessingField

show as:
view Lean formalization →

ProcessingField packages a real-valued potential function over heights. Acoustic levitation and coherence-coupling proofs cite it to supply the gravitational gradient for cancellation arguments. The declaration is a bare structure with one field, introduced without lemmas or proof obligations.

claimA processing field is a map $Phi : R to R$ giving the gravitational potential at each height.

background

In the CoherenceFall module, Position is the abbreviation for the real line, used as the one-dimensional height coordinate. ProcessingField is the structure that carries the potential function phi from these positions to reals. The module imports only Mathlib and supplies this type for all subsequent gradient and defect calculations.

proof idea

The declaration is a structure definition that directly introduces the phi component. No lemmas or tactics are applied.

why it matters in Recognition Science

It supplies the gravitational potential type required by acoustic_levitation, which concludes that exact gradient cancellation yields zero modified coherence defect. The same type appears in anti_coherence_reduces_coupling, antiGravField, and baseline_gravitational_coupling. Within Recognition Science it operationalizes the gravitational term inside the coherence-restoration dynamics that follow from the T5 J-uniqueness and T8 three-dimensional forcing chain.

scope and limits

formal statement (Lean)

  34structure ProcessingField where
  35  /-- Potential function Φ(h) -/
  36  phi : Position → ℝ
  37

used by (32)

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

… and 2 more

depends on (1)

Lean names referenced from this declaration's body.