IndisputableMonolith.Verification.BornRuleRouteB
Module packaging the Route B hypothesis bundle for the Born-rule derivation (paper Proposition 3.7(a)–(d), pre-processed). It introduces a single structure collecting continuity, splitting, and additivity assumptions on a deviation functional, plus elementary consequences for nonnegative reals. Anyone citing the conditional Born-rule route would import this bundle. The file is definitional scaffolding: no deep proofs, only the interface and immediate algebraic lemmas.
claimRoute B collects hypotheses on a real functional $h$ (deviation from the Born weight): $h(0)=0$, $h(1)=0$, continuity of $h$, a splitting identity, and Cauchy additivity $h(x+y)=h(x)+h(y)$ on a suitable domain. From additivity one obtains $h(n\cdot x)=n\,h(x)$ for $n\in\mathbb{N}$, hence $h$ vanishes on the unit interval and on all nonnegative reals under the standing continuity assumption. A companion deviation map $g$ is recorded alongside the bundle.
background
Recognition Science aims to derive the Born rule (squared-modulus probabilities) from cost and recognition axioms rather than postulate it. Route B is one formal path: assume a small list of analytic and algebraic properties of a deviation functional measuring departure from the Born weight, then conclude the deviation is identically zero.
The module sits in the Verification domain and imports only Mathlib plus RS constants (the native tick $\tau_0$). The central object is the hypothesis structure whose fields are the four clauses of Proposition 3.7(a)–(d): normalization at $0$ and $1$, continuity, a splitting law, and additivity. Downstream lemmas record the standard consequences of Cauchy's equation on $\mathbb{R}_{\ge 0}$ once continuity is present: integer homogeneity and vanishing on the nonnegative ray.
No forcing-chain landmark (T5–T8) is invoked here; the file is pure interface for the Born-rule verification branch.
proof idea
This is a definition-and-interface module, not a theorem file. It declares the Route B hypothesis structure, names the individual field projections (normalization, continuity, splitting, additivity), and proves only the immediate arithmetic corollaries of additivity: $h(nx)=n h(x)$ by induction, $h(0)=0$ on the unit, and, with continuity, $h\equiv 0$ on $\mathbb{R}_{\ge 0}$. No external RS lemmas beyond the constants import are required.
why it matters in Recognition Science
The bundle is the pre-processed hypothesis package for paper Proposition 3.7(a)–(d) on the Born-rule Route B. It isolates exactly the analytic assumptions a later uniqueness or vanishing theorem will discharge, keeping the verification layer modular. With no recorded downstream dependents in the current graph, the module is an entry point for any proof that the Born weight is the unique continuous additive solution compatible with the recognition cost. It does not itself close the Born-rule derivation; it only standardizes the hypotheses so that conditional theorems can cite a single structure rather than four loose assumptions.
scope and limits
- Does not prove the Born rule; only packages hypotheses.
- Does not derive continuity or additivity from RS axioms.
- Does not address discrete or non-measurable solutions of Cauchy's equation.
- Does not connect to the forcing chain T5–T8 or the J-cost uniqueness theorem.
- Does not supply a numerical or experimental check of the Born weights.
depends on (1)
declarations in this module (17)
-
structure
RouteBHyp -
def
hSub -
theorem
hSub_zero -
theorem
hSub_one -
theorem
hSub_cont -
theorem
hSub_split -
theorem
hSub_additive -
theorem
additive_nat_mul -
theorem
additive_nat_zero -
theorem
additive_zero_on_unit -
theorem
additive_zero_on_nonneg -
def
gDev -
theorem
hSub_eq_id -
theorem
born_rule_route_B -
theorem
modulus_multiplicativity -
structure
RouteBCert -
theorem
route_B_certified