Measurement C2 Abridge Light C Equals 2 A

The bridge

In ordinary physics, a decay rate and an initial amplitude are different kinds of quantities: one tells you how fast something fades, the other how strong it starts. The Recognition Science declaration C_equals_2A states that, under a specific two-branch rotation model, these two are not independent. It proves that there exist real numbers C and A such that C = 2A and exp(-C) equals the initial amplitude squared. In plain words, the decay constant is twice the action rate, and the exponential of minus that decay constant matches the square of the starting amplitude.

The theorem is a lightweight export, a paper-safe version of a larger bridge result, kept free of heavy dependencies so it can be cited without loading the whole framework. It is a machine-checked theorem in the framework's library of formal theorems, meaning the proof has been verified by a computer. The proof uses the definition of initial amplitude squared and a prior result about the born weight from the rate. The statement is existential: it asserts that such numbers exist, and it constructs them explicitly as twice the rate action and the rate action itself.

What the declaration does not claim is just as important. It does not say that C and A are physically measurable in any experiment, nor does it interpret what the initial amplitude represents. The theorem is conditional on a two-branch rotation model; without that model, the relationship does not follow. It also does not claim uniqueness: there may be other pairs satisfying the equation, and the theorem only guarantees one. Finally, it does not assert that exp(-C) is a probability or a physical observable; it only states a mathematical equality within the model.

/-- Lightweight export: existence of C and A with C = 2A and exp(-C) match. -/
theorem C_equals_2A (rot : TwoBranchRotation) :
  ∃ (C A : ℝ), C = 2 * A ∧ Real.exp (-C) = initialAmplitudeSquared rot := by
  use 2 * rateAction rot, rateAction rot
  refine ⟨by ring, ?_⟩
  simp only [initialAmplitudeSquared]
  have h := born_weight_from_rate rot
  convert h using 2
  ring

/-- Lightweight export: existence of C and A with C = 2A and exp(-C) match. -/
theorem C_equals_2A (rot : TwoBranchRotation) :
  ∃ (C A : ℝ), C = 2 * A ∧ Real.exp (-C) = initialAmplitudeSquared rot := by
  use 2 * rateAction rot, rateAction rot
  refine ⟨by ring, ?_⟩
  simp only [initialAmplitudeSquared]
  have h := born_weight_from_rate rot
  convert h using 2
  ring

What this page does not claim

The theorem does not claim that C and A are measurable physical quantities. It does not claim that the pair (C, A) is unique. It does not claim that exp(-C) is a probability or observable.

Verify this page

Every tagged claim above names its theorem. To check one yourself rather than trust this page, elaborate the source module with Lean 4 and audit its axiom basis:

$ lake env lean IndisputableMonolith/Measurement/C2ABridgeLight.lean
expected axiom basis: [propext, Classical.choice, Quot.sound] (the Lean kernel's standard three; no RS-specific axioms)

A page whose claims cannot be reproduced this way does not ship. In production, every anchor links to the exact declaration in the public source release, and this block carries the build receipt for the page itself.

Derived articles

This page is generated by a question-recursion engine: the questions its answers raise become the next pages. The current agenda, with open targets marked red: