Measurement C2 Abridge Light

The lightweight bridge

In Recognition Science, measurement often involves two related quantities: a rate action, a numerical measure of how strongly a recognition event acts, and an initial amplitude squared, a value derived from the starting state of a two-branch rotation. The module C2ABridgeLight establishes a concise bridge between them. It proves that for any two-branch rotation, there exist real numbers C and A such that C equals twice A, and the exponential of negative C matches the initial amplitude squared. In plainer terms, the theorem guarantees that a certain exponential decay factor, determined by the rate action, exactly reproduces the initial amplitude squared.

This result is a lightweight export, meaning it avoids heavy dependencies while preserving the core statement. The proof is short: it sets C to twice the rate action and A to the rate action itself, then uses a known property called born_weight_from_rate to complete the match. The practical consequence is that the framework can rely on this bridge without dragging in the full formal apparatus, making the theorem easier to reuse in other contexts.

/-- 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 module does not define the rate action or the initial amplitude squared; it only relates them. The theorem does not specify how to measure either quantity in a physical experiment.

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: