IndisputableMonolith.Foundation.BranchSelection
Foundation module classifying two-argument combiners P:R×R→R as separately additive (P(u,v)=p(u)+q(v)) versus genuinely coupling. It introduces an interaction defect that vanishes exactly on the additive class, then specializes to the RCL combiner. Anyone proving composition consistency or excluding product-factor branches cites these equivalences. The development is definitional plus short algebraic iff chains.
claimA combiner $P:\mathbb{R}\to\mathbb{R}\to\mathbb{R}$ is separately additive if $P(u,v)=p(u)+q(v)$ for unary $p,q$. The interaction defect of $P$ is zero iff $P$ is separately additive, and nonzero iff $P$ is a coupling combiner. The RCL combiner satisfies the same dichotomy: it is separately additive precisely when the defect vanishes, and couples otherwise.
background
Recognition Science forces physics from a single functional equation, the Recognition Composition Law (RCL) $J(xy)+J(x/y)=2J(x)J(y)+2J(x)+2J(y)$. Combiners $P$ package how two scalar channels are joined before $J$ is applied. The structural shape that must be excluded from genuine composition consistency is separate additivity: existence of unary $p,q$ with $P(u,v)=p(u)+q(v)$ for all real $u,v$. Such $P$ never mixes the channels.
The module works over plain $\mathbb{R}$ (Mathlib only) and introduces an interaction defect that quantifies failure of separate additivity. A coupling combiner is defined as one whose defect is nonzero. The RCL-derived combiner is the principal example: its defect vanishes exactly on the degenerate (separately additive) locus and is nonzero when the channels actually interact.
proof idea
Definition layer first: SeparatelyAdditive, IsCouplingCombiner, and the real-valued interactionDefect. Three short lemmas then close the circle: defect zero of separate additivity, the converse reconstruction, and the iff. Coupling is defined as nonzero defect, yielding the matching iff. RCLCombiner is introduced as a concrete $P$; direct evaluation shows its defect vanishes precisely on the separately additive case and is nonzero otherwise, so the same dichotomy holds for the RCL combiner.
why it matters in Recognition Science
Branch selection in the forcing chain needs a clean cut between product-factor (non-mixing) combiners and those that implement genuine RCL composition. This module supplies that cut: separate additivity is exactly defect zero, and the RCL combiner couples precisely when the defect is nonzero. Downstream arguments that rule out non-interacting branches, or that identify the unique consistent composition law with the T5 J-cost and the self-similar fixed point $\phi$, rest on these equivalences. The module is pure foundation scaffolding for the RCL side of UnifiedForcingChain; it does not itself force dimension or the eight-tick octave.
scope and limits
- Does not derive the RCL identity itself; only classifies combiners relative to it.
- Does not force J-uniqueness, phi, eight-tick structure, or D=3.
- Does not treat combiners on domains other than real scalars.
- Does not quantify physical units or mass-ladder consequences of coupling.
- Does not assert uniqueness of the RCL combiner among all coupling maps.
declarations in this module (17)
-
def
SeparatelyAdditive -
def
IsCouplingCombiner -
def
interactionDefect -
theorem
interactionDefect_eq_zero_of_separatelyAdditive -
theorem
separatelyAdditive_of_interactionDefect_zero -
theorem
separatelyAdditive_iff_interactionDefect_zero -
theorem
isCouplingCombiner_iff_interactionDefect_nonzero -
def
RCLCombiner -
theorem
interactionDefect_RCLCombiner -
theorem
RCLCombiner_zero_separatelyAdditive -
theorem
RCLCombiner_nonzero_couples -
theorem
RCLCombiner_isCoupling_iff -
theorem
branch_selection -
theorem
additive_branch_not_coupling -
structure
BranchSelectionCert -
def
branchSelectionCert -
theorem
branchSelectionCert_inhabited