OAI/Analysis/LipschitzHilbert/Trees/SourcePathAmplitudeCongr.lean

GitHub source file

4 declarations, 0 contain sorry, 0 declared as axioms

Exact node amplitude identities preserve the path ratios and their predictors. This permits literal regrouping of physical packets before the marked path integral, without changing any mass or transition.

  1. theorem OAI.LipschitzHilbert.AngularGrid.sourceBlockNodeRatio_congr_amplitude line 27
  2. theorem OAI.LipschitzHilbert.AngularGrid.sourceShiftedPathRatio_congr_amplitude line 34
  3. theorem OAI.LipschitzHilbert.AngularGrid.sourceActivePathValue_congr_amplitude line 43
  4. theorem OAI.LipschitzHilbert.AngularGrid.sourceShiftedPathPrediction_congr_amplitude line 58