amplitude_modulus_bridge
The modulus of the path amplitude equals exp(-rate action) for any two-branch rotation. Workers deriving Born-rule weights from recognition costs cite this to equate amplitude modulus with the square root of the weight. The proof unfolds the amplitude into a product of exponentials, applies complex norm rules, and substitutes the C=2A relation to collapse the real exponent.
claim$|𝒜(γ,φ)| = e^{-A}$ where γ is the recognition path built from a two-branch geodesic rotation, A denotes its rate action, and 𝒜(γ,φ) = exp(-C[γ]/2) ⋅ exp(i φ) with C[γ] the integrated J-cost along γ.
background
The module establishes the central C=2A equivalence: for any two-branch geodesic rotation the recognition action C equals twice the rate action A. Path action is the integral of J-cost over the rate profile of the constructed path. Amplitude is defined as exp(-C/2) times a unit-modulus phase factor exp(i φ). The upstream measurement_bridge_C_eq_2A theorem states that pathAction(pathFromRotation rot) = 2 ⋅ rateAction rot exactly.
proof idea
Unfolds pathAmplitude into the product of exp(-pathAction/2) and exp(i φ). Applies Complex.norm_exp_ofReal to obtain the real exponential for the first factor and unit norm for the phase factor. Invokes measurement_bridge_C_eq_2A to replace pathAction with 2 ⋅ rateAction, then uses norm_mul and ring to finish the equality.
why it matters in Recognition Science
This supplies the modulus form that lets the weight equal the square of the amplitude modulus, directly supporting the module's main C=2A theorem. It links the J-cost functional to quantum amplitudes inside the Recognition Science framework, where the same unique cost governs measurement. No open scaffolding remains; the result is fully discharged.
scope and limits
- Does not apply to paths outside the two-branch geodesic construction.
- Does not derive phase information or interference terms.
- Does not address multi-branch or higher-dimensional rotations.
- Does not prove normalization or the full probability interpretation.
formal statement (Lean)
196theorem amplitude_modulus_bridge (rot : TwoBranchRotation) (φ : ℝ) :
197 ‖pathAmplitude (pathFromRotation rot) φ‖ = Real.exp (- rateAction rot) := by
proof body
Tactic-mode proof.
198 unfold pathAmplitude
199 have hExpReal :
200 ‖Complex.exp (-(pathAction (pathFromRotation rot)) / 2)‖ =
201 Real.exp (-(pathAction (pathFromRotation rot)) / 2) := by
202 simpa using Complex.norm_exp_ofReal (-(pathAction (pathFromRotation rot)) / 2)
203 have hExpI :
204 ‖Complex.exp (φ * Complex.I)‖ = 1 := by
205 simpa using Complex.norm_exp_ofReal_mul_I φ
206 have hAction :
207 -(pathAction (pathFromRotation rot)) / 2 = - rateAction rot := by
208 have h := measurement_bridge_C_eq_2A rot
209 calc
210 -(pathAction (pathFromRotation rot)) / 2
211 = -(2 * rateAction rot) / 2 := by simpa [h]
212 _ = - rateAction rot := by ring
213 calc
214 ‖Complex.exp (-(pathAction (pathFromRotation rot)) / 2)
215 * Complex.exp (φ * Complex.I)‖
216 = ‖Complex.exp (-(pathAction (pathFromRotation rot)) / 2)‖ *
217 ‖Complex.exp (φ * Complex.I)‖ := by simpa using norm_mul _ _
218 _ = Real.exp (-(pathAction (pathFromRotation rot)) / 2) * 1 := by
219 simpa [hExpReal, hExpI]
220 _ = Real.exp (- rateAction rot) := by
221 simpa [hAction]
222
223end Measurement
224end IndisputableMonolith