module module high

`IndisputableMonolith.Foundation.BranchSelection`

This module defines predicates that exclude trivial additive combiners from genuine composition in the Recognition Science foundation. It introduces SeparatelyAdditive as the case P(u,v) = p(u) + q(v) and interactionDefect as its deviation measure, plus related coupling predicates. Researchers tracing the forcing chain cite these to enforce non-trivial branches. The module supplies definitions and equivalences rather than a central theorem.

claimA combiner $P : ℝ → ℝ → ℝ$ is separately additive when $P(u,v) = p(u) + q(v)$ for functions $p,q : ℝ → ℝ$. The interaction defect of $P$ quantifies deviation from this form. Related predicates characterize when $P$ is a coupling combiner or satisfies the RCLCombiner condition.

background

The module belongs to the Foundation domain and supplies structural filters for composition consistency. It defines SeparatelyAdditive to capture the excluded additive shape and interactionDefect to measure its failure. Sibling definitions include IsCouplingCombiner, RCLCombiner, and the equivalences separatelyAdditive_iff_interactionDefect_zero together with RCLCombiner_isCoupling_iff.

proof idea

This is a definition module, no proofs.

why it matters in Recognition Science

The module feeds the root IndisputableMonolith, which exposes the master forcing-chain theorem and the T0-T8 landmarks. It supplies the branch-selection predicates required to exclude separately additive cases before J-uniqueness (T5) and the eight-tick octave (T7) are applied.

scope and limits

Does not prove the master forcing-chain theorem.
Does not introduce the phi-ladder or mass formulas.
Does not define constants such as G or alpha.
Does not treat the Berry creation threshold or Z_cf.

used by (1)

From the project-wide theorem graph. These declarations reference this one in their body.

IndisputableMonolith module_import

declarations in this module (17)

def SeparatelyAdditive L47
def IsCouplingCombiner L54
def interactionDefect L63
theorem interactionDefect_eq_zero_of_separatelyAdditive L70
theorem separatelyAdditive_of_interactionDefect_zero L82
theorem separatelyAdditive_iff_interactionDefect_zero L93
theorem isCouplingCombiner_iff_interactionDefect_nonzero L100
def RCLCombiner L117
theorem interactionDefect_RCLCombiner L122
theorem RCLCombiner_zero_separatelyAdditive L130
theorem RCLCombiner_nonzero_couples L139
theorem RCLCombiner_isCoupling_iff L145
theorem branch_selection L173
theorem additive_branch_not_coupling L180
structure BranchSelectionCert L192
def branchSelectionCert L206
theorem branchSelectionCert_inhabited L215