C_equals_2A
plain-language theorem explainer
The theorem establishes existence of real numbers C and A for any two-branch rotation such that C equals twice A and the exponential of negative C equals the initial amplitude squared. Researchers deriving the Born rule from recognition actions in the Recognition Science framework cite this lightweight bridge. The proof constructs C and A directly from the rate action and reduces the amplitude equality via conversion from the born weight theorem plus ring simplification.
Claim. For any two-branch rotation ρ, there exist real numbers C and A such that C = 2A and exp(−C) equals the initial amplitude squared of ρ.
background
The module supplies a paper-safe export of the central C = 2A bridge to avoid heavy dependencies in the Measurement domain. Upstream, the born weight from rate theorem states that exp(−2 × rate action) equals sin²(θ_s) for rotation angle θ_s. The rate action is defined as −log(sin θ_s), so the exponential relation directly supplies the amplitude square that appears in the Born rule emergence section of the coherence collapse module.
proof idea
The proof is a term-mode construction that instantiates C as twice the rate action of the rotation and A as the rate action itself. It verifies C = 2A by the ring tactic. It then simplifies the initial amplitude squared definition and converts the born weight from rate theorem, adjusting the second conjunct by ring to obtain the required exponential equality.
why it matters
This theorem supplies the C is 2A fact used by the coherence collapse certificate (which packages it with positivity and normalization) and by the born rule from C theorem that constructs the two-outcome measurement. It realizes the central recognition action equals twice rate action relation in lightweight form, supporting Born rule emergence without full dependency overhead. The relation connects to the eight-tick octave and phi-ladder through the rate action definitions.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.