structure definition def or abbrev

`ProcessingField`

No prose has been written for this declaration yet. The Lean source and graph data below render without it.

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.

acoustic_levitation in IndisputableMonolith.Gravity.AcousticPhaseLevitation decl_use
anti_coherence_reduces_coupling in IndisputableMonolith.Gravity.AcousticPhaseLevitation decl_use
antiGravField in IndisputableMonolith.Gravity.AcousticPhaseLevitation decl_use
antiGravField_cancels in IndisputableMonolith.Gravity.AcousticPhaseLevitation decl_use
any_source_suffices in IndisputableMonolith.Gravity.AcousticPhaseLevitation decl_use
baseline_gravitational_coupling in IndisputableMonolith.Gravity.AcousticPhaseLevitation decl_use
complete_cancellation_is_levitation in IndisputableMonolith.Gravity.AcousticPhaseLevitation decl_use
concrete_levitation in IndisputableMonolith.Gravity.AcousticPhaseLevitation decl_use
effective_gravitational_coupling in IndisputableMonolith.Gravity.AcousticPhaseLevitation decl_use
equilibrium_acceleration in IndisputableMonolith.Gravity.AcousticPhaseLevitation decl_use
equilibrium_is_coherent in IndisputableMonolith.Gravity.AcousticPhaseLevitation decl_use
FullLevitationCert in IndisputableMonolith.Gravity.AcousticPhaseLevitation decl_use
levitation_field_exists in IndisputableMonolith.Gravity.AcousticPhaseLevitation decl_use
LevitationInevitability in IndisputableMonolith.Gravity.AcousticPhaseLevitation decl_use
modified_coherence_defect in IndisputableMonolith.Gravity.AcousticPhaseLevitation decl_use
modified_coherence_defect_expand in IndisputableMonolith.Gravity.AcousticPhaseLevitation decl_use
modified_coherence_defect_simplify in IndisputableMonolith.Gravity.AcousticPhaseLevitation decl_use
modified_falling_condition in IndisputableMonolith.Gravity.AcousticPhaseLevitation decl_use
modified_total_potential in IndisputableMonolith.Gravity.AcousticPhaseLevitation decl_use
partial_weight_reduction in IndisputableMonolith.Gravity.AcousticPhaseLevitation decl_use
UnconditionalLevitationCert in IndisputableMonolith.Gravity.AcousticPhaseLevitation decl_use
weight_reduction_factor in IndisputableMonolith.Gravity.AcousticPhaseLevitation decl_use
coherence_defect in IndisputableMonolith.Gravity.CoherenceFall decl_use
coherence_defect_expand in IndisputableMonolith.Gravity.CoherenceFall decl_use
coherence_defect_simplify in IndisputableMonolith.Gravity.CoherenceFall decl_use
falling_restores_coherence in IndisputableMonolith.Gravity.CoherenceFall decl_use
total_potential_in_frame in IndisputableMonolith.Gravity.CoherenceFall decl_use
energy_distribution_creates_gravity_modifier in IndisputableMonolith.Gravity.EnergyProcessingBridge decl_use
EnergyProcessingEquivalence in IndisputableMonolith.Gravity.EnergyProcessingBridge decl_use
energy_to_processing_field in IndisputableMonolith.Gravity.EnergyProcessingBridge decl_use

… and 2 more

depends on (1)

Lean names referenced from this declaration's body.

Position in IndisputableMonolith.Gravity.CoherenceFall decl_use