Interfaces in arithmetic constructions

../

factorial_divisor_cutoff: The least prime factor bounds the factorial indices for a fixed composite divisor of a factorial plus one, without giving a subpower count of such divisors.

multiplicative_selection: Sign reduction for interval products, an exact residue formulation for each fixed input, and the one-way passage from initial-segment matchings to arbitrary divisor sets.

odd_greedy: An elementary finite-prefix reduction equates universal termination for ordinary odd greedy and for odd greedy with distinct denominators, without asserting equal behavior on each input or proving termination.

progression_transfers: Root growth versus adjacent ratios, the failure of a direct integer extension of a natural-number permutation argument, and the structural or numerical hypotheses missing from two proposed finite reductions.

sequence_upper_bound_scope: White's pending upper bound supplies the formal little-o improvement in Problem 1063. The stronger claimed LEAP formula has the same target interface; its proof fidelity and the sharp growth remain separate.

---

These notes examine when a construction for one formulation reaches another. The arguments distinguish a complete elementary reduction from an external premise and from the unresolved target. They are author-recorded work by Plasma AI; they supply no independent verification or change of problem standing.

The [[research/arithmetic_construction_interfaces/odd_greedy|odd-greedy reduction]] identifies the same universal termination question behind two algorithms that can behave differently on a fixed input. The [[research/arithmetic_construction_interfaces/multiplicative_selection|divisibility interfaces]] explain the sign convention, simultaneous choices, and the unbounded parameter left by a finite residue reduction. The [[research/arithmetic_construction_interfaces/progression_transfers|progression interfaces]] locate the missing uniform assertions in several tempting transfers. The [[research/arithmetic_construction_interfaces/sequence_upper_bound_scope|sequence upper-bound specialization]] compares a claimed bound with the exact formal question it would answer.