`WeakFieldPair`

definition

show as: view math explainer →

module: IndisputableMonolith.Gravity.WeakFieldSuperposition
domain: Gravity
line: 67 · github
papers citing: none yet

open explainer

Generate a durable explainer page for this declaration.

open lean source

IndisputableMonolith.Gravity.WeakFieldSuperposition on GitHub at line 67.

browse module

All declarations in this module, on Recognition.

explainer page

Tracked in the explainer inventory; generation is lazy so crawlers do not trigger LLM jobs.

open explainer

depends on

used by

formal source

  64
  65/-- Two independent processing fields (gravitational + external).
  66    In the weak-field regime, their combined effect is their sum. -/
  67structure WeakFieldPair where
  68  field_grav : ProcessingField
  69  field_ext : ProcessingField
  70
  71/-- The combined processing field: pointwise addition. -/
  72def WeakFieldPair.combined (pair : WeakFieldPair) : ProcessingField where
  73  phi h := pair.field_grav.phi h + pair.field_ext.phi h
  74
  75/-- SUPERPOSITION THEOREM: In the weak-field regime, the gradient of the combined
  76    field equals the sum of the individual gradients.
  77
  78    This is the key result that justifies the linear addition in CoherenceFall. -/
  79theorem gradient_superposition (pair : WeakFieldPair) (h0 : Position)
  80    (h_diff_grav : DifferentiableAt ℝ pair.field_grav.phi h0)
  81    (h_diff_ext : DifferentiableAt ℝ pair.field_ext.phi h0) :
  82    deriv pair.combined.phi h0 =
  83    deriv pair.field_grav.phi h0 + deriv pair.field_ext.phi h0 := by
  84  simp only [WeakFieldPair.combined]
  85  exact deriv_add h_diff_grav h_diff_ext
  86
  87/-- COHERENCE DEFECT SUPERPOSITION: The coherence defect of the combined field
  88    decomposes as expected from the sum of gradients. -/
  89theorem coherence_defect_of_combined (pair : WeakFieldPair) (obj : ExtendedObject) (a : ℝ)
  90    (h_diff_grav : DifferentiableAt ℝ pair.field_grav.phi obj.h_cm)
  91    (h_diff_ext : DifferentiableAt ℝ pair.field_ext.phi obj.h_cm) :
  92    coherence_defect pair.combined obj a =
  93    abs (2 * obj.extent *
  94      (deriv pair.field_grav.phi obj.h_cm + deriv pair.field_ext.phi obj.h_cm + a)) := by
  95  rw [coherence_defect_simplify]
  96  congr 1; congr 1; congr 1
  97  exact gradient_superposition pair obj.h_cm h_diff_grav h_diff_ext

papers checked against this theorem

No papers in the current corpus map onto this theorem yet.