Coverage

Manuscript: Chemotaxis models with signal-dependent sensitivity and a logistic-type source, III: Bifurcation and spike-like solutions, arXiv:2610.20976v2.

Paper results: 73 (47 same assumptions, 23 inputs supplied, 3 outside this formalization).
lean-pkg’s claims ledger: ready (sha256:f931501bf70fa8a5…).

Paper	Title	Correspondence	Claims	Lean declarations	Ledger	Inputs	Note
Proposition 1.1	Linear stability/instability	Same assumptions	`chemotaxis-bifurcation-lean/chemotaxisbifurcation-physicallinearregime-criticalsensitivity-eq-chistar` `chemotaxis-bifurcation-lean/chemotaxisbifurcation-physicallinearregime-minimizingmode-beta-iff` `chemotaxis-bifurcation-lean/chemotaxisbifurcation-physicallinearregime-physicalgrowth-eq-coupled` `chemotaxis-bifurcation-lean/chemotaxisbifurcation-physicallinearregime-physicalgrowth-neg-iff` `chemotaxis-bifurcation-lean/chemotaxisbifurcation-physicallinearregime-physicalgrowth-pos-iff` `chemotaxis-bifurcation-lean/chemotaxisbifurcation-physicallinearregime-physicalgrowth-zero-iff` `chemotaxis-bifurcation-lean/chemotaxisbifurcation-physicallinearregime-strictcriticalmode-other-growth-neg`	`ChemotaxisBifurcation.PhysicalLinearRegime.criticalSensitivity_eq_chiStar` `ChemotaxisBifurcation.PhysicalLinearRegime.minimizingMode_beta_iff` `ChemotaxisBifurcation.PhysicalLinearRegime.physicalGrowth_eq_coupled` `ChemotaxisBifurcation.PhysicalLinearRegime.physicalGrowth_neg_iff` `ChemotaxisBifurcation.PhysicalLinearRegime.physicalGrowth_pos_iff` `ChemotaxisBifurcation.PhysicalLinearRegime.physicalGrowth_zero_iff` `ChemotaxisBifurcation.PhysicalLinearRegime.strictCriticalMode_other_growth_neg`	verified verified verified verified verified verified verified	—	V2 scope: The semigroup and nonlinear PDE stability conclusions in the proposition are excluded; this row covers only modewise ordered-field algebra. Source locator: p. 5, TeX line 500.
Theorem 1.1 (PDE branches and stability)	Local pitchfork bifurcation: curves, expansions and PDE stability	Outside this formalization	—	—	—	—	V2 scope: Requires center-manifold construction, finite-regularity remainder control, implicit bifurcation, and PDE spectral stability. Source locator: p. 6, TeX line 580.
Theorem 1.1 (reduced scalar equation)	Local pitchfork bifurcation: equilibria of the reduced scalar equation	Inputs supplied	`chemotaxis-bifurcation-lean/chemotaxisbifurcation-mixedremainder-reducedfield` `chemotaxis-bifurcation-lean/chemotaxisbifurcation-mixedremainder-mixed-equilibrium-core` `chemotaxis-bifurcation-lean/chemotaxisbifurcation-mixedremainder-mixed-parameter-le-amp-sq` `chemotaxis-bifurcation-lean/chemotaxisbifurcation-mixedremainder-mixed-value-bound-absorbed` `chemotaxis-bifurcation-lean/chemotaxisbifurcation-mixedremainder-mixed-deriv-bound-absorbed` `chemotaxis-bifurcation-lean/chemotaxisbifurcation-mixedremainder-mixed-branch-eventually` `chemotaxis-bifurcation-lean/chemotaxisbifurcation-mixedremainder-mixed-side-condition-eventually` `chemotaxis-bifurcation-lean/chemotaxisbifurcation-mixedremainder-exists-pos-equilibrium` `chemotaxis-bifurcation-lean/chemotaxisbifurcation-mixedremainder-branchsmall-eventually` `chemotaxis-bifurcation-lean/chemotaxisbifurcation-mixedremainder-branchsmall` `chemotaxis-bifurcation-lean/chemotaxisbifurcation-mixedremainder-ampconst` `chemotaxis-bifurcation-lean/chemotaxisbifurcation-mixedremainder-absorbedconst` `chemotaxis-bifurcation-lean/chemotaxisbifurcation-mixedremainder-center-ode-final-value-bound-weak` `chemotaxis-bifurcation-lean/chemotaxisbifurcation-mixedremainder-center-ode-final-deriv-bound-weak` `chemotaxis-bifurcation-lean/chemotaxisbifurcation-normalform-paper-equilibrium-core`	`ChemotaxisBifurcation.MixedRemainder.reducedField` `ChemotaxisBifurcation.MixedRemainder.mixed_equilibrium_core` `ChemotaxisBifurcation.MixedRemainder.mixed_parameter_le_amp_sq` `ChemotaxisBifurcation.MixedRemainder.mixed_value_bound_absorbed` `ChemotaxisBifurcation.MixedRemainder.mixed_deriv_bound_absorbed` `ChemotaxisBifurcation.MixedRemainder.mixed_branch_eventually` `ChemotaxisBifurcation.MixedRemainder.mixed_side_condition_eventually` `ChemotaxisBifurcation.MixedRemainder.exists_pos_equilibrium` `ChemotaxisBifurcation.MixedRemainder.branchSmall_eventually` `ChemotaxisBifurcation.MixedRemainder.BranchSmall` `ChemotaxisBifurcation.MixedRemainder.ampConst` `ChemotaxisBifurcation.MixedRemainder.absorbedConst` `ChemotaxisBifurcation.MixedRemainder.center_ODE_final_value_bound_weak` `ChemotaxisBifurcation.MixedRemainder.center_ODE_final_deriv_bound_weak` `ChemotaxisBifurcation.NormalForm.paper_equilibrium_core`	verified verified verified verified verified verified verified verified verified verified verified verified verified verified verified	identification of η=χ₀−χ* and s=u_n₀ with the reduced scalar equation α>0 and β≠0 fixed C≥0 and 0<r≤1 uniform bound \|R(η,s)\|≤C(\|s\|η²+\|s\|³\|η\|+s⁴) on \|η\|,\|s\|≤r, or its stronger Eq. 2.43 version HasDerivAt (R η) (Rs η s) s throughout that box uniform derivative bound \|Rs(η,s)\|≤C(η²+s²\|η\|+\|s\|³), or the stronger matching version	V2 scope: The finite scalar side, derivative-sign, and amplitude conclusions are proved from the explicit reduced equation and separate remainder interfaces. Center-manifold reduction, branch existence, and PDE stability lifting remain outside this row. Source locator: p. 6, TeX line 580. arXiv v2: Step 5 of the proof drops the derivative remainder estimate (ledger arxiv_v2_note).
Theorem 1.2(1)	beta_n0 is a quadratic in beta with negative leading coefficient	Inputs supplied	`chemotaxis-bifurcation-lean/chemotaxisbifurcation-betaassemblydata-coeff-quadratic` `chemotaxis-bifurcation-lean/chemotaxisbifurcation-betaassemblydata-constant` `chemotaxis-bifurcation-lean/chemotaxisbifurcation-betaassemblydata-leading` `chemotaxis-bifurcation-lean/chemotaxisbifurcation-betaassemblydata-linear` `chemotaxis-bifurcation-lean/chemotaxisbifurcation-betacoefficientata0-eq-assembly` `chemotaxis-bifurcation-lean/chemotaxisbifurcation-betacoefficientata0-quadratic` `chemotaxis-bifurcation-lean/chemotaxisbifurcation-betadouble-data` `chemotaxis-bifurcation-lean/chemotaxisbifurcation-betaleading-eq-manuscript` `chemotaxis-bifurcation-lean/chemotaxisbifurcation-betaleading-eq-manuscript-pi` `chemotaxis-bifurcation-lean/chemotaxisbifurcation-betaleading-neg` `chemotaxis-bifurcation-lean/chemotaxisbifurcation-betaminus-is-root` `chemotaxis-bifurcation-lean/chemotaxisbifurcation-betaminus-lt-betaplus` `chemotaxis-bifurcation-lean/chemotaxisbifurcation-betaplus-is-root` `chemotaxis-bifurcation-lean/chemotaxisbifurcation-betaquadratic-double-root-factor` `chemotaxis-bifurcation-lean/chemotaxisbifurcation-betaquadratic-factor-of-root` `chemotaxis-bifurcation-lean/chemotaxisbifurcation-betaquadratic-factor-two-roots` `chemotaxis-bifurcation-lean/chemotaxisbifurcation-betaregime-conditions-exhaustive` `chemotaxis-bifurcation-lean/chemotaxisbifurcation-betaregime-conditions-pairwise-disjoint` `chemotaxis-bifurcation-lean/chemotaxisbifurcation-betaroots-nonnegative-of-c-nonpos-b-pos` `chemotaxis-bifurcation-lean/chemotaxisbifurcation-betaroots-sign-of-c-pos` `chemotaxis-bifurcation-lean/chemotaxisbifurcation-cofactor-neg-of-pos-constant` `chemotaxis-bifurcation-lean/chemotaxisbifurcation-cubice-eq-at-zero` `chemotaxis-bifurcation-lean/chemotaxisbifurcation-cubicgslope-neg` `chemotaxis-bifurcation-lean/chemotaxisbifurcation-cubicg-eq-affine` `chemotaxis-bifurcation-lean/chemotaxisbifurcation-cubich-eq-affine` `chemotaxis-bifurcation-lean/chemotaxisbifurcation-fixedmassbetacoefficient-physical-quadratic` `chemotaxis-bifurcation-lean/chemotaxisbifurcation-fixedmassbetacoefficient-quadratic` `chemotaxis-bifurcation-lean/chemotaxisbifurcation-logisticbetacoefficient-physical-quadratic` `chemotaxis-bifurcation-lean/chemotaxisbifurcation-logisticbetacoefficient-quadratic` `chemotaxis-bifurcation-lean/chemotaxisbifurcation-physicalbetaa-neg` `chemotaxis-bifurcation-lean/chemotaxisbifurcation-physicalbetacoefficientata0-quadratic` `chemotaxis-bifurcation-lean/chemotaxisbifurcation-physical-regime-case-i` `chemotaxis-bifurcation-lean/chemotaxisbifurcation-physical-regime-case-ii` `chemotaxis-bifurcation-lean/chemotaxisbifurcation-physical-regime-case-iii-double` `chemotaxis-bifurcation-lean/chemotaxisbifurcation-physical-regime-case-iii-zero` `chemotaxis-bifurcation-lean/chemotaxisbifurcation-physical-regime-case-iv-b-nonpos` `chemotaxis-bifurcation-lean/chemotaxisbifurcation-physical-regime-case-iv-discriminant-neg` `chemotaxis-bifurcation-lean/chemotaxisbifurcation-regime-case-i` `chemotaxis-bifurcation-lean/chemotaxisbifurcation-regime-case-ii` `chemotaxis-bifurcation-lean/chemotaxisbifurcation-regime-case-iii-double` `chemotaxis-bifurcation-lean/chemotaxisbifurcation-regime-double-nonnegative-root` `chemotaxis-bifurcation-lean/chemotaxisbifurcation-regime-everywhere-neg-of-b-nonpos` `chemotaxis-bifurcation-lean/chemotaxisbifurcation-regime-everywhere-neg-of-discriminant-neg` `chemotaxis-bifurcation-lean/chemotaxisbifurcation-regime-one-positive-root` `chemotaxis-bifurcation-lean/chemotaxisbifurcation-regime-two-nonnegative-roots` `chemotaxis-bifurcation-lean/chemotaxisbifurcation-regime-zero-root` `chemotaxis-bifurcation-lean/chemotaxisbifurcation-secondmodea2slope-neg` `chemotaxis-bifurcation-lean/chemotaxisbifurcation-secondmodea2-eq-affine` `chemotaxis-bifurcation-lean/chemotaxisbifurcation-upow-mul-piscaled`	`ChemotaxisBifurcation.BetaAssemblyData.coeff_quadratic` `ChemotaxisBifurcation.betaAssemblyData_constant` `ChemotaxisBifurcation.betaAssemblyData_leading` `ChemotaxisBifurcation.betaAssemblyData_linear` `ChemotaxisBifurcation.betaCoefficientAtA0_eq_assembly` `ChemotaxisBifurcation.betaCoefficientAtA0_quadratic` `ChemotaxisBifurcation.betaDouble_data` `ChemotaxisBifurcation.betaLeading_eq_manuscript` `ChemotaxisBifurcation.betaLeading_eq_manuscript_Pi` `ChemotaxisBifurcation.betaLeading_neg` `ChemotaxisBifurcation.betaMinus_is_root` `ChemotaxisBifurcation.betaMinus_lt_betaPlus` `ChemotaxisBifurcation.betaPlus_is_root` `ChemotaxisBifurcation.betaQuadratic_double_root_factor` `ChemotaxisBifurcation.betaQuadratic_factor_of_root` `ChemotaxisBifurcation.betaQuadratic_factor_two_roots` `ChemotaxisBifurcation.betaRegime_conditions_exhaustive` `ChemotaxisBifurcation.betaRegime_conditions_pairwise_disjoint` `ChemotaxisBifurcation.betaRoots_nonnegative_of_C_nonpos_B_pos` `ChemotaxisBifurcation.betaRoots_sign_of_C_pos` `ChemotaxisBifurcation.cofactor_neg_of_pos_constant` `ChemotaxisBifurcation.cubicE_eq_at_zero` `ChemotaxisBifurcation.cubicGSlope_neg` `ChemotaxisBifurcation.cubicG_eq_affine` `ChemotaxisBifurcation.cubicH_eq_affine` `ChemotaxisBifurcation.fixedMassBetaCoefficient_physical_quadratic` `ChemotaxisBifurcation.fixedMassBetaCoefficient_quadratic` `ChemotaxisBifurcation.logisticBetaCoefficient_physical_quadratic` `ChemotaxisBifurcation.logisticBetaCoefficient_quadratic` `ChemotaxisBifurcation.physicalBetaA_neg` `ChemotaxisBifurcation.physicalBetaCoefficientAtA0_quadratic` `ChemotaxisBifurcation.physical_regime_case_i` `ChemotaxisBifurcation.physical_regime_case_ii` `ChemotaxisBifurcation.physical_regime_case_iii_double` `ChemotaxisBifurcation.physical_regime_case_iii_zero` `ChemotaxisBifurcation.physical_regime_case_iv_B_nonpos` `ChemotaxisBifurcation.physical_regime_case_iv_discriminant_neg` `ChemotaxisBifurcation.regime_case_i` `ChemotaxisBifurcation.regime_case_ii` `ChemotaxisBifurcation.regime_case_iii_double` `ChemotaxisBifurcation.regime_double_nonnegative_root` `ChemotaxisBifurcation.regime_everywhere_neg_of_B_nonpos` `ChemotaxisBifurcation.regime_everywhere_neg_of_discriminant_neg` `ChemotaxisBifurcation.regime_one_positive_root` `ChemotaxisBifurcation.regime_two_nonnegative_roots` `ChemotaxisBifurcation.regime_zero_root` `ChemotaxisBifurcation.secondModeA2Slope_neg` `ChemotaxisBifurcation.secondModeA2_eq_affine` `ChemotaxisBifurcation.uPow_mul_PiScaled`	verified verified verified verified verified verified verified verified verified verified verified verified verified verified verified verified verified verified verified verified verified verified verified verified verified verified verified verified verified verified verified verified verified verified verified verified verified verified verified verified verified verified verified verified verified verified verified verified verified	identification of the reduced cubic coefficient with E:beta-n0 quadratic graph coefficients E:a_0,i and E:a_k,i>0 and cubic assembly E:Gamma-n0-explicit fixed-mass coefficient identification E:beta-n0-minimal with a=b=a₀=0	Case (iii) is covered for the corrected statement (negativity for beta >= 0, beta != beta_0); see finding v1-misprint-thm12-iii-beta-range. Source locator: p. 8, TeX line 699.
Theorem 1.2(2)	beta_n0 as a rational function of lambda_n0; sign changes and domain-size limits	Inputs supplied	`chemotaxis-bifurcation-lean/chemotaxisbifurcation-coefficientlimits-denominator-ne-zero-at-balancing` `chemotaxis-bifurcation-lean/chemotaxisbifurcation-coefficientlimits-eventually-neg-at-critical-small-domain` `chemotaxis-bifurcation-lean/chemotaxisbifurcation-coefficientlimits-eventually-neg-of-large-domain-limit` `chemotaxis-bifurcation-lean/chemotaxisbifurcation-coefficientlimits-eventually-pos-at-critical-small-domain` `chemotaxis-bifurcation-lean/chemotaxisbifurcation-coefficientlimits-eventually-pos-of-large-domain-limit` `chemotaxis-bifurcation-lean/chemotaxisbifurcation-coefficientlimits-physical-critical-coefficient-sub-first-mode-tendsto-small-domain` `chemotaxis-bifurcation-lean/chemotaxisbifurcation-coefficientlimits-physical-critical-coefficient-tendsto-atbot-of-scriptp-neg` `chemotaxis-bifurcation-lean/chemotaxisbifurcation-coefficientlimits-physical-critical-coefficient-tendsto-atbot-small-domain` `chemotaxis-bifurcation-lean/chemotaxisbifurcation-coefficientlimits-physical-critical-coefficient-tendsto-attop-small-domain` `chemotaxis-bifurcation-lean/chemotaxisbifurcation-coefficientlimits-physical-critical-coefficient-tendsto-large-domain` `chemotaxis-bifurcation-lean/chemotaxisbifurcation-coefficientlimits-physical-critical-coefficient-tendsto-small-domain` `chemotaxis-bifurcation-lean/chemotaxisbifurcation-coefficientlimits-physical-critical-coefficient-tendsto-small-domain-of-d-pos` `chemotaxis-bifurcation-lean/chemotaxisbifurcation-domainlimits-physical-critical-eigenvalue-tendsto-balancing` `chemotaxis-bifurcation-lean/chemotaxisbifurcation-modeexamples-beta-nineteen-tenths-higher-modes-negative` `chemotaxis-bifurcation-lean/chemotaxisbifurcation-modeexamples-beta-three-halves-higher-modes-negative` `chemotaxis-bifurcation-lean/chemotaxisbifurcation-moderootcounts-actual-balanced-zero-lengths-card-le-four` `chemotaxis-bifurcation-lean/chemotaxisbifurcation-moderootcounts-actual-zero-lengths-card-le-five` `chemotaxis-bifurcation-lean/chemotaxisbifurcation-moderootcrossing-physical-coefficient-zero-of-zero-numerator` `chemotaxis-bifurcation-lean/chemotaxisbifurcation-moderootcrossing-physical-mode-local-same-sign-of-even-rootmultiplicity` `chemotaxis-bifurcation-lean/chemotaxisbifurcation-moderootcrossing-physical-mode-local-sign-change-of-odd-rootmultiplicity` `chemotaxis-bifurcation-lean/chemotaxisbifurcation-oddrootcrossing-physical-coefficient-local-same-sign-of-even-rootmultiplicity` `chemotaxis-bifurcation-lean/chemotaxisbifurcation-oddrootcrossing-physical-coefficient-local-sign-change-of-odd-rootmultiplicity` `chemotaxis-bifurcation-lean/chemotaxisbifurcation-physicalpolynomial-logisticbetacoefficient-eq-paperratio` `chemotaxis-bifurcation-lean/chemotaxisbifurcation-physicalpolynomial-natdegree-paperbalancednumeratorpoly-le` `chemotaxis-bifurcation-lean/chemotaxisbifurcation-physicalpolynomial-natdegree-papernumeratorpoly-le` `chemotaxis-bifurcation-lean/chemotaxisbifurcation-physicalpolynomial-paperdenominatorpoly-eval-pos` `chemotaxis-bifurcation-lean/chemotaxisbifurcation-rationalcoefficient-logisticbetacoefficient-eq-numerator-div-denominator`	`ChemotaxisBifurcation.CoefficientLimits.denominator_ne_zero_at_balancing` `ChemotaxisBifurcation.CoefficientLimits.eventually_neg_at_critical_small_domain` `ChemotaxisBifurcation.CoefficientLimits.eventually_neg_of_large_domain_limit` `ChemotaxisBifurcation.CoefficientLimits.eventually_pos_at_critical_small_domain` `ChemotaxisBifurcation.CoefficientLimits.eventually_pos_of_large_domain_limit` `ChemotaxisBifurcation.CoefficientLimits.physical_critical_coefficient_sub_first_mode_tendsto_small_domain` `ChemotaxisBifurcation.CoefficientLimits.physical_critical_coefficient_tendsto_atBot_of_scriptP_neg` `ChemotaxisBifurcation.CoefficientLimits.physical_critical_coefficient_tendsto_atBot_small_domain` `ChemotaxisBifurcation.CoefficientLimits.physical_critical_coefficient_tendsto_atTop_small_domain` `ChemotaxisBifurcation.CoefficientLimits.physical_critical_coefficient_tendsto_large_domain` `ChemotaxisBifurcation.CoefficientLimits.physical_critical_coefficient_tendsto_small_domain` `ChemotaxisBifurcation.CoefficientLimits.physical_critical_coefficient_tendsto_small_domain_of_D_pos` `ChemotaxisBifurcation.DomainLimits.physical_critical_eigenvalue_tendsto_balancing` `ChemotaxisBifurcation.ModeExamples.beta_nineteen_tenths_higher_modes_negative` `ChemotaxisBifurcation.ModeExamples.beta_three_halves_higher_modes_negative` `ChemotaxisBifurcation.ModeRootCounts.actual_balanced_zero_lengths_card_le_four` `ChemotaxisBifurcation.ModeRootCounts.actual_zero_lengths_card_le_five` `ChemotaxisBifurcation.ModeRootCrossing.physical_coefficient_zero_of_zero_numerator` `ChemotaxisBifurcation.ModeRootCrossing.physical_mode_local_same_sign_of_even_rootMultiplicity` `ChemotaxisBifurcation.ModeRootCrossing.physical_mode_local_sign_change_of_odd_rootMultiplicity` `ChemotaxisBifurcation.OddRootCrossing.physical_coefficient_local_same_sign_of_even_rootMultiplicity` `ChemotaxisBifurcation.OddRootCrossing.physical_coefficient_local_sign_change_of_odd_rootMultiplicity` `ChemotaxisBifurcation.PhysicalPolynomial.logisticBetaCoefficient_eq_paperRatio` `ChemotaxisBifurcation.PhysicalPolynomial.natDegree_paperBalancedNumeratorPoly_le` `ChemotaxisBifurcation.PhysicalPolynomial.natDegree_paperNumeratorPoly_le` `ChemotaxisBifurcation.PhysicalPolynomial.paperDenominatorPoly_eval_pos` `ChemotaxisBifurcation.RationalCoefficient.logisticBetaCoefficient_eq_numerator_div_denominator`	verified verified verified verified verified verified verified verified verified verified verified verified verified verified verified verified verified verified verified verified verified verified verified verified verified verified verified	identification of the non-minimal reduced cubic coefficient with E:beta-n0 its quadratic graph and cubic assembly formulas E:a_0,i, E:a_k,i>0, and E:Gamma-n0-explicit	V2 scope: The all-parameter physical rational formula, degree/cancellation bounds, admissible mode corridors, roots, limits, and finite sign consequences are proved. Excluded tie bifurcations and PDE branch/stability conclusions are not classified. Source locator: p. 8, TeX line 699.
Remark 1.1(1)	Reduction to the scalar ODE for u_n0	Inputs supplied	`chemotaxis-bifurcation-lean/chemotaxisbifurcation-mixedremainder-reducedfield` `chemotaxis-bifurcation-lean/chemotaxisbifurcation-mixedremainder-mixed-equilibrium-core` `chemotaxis-bifurcation-lean/chemotaxisbifurcation-mixedremainder-mixed-parameter-le-amp-sq` `chemotaxis-bifurcation-lean/chemotaxisbifurcation-mixedremainder-mixed-value-bound-absorbed` `chemotaxis-bifurcation-lean/chemotaxisbifurcation-mixedremainder-mixed-deriv-bound-absorbed` `chemotaxis-bifurcation-lean/chemotaxisbifurcation-mixedremainder-mixed-branch-eventually` `chemotaxis-bifurcation-lean/chemotaxisbifurcation-mixedremainder-mixed-side-condition-eventually` `chemotaxis-bifurcation-lean/chemotaxisbifurcation-mixedremainder-exists-pos-equilibrium` `chemotaxis-bifurcation-lean/chemotaxisbifurcation-mixedremainder-branchsmall-eventually` `chemotaxis-bifurcation-lean/chemotaxisbifurcation-mixedremainder-branchsmall` `chemotaxis-bifurcation-lean/chemotaxisbifurcation-mixedremainder-ampconst` `chemotaxis-bifurcation-lean/chemotaxisbifurcation-mixedremainder-absorbedconst` `chemotaxis-bifurcation-lean/chemotaxisbifurcation-mixedremainder-center-ode-final-value-bound-weak` `chemotaxis-bifurcation-lean/chemotaxisbifurcation-mixedremainder-center-ode-final-deriv-bound-weak` `chemotaxis-bifurcation-lean/chemotaxisbifurcation-normalform-paper-equilibrium-core` `chemotaxis-bifurcation-lean/chemotaxisbifurcation-remainderaxis-model-final-interface` `chemotaxis-bifurcation-lean/chemotaxisbifurcation-remainderaxis-model-branch-curves`	`ChemotaxisBifurcation.MixedRemainder.reducedField` `ChemotaxisBifurcation.MixedRemainder.mixed_equilibrium_core` `ChemotaxisBifurcation.MixedRemainder.mixed_parameter_le_amp_sq` `ChemotaxisBifurcation.MixedRemainder.mixed_value_bound_absorbed` `ChemotaxisBifurcation.MixedRemainder.mixed_deriv_bound_absorbed` `ChemotaxisBifurcation.MixedRemainder.mixed_branch_eventually` `ChemotaxisBifurcation.MixedRemainder.mixed_side_condition_eventually` `ChemotaxisBifurcation.MixedRemainder.exists_pos_equilibrium` `ChemotaxisBifurcation.MixedRemainder.branchSmall_eventually` `ChemotaxisBifurcation.MixedRemainder.BranchSmall` `ChemotaxisBifurcation.MixedRemainder.ampConst` `ChemotaxisBifurcation.MixedRemainder.absorbedConst` `ChemotaxisBifurcation.MixedRemainder.center_ODE_final_value_bound_weak` `ChemotaxisBifurcation.MixedRemainder.center_ODE_final_deriv_bound_weak` `ChemotaxisBifurcation.NormalForm.paper_equilibrium_core` `ChemotaxisBifurcation.RemainderAxis.model_final_interface` `ChemotaxisBifurcation.RemainderAxis.model_branch_curves`	verified verified verified verified verified verified verified verified verified verified verified verified verified verified verified verified verified	identification of the minimal-model scalar equation and its coefficients, including the fixed-mass reduction α>0 and β≠0 fixed C≥0 and 0<r≤1 uniform weak mixed value bound on \|η\|,\|s\|≤r differentiability in s and the uniform weak derivative bound for the full mapped scalar interface For the stronger v2 value and derivative bounds: C4 reduced-field JetHyp and exact TrivialBranchLinearization in the physical Fourier amplitude and original time coordinate.	V2 scope: scalar zero exclusion, sign, local branches and stronger value/derivative remainder estimates from the explicit reduced equation, C4 jets and exact trivial-branch linearization. The actual fixed-mass PDE reduction and PDE spectral stability remain inputs. Source locator: p. 7, TeX line 638. arXiv v2: Step 4’ of the proof drops the derivative remainder sentence (ledger arxiv_v2_note).
Theorem 1.3	Extension of the local bifurcation branches	Outside this formalization	—	—	—	—	V2 scope: Requires unilateral global bifurcation, compactness, and PDE a priori theory. Source locator: p. 10, TeX line 933.
Theorem 1.4	Spike-like stationary solutions	Same assumptions	`chemotaxis-bifurcation-lean/chemotaxisbifurcation-classicalspikeblowup-minimal-gradient-blowup` `chemotaxis-bifurcation-lean/chemotaxisbifurcation-classicalspikeblowup-logistic-gradient-blowup-of-eventual-peak` `chemotaxis-bifurcation-lean/chemotaxisbifurcation-classicalspikeblowup-logistic-spike-all-tests-of-eventual-peak`	`ChemotaxisBifurcation.ClassicalSpikeBlowup.minimal_gradient_blowup` `ChemotaxisBifurcation.ClassicalSpikeBlowup.logistic_gradient_blowup_of_eventual_peak` `ChemotaxisBifurcation.ClassicalSpikeBlowup.logistic_spike_all_tests_of_eventual_peak`	verified verified verified	—	Exact public scope, hypotheses and exclusions: data/public-scope-ledger.json, row paper3/T:spiky-solu-thm. This display summary does not extend that scope. Source locator: p. 11, TeX line 991.
Remark 1.3(2)	No Dirac mass in the non-minimal model	Same assumptions	`chemotaxis-bifurcation-lean/chemotaxisbifurcation-stationarymassidentity-classicalprofile-window-mass-bounds` `chemotaxis-bifurcation-lean/chemotaxisbifurcation-stationarymassidentity-window-mass-decay-of-classical-profiles` `chemotaxis-bifurcation-lean/chemotaxisbifurcation-stationarymassidentity-no-atoms-of-classical-profiles` `chemotaxis-bifurcation-lean/chemotaxisbifurcation-stationarymassidentity-no-dirac-subsequence-of-classical-profiles`	`ChemotaxisBifurcation.StationaryMassIdentity.ClassicalProfile.window_mass_bounds` `ChemotaxisBifurcation.StationaryMassIdentity.window_mass_decay_of_classical_profiles` `ChemotaxisBifurcation.StationaryMassIdentity.no_atoms_of_classical_profiles` `ChemotaxisBifurcation.StationaryMassIdentity.no_dirac_subsequence_of_classical_profiles`	verified verified verified verified	—	Exact public scope, hypotheses and exclusions: data/public-scope-ledger.json, row paper3/R:no-delta-concentration. This display summary does not extend that scope. Source locator: p. 11, TeX line 1019.
Proposition 1.2	Consistency of thresholds	Same assumptions	`chemotaxis-bifurcation-lean/chemotaxisbifurcation-semidiscrete-chistar-eq-physical-modethreshold` `chemotaxis-bifurcation-lean/chemotaxisbifurcation-semidiscrete-continuumcritical-eq-finite` `chemotaxis-bifurcation-lean/chemotaxisbifurcation-semidiscrete-critical-threshold-tendsto-of-finite-cutoff` `chemotaxis-bifurcation-lean/chemotaxisbifurcation-semidiscrete-discarg-mem-icc` `chemotaxis-bifurcation-lean/chemotaxisbifurcation-semidiscrete-discarg-one-le` `chemotaxis-bifurcation-lean/chemotaxisbifurcation-semidiscrete-discarg-tendsto-zero` `chemotaxis-bifurcation-lean/chemotaxisbifurcation-semidiscrete-disclam-eq-continuum-mul-sinc-sq` `chemotaxis-bifurcation-lean/chemotaxisbifurcation-semidiscrete-disclam-lower-bound` `chemotaxis-bifurcation-lean/chemotaxisbifurcation-semidiscrete-disclam-one-le` `chemotaxis-bifurcation-lean/chemotaxisbifurcation-semidiscrete-disclam-tendsto-continuum` `chemotaxis-bifurcation-lean/chemotaxisbifurcation-semidiscrete-discretecritical-tendsto-continuumcritical` `chemotaxis-bifurcation-lean/chemotaxisbifurcation-semidiscrete-exists-quadratic-tail` `chemotaxis-bifurcation-lean/chemotaxisbifurcation-semidiscrete-exists-uniform-continuum-tail` `chemotaxis-bifurcation-lean/chemotaxisbifurcation-semidiscrete-exists-uniform-discrete-tail` `chemotaxis-bifurcation-lean/chemotaxisbifurcation-semidiscrete-finite-infimum-eq-of-tail` `chemotaxis-bifurcation-lean/chemotaxisbifurcation-semidiscrete-finite-mode-minimum-tendsto` `chemotaxis-bifurcation-lean/chemotaxisbifurcation-semidiscrete-fixedmass-discretecritical-tendsto` `chemotaxis-bifurcation-lean/chemotaxisbifurcation-semidiscrete-logistic-discretecritical-tendsto` `chemotaxis-bifurcation-lean/chemotaxisbifurcation-semidiscrete-minimaldiscthreshold-isleast` `chemotaxis-bifurcation-lean/chemotaxisbifurcation-semidiscrete-minimaldiscthreshold-one-le` `chemotaxis-bifurcation-lean/chemotaxisbifurcation-semidiscrete-minimaldiscthreshold-tendsto` `chemotaxis-bifurcation-lean/chemotaxisbifurcation-semidiscrete-modethreshold-disc-tendsto` `chemotaxis-bifurcation-lean/chemotaxisbifurcation-semidiscrete-physicalprefactor-eq-inv-thresholdk` `chemotaxis-bifurcation-lean/chemotaxisbifurcation-semidiscrete-physicalprefactor-pos` `chemotaxis-bifurcation-lean/chemotaxisbifurcation-semidiscrete-positivemodes-nonempty` `chemotaxis-bifurcation-lean/chemotaxisbifurcation-semidiscrete-threshold-lower-bound`	`ChemotaxisBifurcation.Semidiscrete.chiStar_eq_physical_modeThreshold` `ChemotaxisBifurcation.Semidiscrete.continuumCritical_eq_finite` `ChemotaxisBifurcation.Semidiscrete.critical_threshold_tendsto_of_finite_cutoff` `ChemotaxisBifurcation.Semidiscrete.discArg_mem_Icc` `ChemotaxisBifurcation.Semidiscrete.discArg_one_le` `ChemotaxisBifurcation.Semidiscrete.discArg_tendsto_zero` `ChemotaxisBifurcation.Semidiscrete.discLam_eq_continuum_mul_sinc_sq` `ChemotaxisBifurcation.Semidiscrete.discLam_lower_bound` `ChemotaxisBifurcation.Semidiscrete.discLam_one_le` `ChemotaxisBifurcation.Semidiscrete.discLam_tendsto_continuum` `ChemotaxisBifurcation.Semidiscrete.discreteCritical_tendsto_continuumCritical` `ChemotaxisBifurcation.Semidiscrete.exists_quadratic_tail` `ChemotaxisBifurcation.Semidiscrete.exists_uniform_continuum_tail` `ChemotaxisBifurcation.Semidiscrete.exists_uniform_discrete_tail` `ChemotaxisBifurcation.Semidiscrete.finite_infimum_eq_of_tail` `ChemotaxisBifurcation.Semidiscrete.finite_mode_minimum_tendsto` `ChemotaxisBifurcation.Semidiscrete.fixedMass_discreteCritical_tendsto` `ChemotaxisBifurcation.Semidiscrete.logistic_discreteCritical_tendsto` `ChemotaxisBifurcation.Semidiscrete.minimalDiscThreshold_isLeast` `ChemotaxisBifurcation.Semidiscrete.minimalDiscThreshold_one_le` `ChemotaxisBifurcation.Semidiscrete.minimalDiscThreshold_tendsto` `ChemotaxisBifurcation.Semidiscrete.modeThreshold_disc_tendsto` `ChemotaxisBifurcation.Semidiscrete.physicalPrefactor_eq_inv_thresholdK` `ChemotaxisBifurcation.Semidiscrete.physicalPrefactor_pos` `ChemotaxisBifurcation.Semidiscrete.positiveModes_nonempty` `ChemotaxisBifurcation.Semidiscrete.threshold_lower_bound`	verified verified verified verified verified verified verified verified verified verified verified verified verified verified verified verified verified verified verified verified verified verified verified verified verified verified	—	V2 scope: The discrete eigenvalue/threshold functions, changing-mode minima, physical identification, and convergence are proved together with the concrete scheme-to-modal bridge. No semidiscrete trajectory existence or nonlinear stability theorem is asserted. Source locator: p. 12, TeX line 1110.
Equation (1.24)	Eigenvalues of the discrete Neumann Laplacian (corrected: of -Delta_h)	Same assumptions	`chemotaxis-bifurcation-lean/chemotaxisbifurcation-discreteeigenmodes-cos-step-identity` `chemotaxis-bifurcation-lean/chemotaxisbifurcation-discreteeigenmodes-cos-reflected-right-identity` `chemotaxis-bifurcation-lean/chemotaxisbifurcation-discreteeigenmodes-reflectedneglaplacian-cosine-eigenpair` `chemotaxis-bifurcation-lean/chemotaxisbifurcation-discreteeigenmodes-discretecosinemode-ne-zero` `chemotaxis-bifurcation-lean/chemotaxisbifurcation-discreteeigenmodes-disclam-strictmono-on-represented` `chemotaxis-bifurcation-lean/chemotaxisbifurcation-discreteeigenmodes-disclam-injective-on-grid` `chemotaxis-bifurcation-lean/chemotaxisbifurcation-discreteeigenmodes-discretecosinemode-haseigenvector` `chemotaxis-bifurcation-lean/chemotaxisbifurcation-discreteeigenmodes-discretecosinemodes-linearindependent` `chemotaxis-bifurcation-lean/chemotaxisbifurcation-discreteeigenmodes-discretecosinemode-exhaustion`	`ChemotaxisBifurcation.DiscreteEigenmodes.cos_step_identity` `ChemotaxisBifurcation.DiscreteEigenmodes.cos_reflected_right_identity` `ChemotaxisBifurcation.DiscreteEigenmodes.reflectedNegLaplacian_cosine_eigenpair` `ChemotaxisBifurcation.DiscreteEigenmodes.discreteCosineMode_ne_zero` `ChemotaxisBifurcation.DiscreteEigenmodes.discLam_strictMono_on_represented` `ChemotaxisBifurcation.DiscreteEigenmodes.discLam_injective_on_grid` `ChemotaxisBifurcation.DiscreteEigenmodes.discreteCosineMode_hasEigenvector` `ChemotaxisBifurcation.DiscreteEigenmodes.discreteCosineModes_linearIndependent` `ChemotaxisBifurcation.DiscreteEigenmodes.discreteCosineMode_exhaustion`	verified verified verified verified verified verified verified verified verified	—	Verified for the corrected statement: Equation 1.24 read with -Delta_h (eigenvalues 4 h^-2 sin^2(n pi/(2N)), n=0..N, of the reflected Neumann stencil). Source locator: p. 12, TeX line 1075.
Equation (6.1)	Semidiscrete scheme for the non-minimal model	Same assumptions	`chemotaxis-bifurcation-lean/chemotaxisbifurcation-discretelinearization-conservativefaceflux-directionalderivative` `chemotaxis-bifurcation-lean/chemotaxisbifurcation-discretelinearization-conservativenoderate-directionalderivative` `chemotaxis-bifurcation-lean/chemotaxisbifurcation-discretelinearization-conservativenoderate-directionalderivative-eq-populationresidual-fixedmass` `chemotaxis-bifurcation-lean/chemotaxisbifurcation-discretelinearization-conservative-coupled-mode-directionalderivative` `chemotaxis-bifurcation-lean/chemotaxisbifurcation-discretelinearization-discretecritical-eq-physical-threshold-min` `chemotaxis-bifurcation-lean/chemotaxisbifurcation-discretelinearization-discrete-coupled-mode-residuals` `chemotaxis-bifurcation-lean/chemotaxisbifurcation-discretelinearization-discrete-growth-eq-physical-modalgrowth` `chemotaxis-bifurcation-lean/chemotaxisbifurcation-discretelinearization-discrete-growth-eq-zero-iff-threshold` `chemotaxis-bifurcation-lean/chemotaxisbifurcation-discretelinearization-expandedellipticnode-directionalderivative` `chemotaxis-bifurcation-lean/chemotaxisbifurcation-discretelinearization-expandedpopulationnode-directionalderivative` `chemotaxis-bifurcation-lean/chemotaxisbifurcation-discretelinearization-expandedpopulationnode-directionalderivative-eq-populationresidual` `chemotaxis-bifurcation-lean/chemotaxisbifurcation-discretelinearization-fixedmass-logisticslope-eq-zero` `chemotaxis-bifurcation-lean/chemotaxisbifurcation-discretelinearization-linearizedconservativenoderate-eq-populationresidual-fixedmass` `chemotaxis-bifurcation-lean/chemotaxisbifurcation-discretelinearization-linearizedconservativenoderate-eq-populationresidual-of-slope-zero` `chemotaxis-bifurcation-lean/chemotaxisbifurcation-discretelinearization-linearizedconservativenoderate-eq-reflected` `chemotaxis-bifurcation-lean/chemotaxisbifurcation-discretelinearization-represented-disclam-pos`	`ChemotaxisBifurcation.DiscreteLinearization.conservativeFaceFlux_directionalDerivative` `ChemotaxisBifurcation.DiscreteLinearization.conservativeNodeRate_directionalDerivative` `ChemotaxisBifurcation.DiscreteLinearization.conservativeNodeRate_directionalDerivative_eq_populationResidual_fixedMass` `ChemotaxisBifurcation.DiscreteLinearization.conservative_coupled_mode_directionalDerivative` `ChemotaxisBifurcation.DiscreteLinearization.discreteCritical_eq_physical_threshold_min` `ChemotaxisBifurcation.DiscreteLinearization.discrete_coupled_mode_residuals` `ChemotaxisBifurcation.DiscreteLinearization.discrete_growth_eq_physical_modalGrowth` `ChemotaxisBifurcation.DiscreteLinearization.discrete_growth_eq_zero_iff_threshold` `ChemotaxisBifurcation.DiscreteLinearization.expandedEllipticNode_directionalDerivative` `ChemotaxisBifurcation.DiscreteLinearization.expandedPopulationNode_directionalDerivative` `ChemotaxisBifurcation.DiscreteLinearization.expandedPopulationNode_directionalDerivative_eq_populationResidual` `ChemotaxisBifurcation.DiscreteLinearization.fixedMass_logisticSlope_eq_zero` `ChemotaxisBifurcation.DiscreteLinearization.linearizedConservativeNodeRate_eq_populationResidual_fixedMass` `ChemotaxisBifurcation.DiscreteLinearization.linearizedConservativeNodeRate_eq_populationResidual_of_slope_zero` `ChemotaxisBifurcation.DiscreteLinearization.linearizedConservativeNodeRate_eq_reflected` `ChemotaxisBifurcation.DiscreteLinearization.represented_discLam_pos`	verified verified verified verified verified verified verified verified verified verified verified verified verified verified verified verified	—	V2 scope: Directional derivatives of both literal schemes, the conservative all-node identity, fixed-mass composition, elliptic elimination, modal growth, and threshold minimum are proved. No ODE trajectory existence, nonlinear stability, or PDE semigroup conclusion is asserted. Source locator: p. 36, TeX line 3328.
Lemma 2.1, Equations 2.1-2.4	Integrals of products of cosine series	Same assumptions	`chemotaxis-bifurcation-lean/chemotaxisbifurcation-trigintegrals-cosine-sine-sine` `chemotaxis-bifurcation-lean/chemotaxisbifurcation-trigintegrals-two-cosines-two-sines` `chemotaxis-bifurcation-lean/chemotaxisbifurcation-trigintegrals-cos-cos-cos` `chemotaxis-bifurcation-lean/chemotaxisbifurcation-trigintegrals-cos-cos-cos-cos` `chemotaxis-bifurcation-lean/chemotaxisbifurcation-trigintegrals-cosine-sine-sine-lp` `chemotaxis-bifurcation-lean/chemotaxisbifurcation-trigintegrals-two-cosines-two-sines-lp` `chemotaxis-bifurcation-lean/chemotaxisbifurcation-trigintegrals-cos-cos-cos-lp` `chemotaxis-bifurcation-lean/chemotaxisbifurcation-trigintegrals-cos-cos-cos-cos-lp` `chemotaxis-bifurcation-lean/chemotaxisbifurcation-trigintegrals-kernel-cos-sin-sin` `chemotaxis-bifurcation-lean/chemotaxisbifurcation-trigintegrals-kernel-cos-cos-sin-sin` `chemotaxis-bifurcation-lean/chemotaxisbifurcation-trigintegrals-kernel-cos-cos-cos` `chemotaxis-bifurcation-lean/chemotaxisbifurcation-trigintegrals-kernel-cos-cos-cos-cos` `chemotaxis-bifurcation-lean/chemotaxisbifurcation-fourierkernels-integral-cos-sin-sin` `chemotaxis-bifurcation-lean/chemotaxisbifurcation-fourierkernels-integral-cos-cos-cos` `chemotaxis-bifurcation-lean/chemotaxisbifurcation-fourierkernels-integral-cos-cos-sin-sin` `chemotaxis-bifurcation-lean/chemotaxisbifurcation-fourierkernels-integral-cos-cos-cos-cos` `chemotaxis-bifurcation-lean/chemotaxisbifurcation-fourierkernels-integral-cos-sin-sin-signed` `chemotaxis-bifurcation-lean/chemotaxisbifurcation-fourierkernels-integral-cos-cos-cos-signed` `chemotaxis-bifurcation-lean/chemotaxisbifurcation-fourierkernels-integral-cos-cos-sin-sin-signed` `chemotaxis-bifurcation-lean/chemotaxisbifurcation-fourierkernels-integral-cos-cos-cos-cos-signed` `chemotaxis-bifurcation-lean/chemotaxisbifurcation-fourierkernels-cos-sin-sin-zero-mode-control` `chemotaxis-bifurcation-lean/chemotaxisbifurcation-fourierkernels-cos-cos-cos-zero-mode-control` `chemotaxis-bifurcation-lean/chemotaxisbifurcation-fourierkernels-cos-cos-cos-cos-zero-mode-control` `chemotaxis-bifurcation-lean/chemotaxisbifurcation-fourierkernels-sinephase` `chemotaxis-bifurcation-lean/chemotaxisbifurcation-fourierkernels-intcosphase` `chemotaxis-bifurcation-lean/chemotaxisbifurcation-fourierkernels-ind` `chemotaxis-bifurcation-lean/chemotaxisbifurcation-fourierkernels-integral-intcosphase` `chemotaxis-bifurcation-lean/chemotaxisbifurcation-fourierseriesproducts-tsum-mul-tsum-bounded` `chemotaxis-bifurcation-lean/chemotaxisbifurcation-fourierseriesproducts-summable-norm-mul-bounded` `chemotaxis-bifurcation-lean/chemotaxisbifurcation-fourierseriesproducts-cosineseries-mul-cosineseries` `chemotaxis-bifurcation-lean/chemotaxisbifurcation-fourierseriesproducts-cosineseries-mul-cosineseries-mul-cosineseries` `chemotaxis-bifurcation-lean/chemotaxisbifurcation-fourierseriesproducts-hassum-integral-tsum-mul` `chemotaxis-bifurcation-lean/chemotaxisbifurcation-fourierseriesproducts-hassum-integral-tsum-mul-tsum` `chemotaxis-bifurcation-lean/chemotaxisbifurcation-fourierseriesproducts-hassum-mul-ite` `chemotaxis-bifurcation-lean/chemotaxisbifurcation-fourierseriesproducts-hassum-mul-ite-int-eq` `chemotaxis-bifurcation-lean/chemotaxisbifurcation-fourierseriesproducts-hassum-pair-ite-add-eq-neg` `chemotaxis-bifurcation-lean/chemotaxisbifurcation-fourierseriesproducts-hassum-pair-ite-add-eq-of-neg` `chemotaxis-bifurcation-lean/chemotaxisbifurcation-fourierseriesproducts-hassum-triple-ite-add-add-eq-neg` `chemotaxis-bifurcation-lean/chemotaxisbifurcation-fourierseriesproducts-cosine-sine-sine-of-kernel` `chemotaxis-bifurcation-lean/chemotaxisbifurcation-fourierseriesproducts-two-cosines-two-sines-of-kernel` `chemotaxis-bifurcation-lean/chemotaxisbifurcation-fourierseriesproducts-cos-cos-cos-of-kernel` `chemotaxis-bifurcation-lean/chemotaxisbifurcation-fourierseriesproducts-cos-cos-cos-cos-of-kernel` `chemotaxis-bifurcation-lean/chemotaxisbifurcation-fourierseriesproducts-summable-norm-of-lp-one` `chemotaxis-bifurcation-lean/chemotaxisbifurcation-infinitecosineprojection-hassum-intervalintegral-boundedphase` `chemotaxis-bifurcation-lean/chemotaxisbifurcation-infinitecosineprojection-cosinephase`	`ChemotaxisBifurcation.TrigIntegrals.cosine_sine_sine` `ChemotaxisBifurcation.TrigIntegrals.two_cosines_two_sines` `ChemotaxisBifurcation.TrigIntegrals.cos_cos_cos` `ChemotaxisBifurcation.TrigIntegrals.cos_cos_cos_cos` `ChemotaxisBifurcation.TrigIntegrals.cosine_sine_sine_lp` `ChemotaxisBifurcation.TrigIntegrals.two_cosines_two_sines_lp` `ChemotaxisBifurcation.TrigIntegrals.cos_cos_cos_lp` `ChemotaxisBifurcation.TrigIntegrals.cos_cos_cos_cos_lp` `ChemotaxisBifurcation.TrigIntegrals.kernel_cos_sin_sin` `ChemotaxisBifurcation.TrigIntegrals.kernel_cos_cos_sin_sin` `ChemotaxisBifurcation.TrigIntegrals.kernel_cos_cos_cos` `ChemotaxisBifurcation.TrigIntegrals.kernel_cos_cos_cos_cos` `ChemotaxisBifurcation.FourierKernels.integral_cos_sin_sin` `ChemotaxisBifurcation.FourierKernels.integral_cos_cos_cos` `ChemotaxisBifurcation.FourierKernels.integral_cos_cos_sin_sin` `ChemotaxisBifurcation.FourierKernels.integral_cos_cos_cos_cos` `ChemotaxisBifurcation.FourierKernels.integral_cos_sin_sin_signed` `ChemotaxisBifurcation.FourierKernels.integral_cos_cos_cos_signed` `ChemotaxisBifurcation.FourierKernels.integral_cos_cos_sin_sin_signed` `ChemotaxisBifurcation.FourierKernels.integral_cos_cos_cos_cos_signed` `ChemotaxisBifurcation.FourierKernels.cos_sin_sin_zero_mode_control` `ChemotaxisBifurcation.FourierKernels.cos_cos_cos_zero_mode_control` `ChemotaxisBifurcation.FourierKernels.cos_cos_cos_cos_zero_mode_control` `ChemotaxisBifurcation.FourierKernels.sinePhase` `ChemotaxisBifurcation.FourierKernels.intCosPhase` `ChemotaxisBifurcation.FourierKernels.ind` `ChemotaxisBifurcation.FourierKernels.integral_intCosPhase` `ChemotaxisBifurcation.FourierSeriesProducts.tsum_mul_tsum_bounded` `ChemotaxisBifurcation.FourierSeriesProducts.summable_norm_mul_bounded` `ChemotaxisBifurcation.FourierSeriesProducts.cosineSeries_mul_cosineSeries` `ChemotaxisBifurcation.FourierSeriesProducts.cosineSeries_mul_cosineSeries_mul_cosineSeries` `ChemotaxisBifurcation.FourierSeriesProducts.hasSum_integral_tsum_mul` `ChemotaxisBifurcation.FourierSeriesProducts.hasSum_integral_tsum_mul_tsum` `ChemotaxisBifurcation.FourierSeriesProducts.hasSum_mul_ite` `ChemotaxisBifurcation.FourierSeriesProducts.hasSum_mul_ite_int_eq` `ChemotaxisBifurcation.FourierSeriesProducts.hasSum_pair_ite_add_eq_neg` `ChemotaxisBifurcation.FourierSeriesProducts.hasSum_pair_ite_add_eq_of_neg` `ChemotaxisBifurcation.FourierSeriesProducts.hasSum_triple_ite_add_add_eq_neg` `ChemotaxisBifurcation.FourierSeriesProducts.cosine_sine_sine_of_kernel` `ChemotaxisBifurcation.FourierSeriesProducts.two_cosines_two_sines_of_kernel` `ChemotaxisBifurcation.FourierSeriesProducts.cos_cos_cos_of_kernel` `ChemotaxisBifurcation.FourierSeriesProducts.cos_cos_cos_cos_of_kernel` `ChemotaxisBifurcation.FourierSeriesProducts.summable_norm_of_lp_one` `ChemotaxisBifurcation.InfiniteCosineProjection.hasSum_intervalIntegral_boundedPhase` `ChemotaxisBifurcation.InfiniteCosineProjection.cosinePhase`	verified verified verified verified verified verified verified verified verified verified verified verified verified verified verified verified verified verified verified verified verified verified verified verified verified verified verified verified verified verified verified verified verified verified verified verified verified verified verified verified verified verified verified verified verified	—	V2 scope: Current scope is finite identities only; the former ell-one infinite-series lemma is a different statement. Source locator: p. 13, TeX line 1153.
Equation (2.16)	Centre manifold as a graph over the critical mode	Outside this formalization	—	—	—	—	V2 scope: The center graph is an analytic input to conditional finite-jet theorems. Source locator: p. 15, TeX line 1389.
Equation (2.8)	Mobility coefficients B_0, B_u, B_v	Same assumptions	`chemotaxis-bifurcation-lean/chemotaxisbifurcation-mobilityinu-derivative-value` `chemotaxis-bifurcation-lean/chemotaxisbifurcation-mobilityinu-hasderivat` `chemotaxis-bifurcation-lean/chemotaxisbifurcation-mobilityinu-hasderivat-normalized` `chemotaxis-bifurcation-lean/chemotaxisbifurcation-mobilityinv-hasderivat` `chemotaxis-bifurcation-lean/chemotaxisbifurcation-mobilityinw-derivative-value` `chemotaxis-bifurcation-lean/chemotaxisbifurcation-mobilityinw-hasderivat` `chemotaxis-bifurcation-lean/chemotaxisbifurcation-mobilityinw-hasderivat-normalized` `chemotaxis-bifurcation-lean/chemotaxisbifurcation-rawcubicprojectiondata-taylor-fields` `chemotaxis-bifurcation-lean/chemotaxisbifurcation-coefficientdictionary-b0-bu-bv-eq`	`ChemotaxisBifurcation.mobilityInU_derivative_value` `ChemotaxisBifurcation.mobilityInU_hasDerivAt` `ChemotaxisBifurcation.mobilityInU_hasDerivAt_normalized` `ChemotaxisBifurcation.mobilityInV_hasDerivAt` `ChemotaxisBifurcation.mobilityInW_derivative_value` `ChemotaxisBifurcation.mobilityInW_hasDerivAt` `ChemotaxisBifurcation.mobilityInW_hasDerivAt_normalized` `ChemotaxisBifurcation.rawCubicProjectionData_taylor_fields` `ChemotaxisBifurcation.CoefficientDictionary.B0_Bu_Bv_eq`	verified verified verified verified verified verified verified verified verified	—	V2 scope: The retained declarations are the derivative formulas of the mobility from which B0, Bu and Bv follow at (u, 1+v); the formulas are identical with the same positive-base domain. Their later infinite-mode use does not change the primitive derivative types. Source locator: p. 14, TeX line 1285.
Equation (2.9)	Mobility coefficients B_uu, B_uv, B_vv	Same assumptions	`chemotaxis-bifurcation-lean/chemotaxisbifurcation-mobilityinu-deriv-hasderivat` `chemotaxis-bifurcation-lean/chemotaxisbifurcation-mobilityinu-second-derivative-value` `chemotaxis-bifurcation-lean/chemotaxisbifurcation-mobilityinu-second-hasderivat` `chemotaxis-bifurcation-lean/chemotaxisbifurcation-mobilityinw-deriv-hasderivat` `chemotaxis-bifurcation-lean/chemotaxisbifurcation-mobilityinw-second-derivative-value` `chemotaxis-bifurcation-lean/chemotaxisbifurcation-mobilityinw-second-hasderivat` `chemotaxis-bifurcation-lean/chemotaxisbifurcation-mobility-mixed-deriv-hasderivat` `chemotaxis-bifurcation-lean/chemotaxisbifurcation-mobility-mixed-derivative-value` `chemotaxis-bifurcation-lean/chemotaxisbifurcation-mobility-mixed-hasderivat` `chemotaxis-bifurcation-lean/chemotaxisbifurcation-rawcubicprojectiondata-taylor-fields`	`ChemotaxisBifurcation.mobilityInU_deriv_hasDerivAt` `ChemotaxisBifurcation.mobilityInU_second_derivative_value` `ChemotaxisBifurcation.mobilityInU_second_hasDerivAt` `ChemotaxisBifurcation.mobilityInW_deriv_hasDerivAt` `ChemotaxisBifurcation.mobilityInW_second_derivative_value` `ChemotaxisBifurcation.mobilityInW_second_hasDerivAt` `ChemotaxisBifurcation.mobility_mixed_deriv_hasDerivAt` `ChemotaxisBifurcation.mobility_mixed_derivative_value` `ChemotaxisBifurcation.mobility_mixed_hasDerivAt` `ChemotaxisBifurcation.rawCubicProjectionData_taylor_fields`	verified verified verified verified verified verified verified verified verified verified	—	V2 scope: The factorial-normalized Buu, Buv and Bvv formulas and positive-base hypotheses are unchanged. Source locator: p. 14, TeX line 1289.
Equation (2.10)	Logistic coefficients A’, A’’, A’’’	Same assumptions	`chemotaxis-bifurcation-lean/chemotaxisbifurcation-baprime-eq-logisticslope` `chemotaxis-bifurcation-lean/chemotaxisbifurcation-normalizedlogisticfirst-hasderivat` `chemotaxis-bifurcation-lean/chemotaxisbifurcation-normalizedlogisticsecond-hasderivat` `chemotaxis-bifurcation-lean/chemotaxisbifurcation-normalizedlogistic-deriv-eq-first` `chemotaxis-bifurcation-lean/chemotaxisbifurcation-normalizedlogistic-hasderivat` `chemotaxis-bifurcation-lean/chemotaxisbifurcation-rawtaylor-logistic-coefficients`	`ChemotaxisBifurcation.bAprime_eq_logisticSlope` `ChemotaxisBifurcation.normalizedLogisticFirst_hasDerivAt` `ChemotaxisBifurcation.normalizedLogisticSecond_hasDerivAt` `ChemotaxisBifurcation.normalizedLogistic_deriv_eq_first` `ChemotaxisBifurcation.normalizedLogistic_hasDerivAt` `ChemotaxisBifurcation.rawTaylor_logistic_coefficients`	verified verified verified verified verified verified	—	V2 scope: A-prime, A-second and A-third retain the same factorial convention (Taylor coefficients of the logistic source at u*). Source locator: p. 14, TeX line 1291.
Equation (2.11)	Signal-source coefficients C’, C’’, C’’’	Same assumptions	`chemotaxis-bifurcation-lean/chemotaxisbifurcation-rawtaylor-signal-coefficients` `chemotaxis-bifurcation-lean/chemotaxisbifurcation-signalsourcefirst-hasderivat` `chemotaxis-bifurcation-lean/chemotaxisbifurcation-signalsourcesecond-hasderivat` `chemotaxis-bifurcation-lean/chemotaxisbifurcation-signalsource-deriv-eq-first`	`ChemotaxisBifurcation.rawTaylor_signal_coefficients` `ChemotaxisBifurcation.signalSourceFirst_hasDerivAt` `ChemotaxisBifurcation.signalSourceSecond_hasDerivAt` `ChemotaxisBifurcation.signalSource_deriv_eq_first`	verified verified verified verified	—	V2 scope: The three signal-source Taylor coefficients are formula-identical and retain the same factorial normalization. Source locator: p. 14, TeX line 1298.
Equation (2.20)	Signal coefficients C_k^(1), C_k^(2), C_k^(3)	Same assumptions	`chemotaxis-bifurcation-lean/chemotaxisbifurcation-signalmode1-residual` `chemotaxis-bifurcation-lean/chemotaxisbifurcation-signalmode2-residual` `chemotaxis-bifurcation-lean/chemotaxisbifurcation-signalmode3-residual` `chemotaxis-bifurcation-lean/chemotaxisbifurcation-signalresponsejet-actual-response-quartic` `chemotaxis-bifurcation-lean/chemotaxisbifurcation-signalresponsejet-actual-response-hasderivat` `chemotaxis-bifurcation-lean/chemotaxisbifurcation-signalresponsejet-actual-response-cubic-jet` `chemotaxis-bifurcation-lean/chemotaxisbifurcation-signalresponsejetinterface-actual-modal-derivative`	`ChemotaxisBifurcation.signalMode1_residual` `ChemotaxisBifurcation.signalMode2_residual` `ChemotaxisBifurcation.signalMode3_residual` `ChemotaxisBifurcation.SignalResponseJet.actual_response_quartic` `ChemotaxisBifurcation.SignalResponseJet.actual_response_hasDerivAt` `ChemotaxisBifurcation.SignalResponseJet.actual_response_cubic_jet` `ChemotaxisBifurcation.SignalResponseJetInterface.actual_modal_derivative`	verified verified verified verified verified verified verified	—	Exact public scope, hypotheses and exclusions: data/public-scope-ledger.json, row paper3/E:Ck-restated. This display summary does not extend that scope. Source locator: p. 16, TeX line 1482.
Equation (2.32)	Quadratic coefficient Gamma_{2 n0}	Inputs supplied	`chemotaxis-bifurcation-lean/chemotaxisbifurcation-quadraticprojectiondata-flux-decomposition` `chemotaxis-bifurcation-lean/chemotaxisbifurcation-quadraticprojectiondata-neg-deriv-flux` `chemotaxis-bifurcation-lean/chemotaxisbifurcation-chigamma2-eq-projected` `chemotaxis-bifurcation-lean/chemotaxisbifurcation-normalized-quadratic-density-projection` `chemotaxis-bifurcation-lean/chemotaxisbifurcation-quadraticprojection-bracket-eq-scaled`	`ChemotaxisBifurcation.QuadraticProjectionData.flux_decomposition` `ChemotaxisBifurcation.QuadraticProjectionData.neg_deriv_flux` `ChemotaxisBifurcation.chiGamma2_eq_projected` `ChemotaxisBifurcation.normalized_quadratic_density_projection` `ChemotaxisBifurcation.quadraticProjection_bracket_eq_scaled`	verified verified verified verified verified	audited primitive Taylor coefficients and quadratic elliptic signal jet positive equilibrium with signal equilibrium relation and nu,gamma>0 L>0 and n0>0 with x=lambda_n0	V2 scope: The displayed second-harmonic coefficient is identical. Current infinite convolution formulas reduce at quadratic center order to the same constant/second-mode support; no infinite-series theorem is claimed by this row. Source locator: p. 19, TeX line 1828.
Equation (2.33)	Constant-mode coefficients a_{0,1}, a_{0,2}	Inputs supplied	`chemotaxis-bifurcation-lean/chemotaxisbifurcation-constantmodejet-a-0-display` `chemotaxis-bifurcation-lean/chemotaxisbifurcation-constantmodejet-constantmode-coefficients` `chemotaxis-bifurcation-lean/chemotaxisbifurcation-constantmodejet-logistica0-eq-explicit` `chemotaxis-bifurcation-lean/chemotaxisbifurcation-a0-eq-zero-of-mean-zero` `chemotaxis-bifurcation-lean/chemotaxisbifurcation-average-quadraticjetprofile` `chemotaxis-bifurcation-lean/chemotaxisbifurcation-coefficients-of-quadratic-jet-residual` `chemotaxis-bifurcation-lean/chemotaxisbifurcation-fixedmassa0-eq-zero` `chemotaxis-bifurcation-lean/chemotaxisbifurcation-logistica0` `chemotaxis-bifurcation-lean/chemotaxisbifurcation-logistica0-physical-residual` `chemotaxis-bifurcation-lean/chemotaxisbifurcation-logistica0-residual` `chemotaxis-bifurcation-lean/chemotaxisbifurcation-quadraticjetresidual` `chemotaxis-bifurcation-lean/chemotaxisbifurcation-weakh2meanjet-quadratic-constant-zero`	`ChemotaxisBifurcation.ConstantModeJet.a_0_display` `ChemotaxisBifurcation.ConstantModeJet.constantMode_coefficients` `ChemotaxisBifurcation.ConstantModeJet.logisticA0_eq_explicit` `ChemotaxisBifurcation.a0_eq_zero_of_mean_zero` `ChemotaxisBifurcation.average_quadraticJetProfile` `ChemotaxisBifurcation.coefficients_of_quadratic_jet_residual` `ChemotaxisBifurcation.fixedMassA0_eq_zero` `ChemotaxisBifurcation.logisticA0` `ChemotaxisBifurcation.logisticA0_physical_residual` `ChemotaxisBifurcation.logisticA0_residual` `ChemotaxisBifurcation.quadraticJetResidual` `ChemotaxisBifurcation.WeakH2MeanJet.quadratic_constant_zero`	verified verified verified verified verified verified verified verified verified verified verified verified	degree-two constant-mode invariance residual obtained from the center-graph equations zero mean of the quadratic graph profile for the separate fixed-mass consumer positive domain length and positive mode index when applying that consumer	Conditional scope retained. Actual cosine complement, curved elliptic cubic response and conserved-mean coefficient extraction supply the scoped ingredients. Family/jet construction, operator identity and global foundations remain explicit. Public scope and supplied inputs: data/public-scope-ledger.json, paper3/E:a_0,i
Equation (2.36b)	Higher-mode coefficients a_{k,1}	Inputs supplied	`chemotaxis-bifurcation-lean/chemotaxisbifurcation-coefficients-of-quadratic-jet-residual` `chemotaxis-bifurcation-lean/chemotaxisbifurcation-integral-neumannmode-positive-zero` `chemotaxis-bifurcation-lean/chemotaxisbifurcation-other-mode-quadratic-coefficient-zero` `chemotaxis-bifurcation-lean/chemotaxisbifurcation-physical-other-quadratic-mode-zero` `chemotaxis-bifurcation-lean/chemotaxisbifurcation-quadraticforcing-other-mode-projection-zero` `chemotaxis-bifurcation-lean/chemotaxisbifurcation-secondmodea2-physical-residual` `chemotaxis-bifurcation-lean/chemotaxisbifurcation-secondmodea2-residual`	`ChemotaxisBifurcation.coefficients_of_quadratic_jet_residual` `ChemotaxisBifurcation.integral_neumannMode_positive_zero` `ChemotaxisBifurcation.other_mode_quadratic_coefficient_zero` `ChemotaxisBifurcation.physical_other_quadratic_mode_zero` `ChemotaxisBifurcation.quadraticForcing_other_mode_projection_zero` `ChemotaxisBifurcation.secondModeA2_physical_residual` `ChemotaxisBifurcation.secondModeA2_residual`	verified verified verified verified verified verified verified	vanishing degree-two center-graph invariance polynomial and projected stable-mode balances audited quadratic forcing and physical coefficient identification positive physical parameters and equilibrium relations unique strict critical mode, supplying nonzero stable growth rates, particularly sigma_(2n0)	V2 scope: The bA’‘/2 term is mandatory. Any legacy wrapper omitting it is rejected. Source locator: p. 20, TeX line 1893.
Equation (2.42)	Auxiliary quantities F, G, H	Inputs supplied	`chemotaxis-bifurcation-lean/chemotaxisbifurcation-h-eq-of-projected-signal-balance` `chemotaxis-bifurcation-lean/chemotaxisbifurcation-rationalcoefficient-physical-e` `chemotaxis-bifurcation-lean/chemotaxisbifurcation-rationalcoefficient-physical-f` `chemotaxis-bifurcation-lean/chemotaxisbifurcation-rationalcoefficient-physical-g` `chemotaxis-bifurcation-lean/chemotaxisbifurcation-rationalcoefficient-physical-h` `chemotaxis-bifurcation-lean/chemotaxisbifurcation-rationalcoefficient-physical-q` `chemotaxis-bifurcation-lean/chemotaxisbifurcation-rationalcoefficient-physical-r` `chemotaxis-bifurcation-lean/chemotaxisbifurcation-rationalcoefficient-physical-s` `chemotaxis-bifurcation-lean/chemotaxisbifurcation-cubicdata` `chemotaxis-bifurcation-lean/chemotaxisbifurcation-cubice` `chemotaxis-bifurcation-lean/chemotaxisbifurcation-cubicf` `chemotaxis-bifurcation-lean/chemotaxisbifurcation-cubicg` `chemotaxis-bifurcation-lean/chemotaxisbifurcation-cubich` `chemotaxis-bifurcation-lean/chemotaxisbifurcation-cubich-eq-of-projected-signal-balance` `chemotaxis-bifurcation-lean/chemotaxisbifurcation-cubicqoverb0` `chemotaxis-bifurcation-lean/chemotaxisbifurcation-cubicroverb0` `chemotaxis-bifurcation-lean/chemotaxisbifurcation-cubicsoverb0` `chemotaxis-bifurcation-lean/chemotaxisbifurcation-curvedsignalresponse-actual-residual-cubic-negligible` `chemotaxis-bifurcation-lean/chemotaxisbifurcation-curvedsignalresponse-profile-power-jets` `chemotaxis-bifurcation-lean/chemotaxisbifurcation-curvedsignalresponse-profileprojection` `chemotaxis-bifurcation-lean/chemotaxisbifurcation-curvedsignalresponse-projected-source-jet` `chemotaxis-bifurcation-lean/chemotaxisbifurcation-curvedsignalresponse-profileprojection-eq` `chemotaxis-bifurcation-lean/chemotaxisbifurcation-curvedsignalresponse-family-isbigo-linear` `chemotaxis-bifurcation-lean/chemotaxisbifurcation-curvedsignalresponse-profileprojection-eq-cosinecoeff` `chemotaxis-bifurcation-lean/chemotaxisbifurcation-curvedsignalresponse-actual-profile-response-jet` `chemotaxis-bifurcation-lean/chemotaxisbifurcation-curvedsignalresponse-profile-cosine-square-zero` `chemotaxis-bifurcation-lean/chemotaxisbifurcation-curvedsignalresponse-actual-phase-cubic-response`	`ChemotaxisBifurcation.H_eq_of_projected_signal_balance` `ChemotaxisBifurcation.RationalCoefficient.physical_E` `ChemotaxisBifurcation.RationalCoefficient.physical_F` `ChemotaxisBifurcation.RationalCoefficient.physical_G` `ChemotaxisBifurcation.RationalCoefficient.physical_H` `ChemotaxisBifurcation.RationalCoefficient.physical_Q` `ChemotaxisBifurcation.RationalCoefficient.physical_R` `ChemotaxisBifurcation.RationalCoefficient.physical_S` `ChemotaxisBifurcation.cubicData` `ChemotaxisBifurcation.cubicE` `ChemotaxisBifurcation.cubicF` `ChemotaxisBifurcation.cubicG` `ChemotaxisBifurcation.cubicH` `ChemotaxisBifurcation.cubicH_eq_of_projected_signal_balance` `ChemotaxisBifurcation.cubicQOverB0` `ChemotaxisBifurcation.cubicROverB0` `ChemotaxisBifurcation.cubicSOverB0` `ChemotaxisBifurcation.CurvedSignalResponse.actual_residual_cubic_negligible` `ChemotaxisBifurcation.CurvedSignalResponse.profile_power_jets` `ChemotaxisBifurcation.CurvedSignalResponse.profileProjection` `ChemotaxisBifurcation.CurvedSignalResponse.projected_source_jet` `ChemotaxisBifurcation.CurvedSignalResponse.profileProjection_eq` `ChemotaxisBifurcation.CurvedSignalResponse.family_isBigO_linear` `ChemotaxisBifurcation.CurvedSignalResponse.profileProjection_eq_cosineCoeff` `ChemotaxisBifurcation.CurvedSignalResponse.actual_profile_response_jet` `ChemotaxisBifurcation.CurvedSignalResponse.profile_cosine_square_zero` `ChemotaxisBifurcation.CurvedSignalResponse.actual_phase_cubic_response`	verified verified verified verified verified verified verified verified verified verified verified verified verified verified verified verified verified verified verified verified verified verified verified verified verified verified verified	projected cubic elliptic signal balance weighted interval integrability of h3φₙ, (φh2)φₙ, and φ³φₙ zero critical projection of h3 identification of φ and h2 with the critical cosine and quadratic graph profile giving Π(φh2)=a0+a2/2 and Π(φ³)=3/4 physical signal-equilibrium relation and positive parameters for the scaled-to-physical identification	Conditional scope retained. Actual cosine complement, curved elliptic cubic response and conserved-mean coefficient extraction supply the scoped ingredients. Family/jet construction, operator identity and global foundations remain explicit. Public scope and supplied inputs: data/public-scope-ledger.json, paper3/E:E-F-G-H
Equation (2.41)	Cubic coefficient Gamma_{n0}^(3)	Inputs supplied	`chemotaxis-bifurcation-lean/chemotaxisbifurcation-rawcubicprojectiondata-flux-decomposition` `chemotaxis-bifurcation-lean/chemotaxisbifurcation-rawcubicprojectiondata-neg-deriv-flux` `chemotaxis-bifurcation-lean/chemotaxisbifurcation-actualcriticalprojection-add-of-intervalintegrable` `chemotaxis-bifurcation-lean/chemotaxisbifurcation-actual-phi-cube-projection` `chemotaxis-bifurcation-lean/chemotaxisbifurcation-actual-phi-quadraticjet-projection` `chemotaxis-bifurcation-lean/chemotaxisbifurcation-chigamma3-eq-projected` `chemotaxis-bifurcation-lean/chemotaxisbifurcation-cubicfluxcoefficient-eq-rawflux` `chemotaxis-bifurcation-lean/chemotaxisbifurcation-normalized-cubic-density-projection` `chemotaxis-bifurcation-lean/chemotaxisbifurcation-rawcubic-criticalbracket-eq-scaled` `chemotaxis-bifurcation-lean/chemotaxisbifurcation-signalcubicsource-actual-projection-of-intervalintegrable`	`ChemotaxisBifurcation.RawCubicProjectionData.flux_decomposition` `ChemotaxisBifurcation.RawCubicProjectionData.neg_deriv_flux` `ChemotaxisBifurcation.actualCriticalProjection_add_of_intervalIntegrable` `ChemotaxisBifurcation.actual_phi_cube_projection` `ChemotaxisBifurcation.actual_phi_quadraticJet_projection` `ChemotaxisBifurcation.chiGamma3_eq_projected` `ChemotaxisBifurcation.cubicFluxCoefficient_eq_rawFlux` `ChemotaxisBifurcation.normalized_cubic_density_projection` `ChemotaxisBifurcation.rawCubic_criticalBracket_eq_scaled` `ChemotaxisBifurcation.signalCubicSource_actual_projection_of_intervalIntegrable`	verified verified verified verified verified verified verified verified verified verified	audited primitive and quadratic-jet coefficients and elliptic signal aggregates projected cubic elliptic balance with nonzero denominator weighted interval integrability of h3, phih2 and phi^3 against the critical mode zero critical projection of h3 identification phi=cos(n0pix/L) and h2=a0+a2cos(2n0pi*x/L) positive physical equilibrium and L>0,n0>0	V2 scope: Conditional on weighted interval integrability and the analytic center-graph condition that the critical projection of h3 is zero; all remaining cubic extraction/projection algebra is proved. Source locator: p. 20, TeX line 1938.
Equation (2.44)	Crossing coefficient alpha_n0	Same assumptions	`chemotaxis-bifurcation-lean/chemotaxisbifurcation-crossingcoefficient-alphan0-eq-explicit` `chemotaxis-bifurcation-lean/chemotaxisbifurcation-crossingcoefficient-alpha-n0-display` `chemotaxis-bifurcation-lean/chemotaxisbifurcation-crossingcoefficient-deriv-modalgrowth-at-chistar` `chemotaxis-bifurcation-lean/chemotaxisbifurcation-crossingcoefficient-hasderivat-modalgrowth-chi` `chemotaxis-bifurcation-lean/chemotaxisbifurcation-crossingcoefficient-modalgrowth-eq-affine` `chemotaxis-bifurcation-lean/chemotaxisbifurcation-physicalmodeguards-alphan0-pos` `chemotaxis-bifurcation-lean/chemotaxisbifurcation-physicalmodeguards-chistartimesb0-pos` `chemotaxis-bifurcation-lean/chemotaxisbifurcation-physicalmodeguards-signalmode1-pos`	`ChemotaxisBifurcation.CrossingCoefficient.alphaN0_eq_explicit` `ChemotaxisBifurcation.CrossingCoefficient.alpha_n0_display` `ChemotaxisBifurcation.CrossingCoefficient.deriv_modalGrowth_at_chiStar` `ChemotaxisBifurcation.CrossingCoefficient.hasDerivAt_modalGrowth_chi` `ChemotaxisBifurcation.CrossingCoefficient.modalGrowth_eq_affine` `ChemotaxisBifurcation.PhysicalModeGuards.alphaN0_pos` `ChemotaxisBifurcation.PhysicalModeGuards.chiStarTimesB0_pos` `ChemotaxisBifurcation.PhysicalModeGuards.signalMode1_pos`	verified verified verified verified verified verified verified verified	—	V2 scope: The linear crossing coefficient and positivity hypotheses are unchanged. Source locator: p. 21, TeX line 1969.
Equation (2.45)	Cubic coefficient beta_n0	Inputs supplied	`chemotaxis-bifurcation-lean/chemotaxisbifurcation-betacoefficient-eq-physical-projected` `chemotaxis-bifurcation-lean/chemotaxisbifurcation-betacoefficient-eq-projected` `chemotaxis-bifurcation-lean/chemotaxisbifurcation-logisticbetacoefficient-eq-physical-projected`	`ChemotaxisBifurcation.betaCoefficient_eq_physical_projected` `ChemotaxisBifurcation.betaCoefficient_eq_projected` `ChemotaxisBifurcation.logisticBetaCoefficient_eq_physical_projected`	verified verified verified	accepted quadratic center jet and cubic critical projection, including their analytic application inputs positive physical equilibrium satisfying logistic and signal equilibrium relations nonzero critical eigenvalue and valid stable-mode denominators when identifying the jet with the center graph	V2 scope: The corrected finite cubic assembly is derived from the accepted quadratic and cubic projection components. It proves the coefficient identity, not center-manifold or PDE branch existence. Source locator: p. 21, TeX line 1979.
Equation (2.43)	Reduced equation on the centre manifold	Inputs supplied	`chemotaxis-bifurcation-lean/chemotaxisbifurcation-mixedremainder-center-ode-final-value-bound-weak` `chemotaxis-bifurcation-lean/chemotaxisbifurcation-mixedremainder-center-ode-final-deriv-bound-weak` `chemotaxis-bifurcation-lean/chemotaxisbifurcation-mixedremainder-center-ode-final-equilibrium-core` `chemotaxis-bifurcation-lean/chemotaxisbifurcation-mixedremainder-center-ode-final-branch-eventually` `chemotaxis-bifurcation-lean/chemotaxisbifurcation-mixedremainder-reducedfield` `chemotaxis-bifurcation-lean/chemotaxisbifurcation-mixedremainder-mixed-equilibrium-core` `chemotaxis-bifurcation-lean/chemotaxisbifurcation-mixedremainder-mixed-parameter-le-amp-sq` `chemotaxis-bifurcation-lean/chemotaxisbifurcation-mixedremainder-mixed-value-bound-absorbed` `chemotaxis-bifurcation-lean/chemotaxisbifurcation-mixedremainder-mixed-deriv-bound-absorbed` `chemotaxis-bifurcation-lean/chemotaxisbifurcation-mixedremainder-mixed-branch-eventually` `chemotaxis-bifurcation-lean/chemotaxisbifurcation-mixedremainder-mixed-side-condition-eventually` `chemotaxis-bifurcation-lean/chemotaxisbifurcation-mixedremainder-exists-pos-equilibrium` `chemotaxis-bifurcation-lean/chemotaxisbifurcation-mixedremainder-branchsmall-eventually` `chemotaxis-bifurcation-lean/chemotaxisbifurcation-mixedremainder-branchsmall` `chemotaxis-bifurcation-lean/chemotaxisbifurcation-mixedremainder-ampconst` `chemotaxis-bifurcation-lean/chemotaxisbifurcation-mixedremainder-absorbedconst` `chemotaxis-bifurcation-lean/chemotaxisbifurcation-normalform-paper-equilibrium-core` `chemotaxis-bifurcation-lean/chemotaxisbifurcation-branchderivativeasymptotic-branch-derivative-error-bound` `chemotaxis-bifurcation-lean/chemotaxisbifurcation-branchderivativeasymptotic-branch-derivative-islittleo`	`ChemotaxisBifurcation.MixedRemainder.center_ODE_final_value_bound_weak` `ChemotaxisBifurcation.MixedRemainder.center_ODE_final_deriv_bound_weak` `ChemotaxisBifurcation.MixedRemainder.center_ODE_final_equilibrium_core` `ChemotaxisBifurcation.MixedRemainder.center_ODE_final_branch_eventually` `ChemotaxisBifurcation.MixedRemainder.reducedField` `ChemotaxisBifurcation.MixedRemainder.mixed_equilibrium_core` `ChemotaxisBifurcation.MixedRemainder.mixed_parameter_le_amp_sq` `ChemotaxisBifurcation.MixedRemainder.mixed_value_bound_absorbed` `ChemotaxisBifurcation.MixedRemainder.mixed_deriv_bound_absorbed` `ChemotaxisBifurcation.MixedRemainder.mixed_branch_eventually` `ChemotaxisBifurcation.MixedRemainder.mixed_side_condition_eventually` `ChemotaxisBifurcation.MixedRemainder.exists_pos_equilibrium` `ChemotaxisBifurcation.MixedRemainder.branchSmall_eventually` `ChemotaxisBifurcation.MixedRemainder.BranchSmall` `ChemotaxisBifurcation.MixedRemainder.ampConst` `ChemotaxisBifurcation.MixedRemainder.absorbedConst` `ChemotaxisBifurcation.NormalForm.paper_equilibrium_core` `ChemotaxisBifurcation.BranchDerivativeAsymptotic.branch_derivative_error_bound` `ChemotaxisBifurcation.BranchDerivativeAsymptotic.branch_derivative_isLittleO`	verified verified verified verified verified verified verified verified verified verified verified verified verified verified verified verified verified verified verified	identification of the reduced field with Eq. 2.43 α>0 and β≠0 fixed C≥0 and 0<r≤1 uniform bound \|R(η,s)\|≤C(s²η²+\|s\|³\|η\|+s⁴) on the local box HasDerivAt (R η) (Rs η s) s there separate uniform bound \|Rs(η,s)\|≤C(\|s\|η²+s²\|η\|+\|s\|³)	V2 scope: Only the exact cubic polynomial and deductions from an explicit remainder interface are formalized. The actual scalar BranchCurves branches also satisfy derivative = -2 alpha eta + o(\|eta\|) along the correct branch-side filter, derived from the remainder estimates and amplitude localization. Source locator: p. 20, TeX line 1961.
Equation (2.49)	beta_n0 in the minimal model	Inputs supplied	`chemotaxis-bifurcation-lean/chemotaxisbifurcation-fixedmassa0-eq-zero` `chemotaxis-bifurcation-lean/chemotaxisbifurcation-fixedmassbetacoefficient-eq-neg-chigamma3`	`ChemotaxisBifurcation.fixedMassA0_eq_zero` `ChemotaxisBifurcation.fixedMassBetaCoefficient_eq_neg_chiGamma3`	verified verified	fixed-mass phase-space identification of the population constant correction with zero a=b=0 and positive signal equilibrium audited fixed-mass quadratic jet and cubic projection, including their analytic application inputs and nonzero modal denominators	V2 scope: The fixed-mass coefficient remains -chi-star Gamma3 with a0=0 and no logistic channels. The constant signal correction is still retained. Source locator: p. 22, TeX line 2148.
Equation (3.1)	beta_n0 in terms of p(beta) and q(beta)	Inputs supplied	`chemotaxis-bifurcation-lean/chemotaxisbifurcation-betadecomposition-betacoefficientata0-eq-pq` `chemotaxis-bifurcation-lean/chemotaxisbifurcation-betadecomposition-pterm-eq-affine` `chemotaxis-bifurcation-lean/chemotaxisbifurcation-betadecomposition-qterm-eq-quadratic` `chemotaxis-bifurcation-lean/chemotaxisbifurcation-physicalmodeguards-physical-pi-eq-scaled` `chemotaxis-bifurcation-lean/chemotaxisbifurcation-betaleading-eq-manuscript-pi` `chemotaxis-bifurcation-lean/chemotaxisbifurcation-upow-mul-piscaled` `chemotaxis-bifurcation-lean/chemotaxisbifurcation-coefficientdictionary-beta-n0-pq-logistic` `chemotaxis-bifurcation-lean/chemotaxisbifurcation-coefficientdictionary-logistica0-eq-233` `chemotaxis-bifurcation-lean/chemotaxisbifurcation-coefficientdictionary-beta-n0-pq-fixedmass`	`ChemotaxisBifurcation.BetaDecomposition.betaCoefficientAtA0_eq_pq` `ChemotaxisBifurcation.BetaDecomposition.pTerm_eq_affine` `ChemotaxisBifurcation.BetaDecomposition.qTerm_eq_quadratic` `ChemotaxisBifurcation.PhysicalModeGuards.physical_Pi_eq_scaled` `ChemotaxisBifurcation.betaLeading_eq_manuscript_Pi` `ChemotaxisBifurcation.uPow_mul_PiScaled` `ChemotaxisBifurcation.CoefficientDictionary.beta_n0_pq_logistic` `ChemotaxisBifurcation.CoefficientDictionary.logisticA0_eq_233` `ChemotaxisBifurcation.CoefficientDictionary.beta_n0_pq_fixedMass`	verified verified verified verified verified verified verified verified verified	audited identification of the assembled cubic coefficient with the reduced-equation coefficient quadratic graph coefficient formulas and the model-appropriate constant mode positive equilibrium relations and strict critical-mode guards supplied in the surrounding manuscript	V2 scope: The p(beta), q(beta), beta-independent Pi and coefficient decomposition are unchanged after movement to Section 3. Source locator: p. 23, TeX line 2200.
Equation (3.3)	Coefficients A, B, C of the quadratic in beta	Same assumptions	`chemotaxis-bifurcation-lean/chemotaxisbifurcation-betadecomposition-betaconstant-eq-pq-at-zero` `chemotaxis-bifurcation-lean/chemotaxisbifurcation-betadecomposition-betaleading-eq-neg-half-q-second` `chemotaxis-bifurcation-lean/chemotaxisbifurcation-betadecomposition-betalinear-eq-ba2-mul-p-deriv-sub-q-deriv` `chemotaxis-bifurcation-lean/chemotaxisbifurcation-betadecomposition-deriv-pterm-zero` `chemotaxis-bifurcation-lean/chemotaxisbifurcation-betadecomposition-deriv-qterm-zero` `chemotaxis-bifurcation-lean/chemotaxisbifurcation-betadecomposition-iterderiv-two-qterm-zero`	`ChemotaxisBifurcation.BetaDecomposition.betaConstant_eq_pq_at_zero` `ChemotaxisBifurcation.BetaDecomposition.betaLeading_eq_neg_half_q_second` `ChemotaxisBifurcation.BetaDecomposition.betaLinear_eq_bA2_mul_p_deriv_sub_q_deriv` `ChemotaxisBifurcation.BetaDecomposition.deriv_pTerm_zero` `ChemotaxisBifurcation.BetaDecomposition.deriv_qTerm_zero` `ChemotaxisBifurcation.BetaDecomposition.iterDeriv_two_qTerm_zero`	verified verified verified verified verified verified	—	V2 scope: The exact derivative formulas A=-q’‘(0)/2, B=bA’‘p’(0)-q’(0), and C at beta=0 are unchanged. Source locator: p. 23, TeX line 2248.
Equation (3.4)	Closed form of the leading coefficient A	Same assumptions	`chemotaxis-bifurcation-lean/chemotaxisbifurcation-betaleading-eq-manuscript` `chemotaxis-bifurcation-lean/chemotaxisbifurcation-betaleading-eq-manuscript-pi` `chemotaxis-bifurcation-lean/chemotaxisbifurcation-betaleading-neg` `chemotaxis-bifurcation-lean/chemotaxisbifurcation-physicalbetaa-neg` `chemotaxis-bifurcation-lean/chemotaxisbifurcation-upow-mul-piscaled` `chemotaxis-bifurcation-lean/chemotaxisbifurcation-coefficientdictionary-physicalbetaa-neg-fixedmass`	`ChemotaxisBifurcation.betaLeading_eq_manuscript` `ChemotaxisBifurcation.betaLeading_eq_manuscript_Pi` `ChemotaxisBifurcation.betaLeading_neg` `ChemotaxisBifurcation.physicalBetaA_neg` `ChemotaxisBifurcation.uPow_mul_PiScaled` `ChemotaxisBifurcation.CoefficientDictionary.physicalBetaA_neg_fixedMass`	verified verified verified verified verified verified	—	V2 scope: The closed form and strict negative sign under a strict critical mode are unchanged for both model classes. Source locator: p. 23, TeX line 2267.
Equation (1.15)	beta_n0 = P(lambda_n0)/Q(lambda_n0)	Same assumptions	`chemotaxis-bifurcation-lean/chemotaxisbifurcation-minimalrational-fixedmassbetacoefficient-eq-cubic-ratio` `chemotaxis-bifurcation-lean/chemotaxisbifurcation-minimalrational-fixedmass-eq-logistic` `chemotaxis-bifurcation-lean/chemotaxisbifurcation-minimalrational-minimalnumeratorpoly` `chemotaxis-bifurcation-lean/chemotaxisbifurcation-minimalrational-natdegree-minimalnumeratorpoly-le` `chemotaxis-bifurcation-lean/chemotaxisbifurcation-physicalpolynomial-logisticbetacoefficient-eq-paperratio` `chemotaxis-bifurcation-lean/chemotaxisbifurcation-physicalpolynomial-natdegree-paperbalancednumeratorpoly-le` `chemotaxis-bifurcation-lean/chemotaxisbifurcation-physicalpolynomial-natdegree-papernumeratorpoly-le` `chemotaxis-bifurcation-lean/chemotaxisbifurcation-physicalpolynomial-paperdenominatorpoly-eval-pos` `chemotaxis-bifurcation-lean/chemotaxisbifurcation-polynomialdegree-rationaldata-balanced-ratio-eq` `chemotaxis-bifurcation-lean/chemotaxisbifurcation-polynomialdegree-rationaldata-denominatorpoly-eq-ppoly-mul-balanced` `chemotaxis-bifurcation-lean/chemotaxisbifurcation-polynomialdegree-rationaldata-eval-denominatorpoly` `chemotaxis-bifurcation-lean/chemotaxisbifurcation-polynomialdegree-rationaldata-eval-numeratorpoly` `chemotaxis-bifurcation-lean/chemotaxisbifurcation-polynomialdegree-rationaldata-natdegree-balanceddenominatorpoly-le` `chemotaxis-bifurcation-lean/chemotaxisbifurcation-polynomialdegree-rationaldata-natdegree-balancednumeratorpoly-le` `chemotaxis-bifurcation-lean/chemotaxisbifurcation-polynomialdegree-rationaldata-natdegree-denominatorpoly-le` `chemotaxis-bifurcation-lean/chemotaxisbifurcation-polynomialdegree-rationaldata-natdegree-numeratorpoly-le` `chemotaxis-bifurcation-lean/chemotaxisbifurcation-polynomialdegree-rationaldata-numeratorpoly-eq-ppoly-mul-balanced` `chemotaxis-bifurcation-lean/chemotaxisbifurcation-rationalcoefficient-rationaldata-coefficient-eq-numerator-div-denominator` `chemotaxis-bifurcation-lean/chemotaxisbifurcation-rationalcoefficient-rationaldata-denominator-pos` `chemotaxis-bifurcation-lean/chemotaxisbifurcation-rationalcoefficient-logisticbetacoefficient-eq-numerator-div-denominator` `chemotaxis-bifurcation-lean/chemotaxisbifurcation-rationalcoefficient-logisticbetacoefficient-eq-symbolic` `chemotaxis-bifurcation-lean/chemotaxisbifurcation-rationalcoefficient-physical-g` `chemotaxis-bifurcation-lean/chemotaxisbifurcation-rationalcoefficient-physical-h` `chemotaxis-bifurcation-lean/chemotaxisbifurcation-rationalcoefficient-physical-q` `chemotaxis-bifurcation-lean/chemotaxisbifurcation-rationalcoefficient-physical-r` `chemotaxis-bifurcation-lean/chemotaxisbifurcation-rationalcoefficient-physical-s` `chemotaxis-bifurcation-lean/chemotaxisbifurcation-rationalcoefficient-physical-a2` `chemotaxis-bifurcation-lean/chemotaxisbifurcation-rationalcoefficient-physical-chigamma2` `chemotaxis-bifurcation-lean/chemotaxisbifurcation-rationalcoefficient-physical-chigamma3`	`ChemotaxisBifurcation.MinimalRational.fixedMassBetaCoefficient_eq_cubic_ratio` `ChemotaxisBifurcation.MinimalRational.fixedMass_eq_logistic` `ChemotaxisBifurcation.MinimalRational.minimalNumeratorPoly` `ChemotaxisBifurcation.MinimalRational.natDegree_minimalNumeratorPoly_le` `ChemotaxisBifurcation.PhysicalPolynomial.logisticBetaCoefficient_eq_paperRatio` `ChemotaxisBifurcation.PhysicalPolynomial.natDegree_paperBalancedNumeratorPoly_le` `ChemotaxisBifurcation.PhysicalPolynomial.natDegree_paperNumeratorPoly_le` `ChemotaxisBifurcation.PhysicalPolynomial.paperDenominatorPoly_eval_pos` `ChemotaxisBifurcation.PolynomialDegree.RationalData.balanced_ratio_eq` `ChemotaxisBifurcation.PolynomialDegree.RationalData.denominatorPoly_eq_pPoly_mul_balanced` `ChemotaxisBifurcation.PolynomialDegree.RationalData.eval_denominatorPoly` `ChemotaxisBifurcation.PolynomialDegree.RationalData.eval_numeratorPoly` `ChemotaxisBifurcation.PolynomialDegree.RationalData.natDegree_balancedDenominatorPoly_le` `ChemotaxisBifurcation.PolynomialDegree.RationalData.natDegree_balancedNumeratorPoly_le` `ChemotaxisBifurcation.PolynomialDegree.RationalData.natDegree_denominatorPoly_le` `ChemotaxisBifurcation.PolynomialDegree.RationalData.natDegree_numeratorPoly_le` `ChemotaxisBifurcation.PolynomialDegree.RationalData.numeratorPoly_eq_pPoly_mul_balanced` `ChemotaxisBifurcation.RationalCoefficient.RationalData.coefficient_eq_numerator_div_denominator` `ChemotaxisBifurcation.RationalCoefficient.RationalData.denominator_pos` `ChemotaxisBifurcation.RationalCoefficient.logisticBetaCoefficient_eq_numerator_div_denominator` `ChemotaxisBifurcation.RationalCoefficient.logisticBetaCoefficient_eq_symbolic` `ChemotaxisBifurcation.RationalCoefficient.physical_G` `ChemotaxisBifurcation.RationalCoefficient.physical_H` `ChemotaxisBifurcation.RationalCoefficient.physical_Q` `ChemotaxisBifurcation.RationalCoefficient.physical_R` `ChemotaxisBifurcation.RationalCoefficient.physical_S` `ChemotaxisBifurcation.RationalCoefficient.physical_a2` `ChemotaxisBifurcation.RationalCoefficient.physical_chiGamma2` `ChemotaxisBifurcation.RationalCoefficient.physical_chiGamma3`	verified verified verified verified verified verified verified verified verified verified verified verified verified verified verified verified verified verified verified verified verified verified verified verified verified verified verified verified verified	—	V2 scope: The general physical numerator/denominator construction, positive denominator, degree-five bound, and balanced degree-four cancellation are proved; the normalized example is only a downstream specialization. Source locator: p. 8, TeX line 731.
Equation (3.6)	Unique minimizing mode on each admissible interval	Same assumptions	`chemotaxis-bifurcation-lean/chemotaxisbifurcation-modeintervals-criticallength-tie-identity` `chemotaxis-bifurcation-lean/chemotaxisbifurcation-modeintervals-modecell-iff-length-interval` `chemotaxis-bifurcation-lean/chemotaxisbifurcation-modeintervals-physical-critical-length-iff` `chemotaxis-bifurcation-lean/chemotaxisbifurcation-modeintervals-tie-at-criticallength` `chemotaxis-bifurcation-lean/chemotaxisbifurcation-modeintervals-tied-adjacent-values` `chemotaxis-bifurcation-lean/chemotaxisbifurcation-modeintervals-tied-minimizers-exact` `chemotaxis-bifurcation-lean/chemotaxisbifurcation-modeintervals-tied-modes-strictly-below-others`	`ChemotaxisBifurcation.ModeIntervals.criticalLength_tie_identity` `ChemotaxisBifurcation.ModeIntervals.modeCell_iff_length_interval` `ChemotaxisBifurcation.ModeIntervals.physical_critical_length_iff` `ChemotaxisBifurcation.ModeIntervals.tie_at_criticalLength` `ChemotaxisBifurcation.ModeIntervals.tied_adjacent_values` `ChemotaxisBifurcation.ModeIntervals.tied_minimizers_exact` `ChemotaxisBifurcation.ModeIntervals.tied_modes_strictly_below_others`	verified verified verified verified verified verified verified	—	V2 scope: The unique minimizing mode cells and exactly two adjacent modes at tie lengths are unchanged. Source locator: p. 26, TeX line 2472.
Theorem 1.2(2), eigenvalue intervals	Interval of lambda_n0 for an admissible length	Same assumptions	`chemotaxis-bifurcation-lean/chemotaxisbifurcation-domainlimits-eigenvalue-tendsto-of-domain-corridor` `chemotaxis-bifurcation-lean/chemotaxisbifurcation-domainlimits-physical-critical-eigenvalue-tendsto-balancing` `chemotaxis-bifurcation-lean/chemotaxisbifurcation-modeintervals-modecell-iff-corridor` `chemotaxis-bifurcation-lean/chemotaxisbifurcation-modeintervals-physical-critical-eigenvalue-corridor-iff` `chemotaxis-bifurcation-lean/chemotaxisbifurcation-modeintervals-physical-critical-lower-corridor` `chemotaxis-bifurcation-lean/chemotaxisbifurcation-modeintervals-physical-critical-upper-corridor` `chemotaxis-bifurcation-lean/chemotaxisbifurcation-modeintervals-physical-realization-iff`	`ChemotaxisBifurcation.DomainLimits.eigenvalue_tendsto_of_domain_corridor` `ChemotaxisBifurcation.DomainLimits.physical_critical_eigenvalue_tendsto_balancing` `ChemotaxisBifurcation.ModeIntervals.modeCell_iff_corridor` `ChemotaxisBifurcation.ModeIntervals.physical_critical_eigenvalue_corridor_iff` `ChemotaxisBifurcation.ModeIntervals.physical_critical_lower_corridor` `ChemotaxisBifurcation.ModeIntervals.physical_critical_upper_corridor` `ChemotaxisBifurcation.ModeIntervals.physical_realization_iff`	verified verified verified verified verified verified verified	—	V2 scope: The exact lambda corridor is unchanged but no longer has its own label; it appears in Theorem 1.2(2) and again in the proof near line 2564. Large-length convergence to sqrt(a alpha mu) is unchanged along admissible lengths. Source locator: p. 8, TeX line 699.
Equation (3.7)	Large-lambda asymptotics of beta_n0 in Example 3.1	Same assumptions	`chemotaxis-bifurcation-lean/chemotaxisbifurcation-normalizedasymptotic-abs-coefficient-sub-linear-le` `chemotaxis-bifurcation-lean/chemotaxisbifurcation-normalizedasymptotic-coefficient-sub-linear` `chemotaxis-bifurcation-lean/chemotaxisbifurcation-normalizedasymptotic-coefficient-sub-linear-isbigo` `chemotaxis-bifurcation-lean/chemotaxisbifurcation-normalizedasymptotic-logisticbetacoefficient-allones-isbigo` `chemotaxis-bifurcation-lean/chemotaxisbifurcation-normalizedasymptotic-numerator-eq-slope-mul-add` `chemotaxis-bifurcation-lean/chemotaxisbifurcation-normalizedasymptotic-remaindernumerator` `chemotaxis-bifurcation-lean/chemotaxisbifurcation-normalizedasymptotic-slope` `chemotaxis-bifurcation-lean/chemotaxisbifurcation-normalizedspecialization-allones-critical-small-domain-limit` `chemotaxis-bifurcation-lean/chemotaxisbifurcation-normalizedspecialization-allones-critical-small-domain-rate` `chemotaxis-bifurcation-lean/chemotaxisbifurcation-normalizedspecialization-betasd-allones` `chemotaxis-bifurcation-lean/chemotaxisbifurcation-normalizedspecialization-csd-allones` `chemotaxis-bifurcation-lean/chemotaxisbifurcation-normalizedspecialization-dbeta-allones` `chemotaxis-bifurcation-lean/chemotaxisbifurcation-normalizedspecialization-dstar-allones` `chemotaxis-bifurcation-lean/chemotaxisbifurcation-normalizedspecialization-logisticbetacoefficient-allones` `chemotaxis-bifurcation-lean/chemotaxisbifurcation-normalizedspecialization-physical-ratio-allones-of-half-lt` `chemotaxis-bifurcation-lean/chemotaxisbifurcation-normalizedspecialization-ratio-allones-of-half-lt` `chemotaxis-bifurcation-lean/chemotaxisbifurcation-specializedpolynomial-coefficient` `chemotaxis-bifurcation-lean/chemotaxisbifurcation-specializedpolynomial-coefficient-neg-of-beta-ge-seven-thirds` `chemotaxis-bifurcation-lean/chemotaxisbifurcation-specializedpolynomial-coefficient-pos-of-beta-mem-icc` `chemotaxis-bifurcation-lean/chemotaxisbifurcation-specializedpolynomial-denominator` `chemotaxis-bifurcation-lean/chemotaxisbifurcation-specializedpolynomial-denominator-pos` `chemotaxis-bifurcation-lean/chemotaxisbifurcation-specializedpolynomial-numerator` `chemotaxis-bifurcation-lean/chemotaxisbifurcation-specializedpolynomial-numerator-neg-of-beta-ge-seven-thirds` `chemotaxis-bifurcation-lean/chemotaxisbifurcation-specializedpolynomial-numerator-pos-of-beta-mem-icc` `chemotaxis-bifurcation-lean/chemotaxisbifurcation-specializedpolynomial-numerator-shift`	`ChemotaxisBifurcation.NormalizedAsymptotic.abs_coefficient_sub_linear_le` `ChemotaxisBifurcation.NormalizedAsymptotic.coefficient_sub_linear` `ChemotaxisBifurcation.NormalizedAsymptotic.coefficient_sub_linear_isBigO` `ChemotaxisBifurcation.NormalizedAsymptotic.logisticBetaCoefficient_allOnes_isBigO` `ChemotaxisBifurcation.NormalizedAsymptotic.numerator_eq_slope_mul_add` `ChemotaxisBifurcation.NormalizedAsymptotic.remainderNumerator` `ChemotaxisBifurcation.NormalizedAsymptotic.slope` `ChemotaxisBifurcation.NormalizedSpecialization.allOnes_critical_small_domain_limit` `ChemotaxisBifurcation.NormalizedSpecialization.allOnes_critical_small_domain_rate` `ChemotaxisBifurcation.NormalizedSpecialization.betaSD_allOnes` `ChemotaxisBifurcation.NormalizedSpecialization.cSD_allOnes` `ChemotaxisBifurcation.NormalizedSpecialization.dBeta_allOnes` `ChemotaxisBifurcation.NormalizedSpecialization.dStar_allOnes` `ChemotaxisBifurcation.NormalizedSpecialization.logisticBetaCoefficient_allOnes` `ChemotaxisBifurcation.NormalizedSpecialization.physical_ratio_allOnes_of_half_lt` `ChemotaxisBifurcation.NormalizedSpecialization.ratio_allOnes_of_half_lt` `ChemotaxisBifurcation.SpecializedPolynomial.coefficient` `ChemotaxisBifurcation.SpecializedPolynomial.coefficient_neg_of_beta_ge_seven_thirds` `ChemotaxisBifurcation.SpecializedPolynomial.coefficient_pos_of_beta_mem_Icc` `ChemotaxisBifurcation.SpecializedPolynomial.denominator` `ChemotaxisBifurcation.SpecializedPolynomial.denominator_pos` `ChemotaxisBifurcation.SpecializedPolynomial.numerator` `ChemotaxisBifurcation.SpecializedPolynomial.numerator_neg_of_beta_ge_seven_thirds` `ChemotaxisBifurcation.SpecializedPolynomial.numerator_pos_of_beta_mem_Icc` `ChemotaxisBifurcation.SpecializedPolynomial.numerator_shift`	verified verified verified verified verified verified verified verified verified verified verified verified verified verified verified verified verified verified verified verified verified verified verified verified verified	—	V2 scope: This is a downstream specialization and regression test, never a replacement for the all-parameter M4 theorem. Source locator: p. 26, TeX line 2543.
Equation (3.8)	Large-domain limit beta_infinity in Example 3.1	Inputs supplied	`chemotaxis-bifurcation-lean/chemotaxisbifurcation-normalizedspecialization-allones-large-domain-limit` `chemotaxis-bifurcation-lean/chemotaxisbifurcation-normalizedspecialization-betalargedomain-rounding-cell` `chemotaxis-bifurcation-lean/chemotaxisbifurcation-specializedpolynomial-betainfinity-eq-zero` `chemotaxis-bifurcation-lean/chemotaxisbifurcation-specializedpolynomial-betainfinity-factor` `chemotaxis-bifurcation-lean/chemotaxisbifurcation-specializedpolynomial-betainfinity-neg-of-gt` `chemotaxis-bifurcation-lean/chemotaxisbifurcation-specializedpolynomial-betainfinity-pos-of-nonneg-of-lt` `chemotaxis-bifurcation-lean/chemotaxisbifurcation-specializedpolynomial-betalargedomainneg-neg` `chemotaxis-bifurcation-lean/chemotaxisbifurcation-specializedpolynomial-betalargedomain-mem-ioo` `chemotaxis-bifurcation-lean/chemotaxisbifurcation-specializedpolynomial-sqrt-21529-sq`	`ChemotaxisBifurcation.NormalizedSpecialization.allOnes_large_domain_limit` `ChemotaxisBifurcation.NormalizedSpecialization.betaLargeDomain_rounding_cell` `ChemotaxisBifurcation.SpecializedPolynomial.betaInfinity_eq_zero` `ChemotaxisBifurcation.SpecializedPolynomial.betaInfinity_factor` `ChemotaxisBifurcation.SpecializedPolynomial.betaInfinity_neg_of_gt` `ChemotaxisBifurcation.SpecializedPolynomial.betaInfinity_pos_of_nonneg_of_lt` `ChemotaxisBifurcation.SpecializedPolynomial.betaLargeDomainNeg_neg` `ChemotaxisBifurcation.SpecializedPolynomial.betaLargeDomain_mem_Ioo` `ChemotaxisBifurcation.SpecializedPolynomial.sqrt_21529_sq`	verified verified verified verified verified verified verified verified verified	the all-ones physical coefficient identification mode data with lengths tending to infinity and eventually strict critical modes β≥0 for the stated nonnegative-parameter sign classification the local bifurcation theorem converting a nonzero cubic-coefficient sign into bifurcation direction	V2 scope: The normalized large-domain quadratic, positive root beta_ld and sign split are unchanged. Source locator: p. 27, TeX line 2550.
Table 3.2	Real roots of P(lambda, beta) for selected beta	Inputs supplied	`chemotaxis-bifurcation-lean/chemotaxisbifurcation-certifiedroots-beta-nineteen-tenths-first-root` `chemotaxis-bifurcation-lean/chemotaxisbifurcation-certifiedroots-beta-nineteen-tenths-second-root` `chemotaxis-bifurcation-lean/chemotaxisbifurcation-certifiedroots-beta-three-halves-first-root` `chemotaxis-bifurcation-lean/chemotaxisbifurcation-certifiedroots-beta-three-halves-second-root` `chemotaxis-bifurcation-lean/chemotaxisbifurcation-modeexamples-beta-nineteen-tenths-higher-modes-negative` `chemotaxis-bifurcation-lean/chemotaxisbifurcation-modeexamples-beta-nineteen-tenths-lower-root-modes` `chemotaxis-bifurcation-lean/chemotaxisbifurcation-modeexamples-beta-nineteen-tenths-mode-one-signs` `chemotaxis-bifurcation-lean/chemotaxisbifurcation-modeexamples-beta-nineteen-tenths-upper-root-modes` `chemotaxis-bifurcation-lean/chemotaxisbifurcation-modeexamples-beta-three-halves-higher-modes-negative` `chemotaxis-bifurcation-lean/chemotaxisbifurcation-modeexamples-beta-three-halves-lower-root-modes` `chemotaxis-bifurcation-lean/chemotaxisbifurcation-modeexamples-beta-three-halves-mode-three-signs` `chemotaxis-bifurcation-lean/chemotaxisbifurcation-modeexamples-beta-three-halves-modes-one-two-signs` `chemotaxis-bifurcation-lean/chemotaxisbifurcation-modeexamples-beta-three-halves-upper-root-modes` `chemotaxis-bifurcation-lean/chemotaxisbifurcation-roottable-beta-nineteen-tenths-physical-signs` `chemotaxis-bifurcation-lean/chemotaxisbifurcation-roottable-beta-nineteen-tenths-rounding-cells` `chemotaxis-bifurcation-lean/chemotaxisbifurcation-roottable-beta-three-halves-physical-signs` `chemotaxis-bifurcation-lean/chemotaxisbifurcation-roottable-beta-three-halves-rounding-cells` `chemotaxis-bifurcation-lean/chemotaxisbifurcation-roottableadmissible-beta-one-no-admissible-root` `chemotaxis-bifurcation-lean/chemotaxisbifurcation-roottableadmissible-beta-seven-thirds-no-admissible-root` `chemotaxis-bifurcation-lean/chemotaxisbifurcation-roottableadmissible-beta-three-no-admissible-root` `chemotaxis-bifurcation-lean/chemotaxisbifurcation-roottableadmissible-beta-twelve-fifths-no-admissible-root` `chemotaxis-bifurcation-lean/chemotaxisbifurcation-roottableadmissible-beta-twenty-one-tenths-unique-admissible-root` `chemotaxis-bifurcation-lean/chemotaxisbifurcation-roottableadmissible-beta-two-unique-admissible-root` `chemotaxis-bifurcation-lean/chemotaxisbifurcation-roottableremaining-beta-seven-thirds-roots-exhaust` `chemotaxis-bifurcation-lean/chemotaxisbifurcation-roottableremaining-beta-twelve-fifths-roots-exhaust` `chemotaxis-bifurcation-lean/chemotaxisbifurcation-roottableremaining-beta-twenty-one-tenths-roots-exhaust` `chemotaxis-bifurcation-lean/chemotaxisbifurcation-roottableremaining-beta-two-roots-exhaust` `chemotaxis-bifurcation-lean/chemotaxisbifurcation-tworootexhaustion-f1-zero-eq-certified-roots` `chemotaxis-bifurcation-lean/chemotaxisbifurcation-tworootexhaustion-f3-zero-eq-certified-roots` `chemotaxis-bifurcation-lean/chemotaxisbifurcation-coefficientdictionary-example-3-1-display` `chemotaxis-bifurcation-lean/chemotaxisbifurcation-roottableaggregate-table-3-2-real-roots` `chemotaxis-bifurcation-lean/chemotaxisbifurcation-roottableaggregate-table-3-2-admissible-roots`	`ChemotaxisBifurcation.CertifiedRoots.beta_nineteen_tenths_first_root` `ChemotaxisBifurcation.CertifiedRoots.beta_nineteen_tenths_second_root` `ChemotaxisBifurcation.CertifiedRoots.beta_three_halves_first_root` `ChemotaxisBifurcation.CertifiedRoots.beta_three_halves_second_root` `ChemotaxisBifurcation.ModeExamples.beta_nineteen_tenths_higher_modes_negative` `ChemotaxisBifurcation.ModeExamples.beta_nineteen_tenths_lower_root_modes` `ChemotaxisBifurcation.ModeExamples.beta_nineteen_tenths_mode_one_signs` `ChemotaxisBifurcation.ModeExamples.beta_nineteen_tenths_upper_root_modes` `ChemotaxisBifurcation.ModeExamples.beta_three_halves_higher_modes_negative` `ChemotaxisBifurcation.ModeExamples.beta_three_halves_lower_root_modes` `ChemotaxisBifurcation.ModeExamples.beta_three_halves_mode_three_signs` `ChemotaxisBifurcation.ModeExamples.beta_three_halves_modes_one_two_signs` `ChemotaxisBifurcation.ModeExamples.beta_three_halves_upper_root_modes` `ChemotaxisBifurcation.RootTable.beta_nineteen_tenths_physical_signs` `ChemotaxisBifurcation.RootTable.beta_nineteen_tenths_rounding_cells` `ChemotaxisBifurcation.RootTable.beta_three_halves_physical_signs` `ChemotaxisBifurcation.RootTable.beta_three_halves_rounding_cells` `ChemotaxisBifurcation.RootTableAdmissible.beta_one_no_admissible_root` `ChemotaxisBifurcation.RootTableAdmissible.beta_seven_thirds_no_admissible_root` `ChemotaxisBifurcation.RootTableAdmissible.beta_three_no_admissible_root` `ChemotaxisBifurcation.RootTableAdmissible.beta_twelve_fifths_no_admissible_root` `ChemotaxisBifurcation.RootTableAdmissible.beta_twenty_one_tenths_unique_admissible_root` `ChemotaxisBifurcation.RootTableAdmissible.beta_two_unique_admissible_root` `ChemotaxisBifurcation.RootTableRemaining.beta_seven_thirds_roots_exhaust` `ChemotaxisBifurcation.RootTableRemaining.beta_twelve_fifths_roots_exhaust` `ChemotaxisBifurcation.RootTableRemaining.beta_twenty_one_tenths_roots_exhaust` `ChemotaxisBifurcation.RootTableRemaining.beta_two_roots_exhaust` `ChemotaxisBifurcation.TwoRootExhaustion.f1_zero_eq_certified_roots` `ChemotaxisBifurcation.TwoRootExhaustion.f3_zero_eq_certified_roots` `ChemotaxisBifurcation.CoefficientDictionary.example_3_1_display` `ChemotaxisBifurcation.RootTableAggregate.table_3_2_real_roots` `ChemotaxisBifurcation.RootTableAggregate.table_3_2_admissible_roots`	verified verified verified verified verified verified verified verified verified verified verified verified verified verified verified verified verified verified verified verified verified verified verified verified verified verified verified verified verified verified verified verified	identification of the normalized rational expression with the reduced cubic coefficient on λ>1/2 interpretation through untied critical-mode intervals the local bifurcation theorem converting coefficient signs into super-critical or sub-critical bifurcation	V2 scope: Exact rational isolating intervals, exhaustive admissible-root counts, rounding cells, physical signs, and finite mode comparisons are proved. Decimal displays are presentation corollaries. Source locator: p. 27, TeX line 2573.
Lemma 4.1	Bounds for stationary solutions of the non-minimal model	Same assumptions	`chemotaxis-bifurcation-lean/chemotaxisbifurcation-classicalholdernorm-logistic-uniform-norm-bound` `chemotaxis-bifurcation-lean/chemotaxisbifurcation-classicalholderinterface-logistic-uniform-norm-bound` `chemotaxis-bifurcation-lean/chemotaxisbifurcation-stationarymassidentity-classicalprofile-interval-bounds`	`ChemotaxisBifurcation.ClassicalHolderNorm.logistic_uniform_norm_bound` `ChemotaxisBifurcation.ClassicalHolderInterface.logistic_uniform_norm_bound` `ChemotaxisBifurcation.StationaryMassIdentity.ClassicalProfile.interval_bounds`	verified verified verified	—	Exact public scope, hypotheses and exclusions: data/public-scope-ledger.json, row paper3/L:spiky-solu-lm1. This display summary does not extend that scope. Source locator: p. 28, TeX line 2633.
Lemma 4.2	Bounds for stationary solutions of the minimal model	Same assumptions	`chemotaxis-bifurcation-lean/chemotaxisbifurcation-classicalholdernorm-minimal-uniform-norm-bound` `chemotaxis-bifurcation-lean/chemotaxisbifurcation-classicalholderinterface-minimal-uniform-norm-bound` `chemotaxis-bifurcation-lean/chemotaxisbifurcation-classicalminimalestimates-interval-bounds`	`ChemotaxisBifurcation.ClassicalHolderNorm.minimal_uniform_norm_bound` `ChemotaxisBifurcation.ClassicalHolderInterface.minimal_uniform_norm_bound` `ChemotaxisBifurcation.ClassicalMinimalEstimates.interval_bounds`	verified verified verified	—	Exact public scope, hypotheses and exclusions: data/public-scope-ledger.json, row paper3/L:minimal-spike-bounds. This display summary does not extend that scope. Source locator: p. 29, TeX line 2765.
Lemma 4.1 and Lemma 4.2, bounded-sensitivity proof context	Compactness at bounded sensitivity (dissolved into Lemmas 4.1-4.2 in v1)	Same assumptions	`chemotaxis-bifurcation-lean/chemotaxisbifurcation-classicalboundedcompactness-logistic-stationary-limit` `chemotaxis-bifurcation-lean/chemotaxisbifurcation-classicalboundedcompactness-minimal-stationary-limit` `chemotaxis-bifurcation-lean/chemotaxisbifurcation-allpositivelogisticcompactness-logistic-all-positive-norm-subsequence` `chemotaxis-bifurcation-lean/chemotaxisbifurcation-weakh2compactness-minimal-physical-norm-subsequence`	`ChemotaxisBifurcation.ClassicalBoundedCompactness.logistic_stationary_limit` `ChemotaxisBifurcation.ClassicalBoundedCompactness.minimal_stationary_limit` `ChemotaxisBifurcation.AllPositiveLogisticCompactness.logistic_all_positive_norm_subsequence` `ChemotaxisBifurcation.WeakH2Compactness.minimal_physical_norm_subsequence`	verified verified verified verified	—	Exact public scope, hypotheses and exclusions: data/public-scope-ledger.json, row paper3/L:bounded-sensitivity-compactness. This display summary does not extend that scope. Source locator: p. 28, TeX line 2633.
Lemma 5.1	Constant limits at large sensitivity	Same assumptions	`chemotaxis-bifurcation-lean/chemotaxisbifurcation-classicalspikesubsequence-exists-constant-signal-and-weak-tests` `chemotaxis-bifurcation-lean/chemotaxisbifurcation-classicalspikeinterface-classical-all-test-subsequence`	`ChemotaxisBifurcation.ClassicalSpikeSubsequence.exists_constant_signal_and_weak_tests` `ChemotaxisBifurcation.ClassicalSpikeInterface.classical_all_test_subsequence`	verified verified	—	Exact public scope, hypotheses and exclusions: data/public-scope-ledger.json, row paper3/L:minimal-spike-limit. This display summary does not extend that scope. Source locator: p. 34, TeX line 3155.
Equation (6.2)	Conservative semidiscrete scheme for the minimal model	Same assumptions	`chemotaxis-bifurcation-lean/chemotaxisbifurcation-conservativemass-conservative-flux-mass-rate-zero` `chemotaxis-bifurcation-lean/chemotaxisbifurcation-conservativemass-conservative-scheme-preserves-trapezoidal-mass` `chemotaxis-bifurcation-lean/chemotaxisbifurcation-conservativemass-flux-difference-telescope` `chemotaxis-bifurcation-lean/chemotaxisbifurcation-discretelinearization-conservativefaceflux-directionalderivative` `chemotaxis-bifurcation-lean/chemotaxisbifurcation-discretelinearization-conservativenoderate-directionalderivative`	`ChemotaxisBifurcation.ConservativeMass.conservative_flux_mass_rate_zero` `ChemotaxisBifurcation.ConservativeMass.conservative_scheme_preserves_trapezoidal_mass` `ChemotaxisBifurcation.ConservativeMass.flux_difference_telescope` `ChemotaxisBifurcation.DiscreteLinearization.conservativeFaceFlux_directionalDerivative` `ChemotaxisBifurcation.DiscreteLinearization.conservativeNodeRate_directionalDerivative`	verified verified verified verified verified	—	V2 scope: The literal finite face-flux divergence telescopes under trapezoidal weights, and its directional derivative is connected to the reflected fixed-mass modal system. Numerical trajectory existence and differentiability are not asserted. Source locator: p. 36, TeX line 3382.
Theorem 1.2	Degree-three numerator and denominator of beta_n0 in the minimal model	Same assumptions	`chemotaxis-bifurcation-lean/chemotaxisbifurcation-minimalrational-x-mul-m3poly` `chemotaxis-bifurcation-lean/chemotaxisbifurcation-minimalrational-coefficient-eq-m3` `chemotaxis-bifurcation-lean/chemotaxisbifurcation-minimalrational-fixedmassbetacoefficient-eq-cubic-ratio` `chemotaxis-bifurcation-lean/chemotaxisbifurcation-minimalrational-fixedmass-eq-logistic` `chemotaxis-bifurcation-lean/chemotaxisbifurcation-minimalrational-m3poly` `chemotaxis-bifurcation-lean/chemotaxisbifurcation-minimalrational-minimalnumeratorpoly` `chemotaxis-bifurcation-lean/chemotaxisbifurcation-minimalrational-n4-eval-zero` `chemotaxis-bifurcation-lean/chemotaxisbifurcation-minimalrational-natdegree-m3poly-le` `chemotaxis-bifurcation-lean/chemotaxisbifurcation-minimalrational-natdegree-minimalnumeratorpoly-le`	`ChemotaxisBifurcation.MinimalRational.X_mul_m3Poly` `ChemotaxisBifurcation.MinimalRational.coefficient_eq_m3` `ChemotaxisBifurcation.MinimalRational.fixedMassBetaCoefficient_eq_cubic_ratio` `ChemotaxisBifurcation.MinimalRational.fixedMass_eq_logistic` `ChemotaxisBifurcation.MinimalRational.m3Poly` `ChemotaxisBifurcation.MinimalRational.minimalNumeratorPoly` `ChemotaxisBifurcation.MinimalRational.n4_eval_zero` `ChemotaxisBifurcation.MinimalRational.natDegree_m3Poly_le` `ChemotaxisBifurcation.MinimalRational.natDegree_minimalNumeratorPoly_le`	verified verified verified verified verified verified verified verified verified	—	Minimal-model degree-three numerator/denominator clause; existing non-minimal bindings do not certify it. Source locator: p. 8, TeX line 699.
Lemma 2.1, Equations 2.1-2.4 (infinite-fourier-convolution)	Infinite Fourier series: summability, exchange of sums and integrals, convolution	Same assumptions	`chemotaxis-bifurcation-lean/chemotaxisbifurcation-fourierseriesproducts-tsum-mul-tsum-bounded` `chemotaxis-bifurcation-lean/chemotaxisbifurcation-fourierseriesproducts-summable-norm-mul-bounded` `chemotaxis-bifurcation-lean/chemotaxisbifurcation-fourierseriesproducts-cosineseries-mul-cosineseries` `chemotaxis-bifurcation-lean/chemotaxisbifurcation-fourierseriesproducts-cosineseries-mul-cosineseries-mul-cosineseries` `chemotaxis-bifurcation-lean/chemotaxisbifurcation-fourierseriesproducts-hassum-integral-tsum-mul` `chemotaxis-bifurcation-lean/chemotaxisbifurcation-fourierseriesproducts-hassum-integral-tsum-mul-tsum` `chemotaxis-bifurcation-lean/chemotaxisbifurcation-fourierseriesproducts-hassum-mul-ite` `chemotaxis-bifurcation-lean/chemotaxisbifurcation-fourierseriesproducts-hassum-mul-ite-int-eq` `chemotaxis-bifurcation-lean/chemotaxisbifurcation-fourierseriesproducts-hassum-pair-ite-add-eq-neg` `chemotaxis-bifurcation-lean/chemotaxisbifurcation-fourierseriesproducts-hassum-pair-ite-add-eq-of-neg` `chemotaxis-bifurcation-lean/chemotaxisbifurcation-fourierseriesproducts-hassum-triple-ite-add-add-eq-neg` `chemotaxis-bifurcation-lean/chemotaxisbifurcation-fourierseriesproducts-cosine-sine-sine-of-kernel` `chemotaxis-bifurcation-lean/chemotaxisbifurcation-fourierseriesproducts-two-cosines-two-sines-of-kernel` `chemotaxis-bifurcation-lean/chemotaxisbifurcation-fourierseriesproducts-cos-cos-cos-of-kernel` `chemotaxis-bifurcation-lean/chemotaxisbifurcation-fourierseriesproducts-cos-cos-cos-cos-of-kernel` `chemotaxis-bifurcation-lean/chemotaxisbifurcation-fourierseriesproducts-summable-norm-of-lp-one` `chemotaxis-bifurcation-lean/chemotaxisbifurcation-infinitecosineprojection-hassum-intervalintegral-boundedphase` `chemotaxis-bifurcation-lean/chemotaxisbifurcation-infinitecosineprojection-cosinephase` `chemotaxis-bifurcation-lean/chemotaxisbifurcation-trigintegrals-cosine-sine-sine` `chemotaxis-bifurcation-lean/chemotaxisbifurcation-trigintegrals-two-cosines-two-sines` `chemotaxis-bifurcation-lean/chemotaxisbifurcation-trigintegrals-cos-cos-cos` `chemotaxis-bifurcation-lean/chemotaxisbifurcation-trigintegrals-cos-cos-cos-cos`	`ChemotaxisBifurcation.FourierSeriesProducts.tsum_mul_tsum_bounded` `ChemotaxisBifurcation.FourierSeriesProducts.summable_norm_mul_bounded` `ChemotaxisBifurcation.FourierSeriesProducts.cosineSeries_mul_cosineSeries` `ChemotaxisBifurcation.FourierSeriesProducts.cosineSeries_mul_cosineSeries_mul_cosineSeries` `ChemotaxisBifurcation.FourierSeriesProducts.hasSum_integral_tsum_mul` `ChemotaxisBifurcation.FourierSeriesProducts.hasSum_integral_tsum_mul_tsum` `ChemotaxisBifurcation.FourierSeriesProducts.hasSum_mul_ite` `ChemotaxisBifurcation.FourierSeriesProducts.hasSum_mul_ite_int_eq` `ChemotaxisBifurcation.FourierSeriesProducts.hasSum_pair_ite_add_eq_neg` `ChemotaxisBifurcation.FourierSeriesProducts.hasSum_pair_ite_add_eq_of_neg` `ChemotaxisBifurcation.FourierSeriesProducts.hasSum_triple_ite_add_add_eq_neg` `ChemotaxisBifurcation.FourierSeriesProducts.cosine_sine_sine_of_kernel` `ChemotaxisBifurcation.FourierSeriesProducts.two_cosines_two_sines_of_kernel` `ChemotaxisBifurcation.FourierSeriesProducts.cos_cos_cos_of_kernel` `ChemotaxisBifurcation.FourierSeriesProducts.cos_cos_cos_cos_of_kernel` `ChemotaxisBifurcation.FourierSeriesProducts.summable_norm_of_lp_one` `ChemotaxisBifurcation.InfiniteCosineProjection.hasSum_intervalIntegral_boundedPhase` `ChemotaxisBifurcation.InfiniteCosineProjection.cosinePhase` `ChemotaxisBifurcation.TrigIntegrals.cosine_sine_sine` `ChemotaxisBifurcation.TrigIntegrals.two_cosines_two_sines` `ChemotaxisBifurcation.TrigIntegrals.cos_cos_cos` `ChemotaxisBifurcation.TrigIntegrals.cos_cos_cos_cos`	verified verified verified verified verified verified verified verified verified verified verified verified verified verified verified verified verified verified verified verified verified verified	—	ell1 summability, exchange of sums/integrals, and convolution multiplicities; finite identities are ingredients only. Source locator: p. 13, TeX line 1153.
Equation (2.43) (current-remainder-consumer)	Mixed remainder and derivative interface of the reduced equation	Inputs supplied	`chemotaxis-bifurcation-lean/chemotaxisbifurcation-mixedremainder-center-ode-final-value-bound-weak` `chemotaxis-bifurcation-lean/chemotaxisbifurcation-mixedremainder-center-ode-final-deriv-bound-weak` `chemotaxis-bifurcation-lean/chemotaxisbifurcation-mixedremainder-center-ode-final-branch-eventually` `chemotaxis-bifurcation-lean/chemotaxisbifurcation-mixedremainder-reducedfield` `chemotaxis-bifurcation-lean/chemotaxisbifurcation-mixedremainder-mixed-equilibrium-core` `chemotaxis-bifurcation-lean/chemotaxisbifurcation-mixedremainder-mixed-parameter-le-amp-sq` `chemotaxis-bifurcation-lean/chemotaxisbifurcation-mixedremainder-mixed-value-bound-absorbed` `chemotaxis-bifurcation-lean/chemotaxisbifurcation-mixedremainder-mixed-deriv-bound-absorbed` `chemotaxis-bifurcation-lean/chemotaxisbifurcation-mixedremainder-mixed-branch-eventually` `chemotaxis-bifurcation-lean/chemotaxisbifurcation-mixedremainder-mixed-side-condition-eventually` `chemotaxis-bifurcation-lean/chemotaxisbifurcation-mixedremainder-exists-pos-equilibrium` `chemotaxis-bifurcation-lean/chemotaxisbifurcation-mixedremainder-branchsmall-eventually` `chemotaxis-bifurcation-lean/chemotaxisbifurcation-mixedremainder-branchsmall` `chemotaxis-bifurcation-lean/chemotaxisbifurcation-mixedremainder-ampconst` `chemotaxis-bifurcation-lean/chemotaxisbifurcation-mixedremainder-absorbedconst` `chemotaxis-bifurcation-lean/chemotaxisbifurcation-normalform-paper-equilibrium-core` `chemotaxis-bifurcation-lean/chemotaxisbifurcation-branchderivativeasymptotic-branch-derivative-error-bound` `chemotaxis-bifurcation-lean/chemotaxisbifurcation-branchderivativeasymptotic-branch-derivative-islittleo`	`ChemotaxisBifurcation.MixedRemainder.center_ODE_final_value_bound_weak` `ChemotaxisBifurcation.MixedRemainder.center_ODE_final_deriv_bound_weak` `ChemotaxisBifurcation.MixedRemainder.center_ODE_final_branch_eventually` `ChemotaxisBifurcation.MixedRemainder.reducedField` `ChemotaxisBifurcation.MixedRemainder.mixed_equilibrium_core` `ChemotaxisBifurcation.MixedRemainder.mixed_parameter_le_amp_sq` `ChemotaxisBifurcation.MixedRemainder.mixed_value_bound_absorbed` `ChemotaxisBifurcation.MixedRemainder.mixed_deriv_bound_absorbed` `ChemotaxisBifurcation.MixedRemainder.mixed_branch_eventually` `ChemotaxisBifurcation.MixedRemainder.mixed_side_condition_eventually` `ChemotaxisBifurcation.MixedRemainder.exists_pos_equilibrium` `ChemotaxisBifurcation.MixedRemainder.branchSmall_eventually` `ChemotaxisBifurcation.MixedRemainder.BranchSmall` `ChemotaxisBifurcation.MixedRemainder.ampConst` `ChemotaxisBifurcation.MixedRemainder.absorbedConst` `ChemotaxisBifurcation.NormalForm.paper_equilibrium_core` `ChemotaxisBifurcation.BranchDerivativeAsymptotic.branch_derivative_error_bound` `ChemotaxisBifurcation.BranchDerivativeAsymptotic.branch_derivative_isLittleO`	verified verified verified verified verified verified verified verified verified verified verified verified verified verified verified verified verified verified	identification of the application remainder and scalar coefficients α>0 and β≠0 fixed C≥0 and 0<r≤1 either stated uniform value-bound interface on the local box actual differentiability in s the corresponding independently supplied uniform derivative bound	Current mixed remainder and derivative interface; retain analytic hypotheses. The actual scalar BranchCurves branches also satisfy derivative = -2 alpha eta + o(\|eta\|) along the correct branch-side filter, derived from the remainder estimates and amplitude localization. Source locator: p. 20, TeX line 1961.
Theorem 1.3(1)	Relative component construction of the global branch	Inputs supplied	`chemotaxis-bifurcation-lean/chemotaxisbifurcation-parentcomponent` `chemotaxis-bifurcation-lean/chemotaxisbifurcation-unilateralremainder` `chemotaxis-bifurcation-lean/chemotaxisbifurcation-selectedcomponent` `chemotaxis-bifurcation-lean/chemotaxisbifurcation-isclosed-connectedcomponentin-of-isclosed` `chemotaxis-bifurcation-lean/chemotaxisbifurcation-isclosed-sdiff-of-isopen-preimage` `chemotaxis-bifurcation-lean/chemotaxisbifurcation-parentcomponent-isclosed` `chemotaxis-bifurcation-lean/chemotaxisbifurcation-unilateralremainder-isclosed` `chemotaxis-bifurcation-lean/chemotaxisbifurcation-retainedwithbase-subset-parentcomponent` `chemotaxis-bifurcation-lean/chemotaxisbifurcation-retainedwithbase-subset-unilateralremainder` `chemotaxis-bifurcation-lean/chemotaxisbifurcation-retainedwithbase-subset-selectedcomponent` `chemotaxis-bifurcation-lean/chemotaxisbifurcation-base-mem-selectedcomponent` `chemotaxis-bifurcation-lean/chemotaxisbifurcation-selectedcomponent-isclosed` `chemotaxis-bifurcation-lean/chemotaxisbifurcation-selectedcomponent-subset-solutionclosure` `chemotaxis-bifurcation-lean/chemotaxisbifurcation-selectedsolutioncomponents-selected-properties` `chemotaxis-bifurcation-lean/chemotaxisbifurcation-selectedsolutioncomponents-logistic-selected-properties` `chemotaxis-bifurcation-lean/chemotaxisbifurcation-selectedsolutioncomponents-minimal-selected-properties` `chemotaxis-bifurcation-lean/chemotaxisbifurcation-localbranchgeometry-insert-image-ioo` `chemotaxis-bifurcation-lean/chemotaxisbifurcation-localbranchgeometry-halfcurve-selected` `chemotaxis-bifurcation-lean/chemotaxisbifurcation-localbranchgeometry-halfcurve-selector-independent` `chemotaxis-bifurcation-lean/chemotaxisbifurcation-localbranchgeometry-negative-arc-relatively-open` `chemotaxis-bifurcation-lean/chemotaxisbifurcation-parametrizedsolutioncomponents-selectedimage-of-local-curve` `chemotaxis-bifurcation-lean/chemotaxisbifurcation-parametrizedsolutioncomponents-selectedimage-selector-independent` `chemotaxis-bifurcation-lean/chemotaxisbifurcation-fourieramplitude-coefficient` `chemotaxis-bifurcation-lean/chemotaxisbifurcation-fourieramplitude-continuous-coefficient` `chemotaxis-bifurcation-lean/chemotaxisbifurcation-fourieramplitude-coefficient-add` `chemotaxis-bifurcation-lean/chemotaxisbifurcation-fourieramplitude-coefficient-smul` `chemotaxis-bifurcation-lean/chemotaxisbifurcation-fourieramplitude-coefficientclm` `chemotaxis-bifurcation-lean/chemotaxisbifurcation-fourieramplitude-coefficient-eq-projection` `chemotaxis-bifurcation-lean/chemotaxisbifurcation-fourieramplitude-coefficient-const` `chemotaxis-bifurcation-lean/chemotaxisbifurcation-fourieramplitude-isclosed-zero-coordinate` `chemotaxis-bifurcation-lean/chemotaxisbifurcation-fourieramplitude-coefficient-eq-cosinecoeff` `chemotaxis-bifurcation-lean/chemotaxisbifurcation-fourieramplitude-coefficient-sub-const` `chemotaxis-bifurcation-lean/chemotaxisbifurcation-fourieramplitude-coefficient-eq-zero-iff` `chemotaxis-bifurcation-lean/chemotaxisbifurcation-fourieramplitude-isclosed-orthogonal` `chemotaxis-bifurcation-lean/chemotaxisbifurcation-fourieramplitude-isclosed-minimal-orthogonal` `chemotaxis-bifurcation-lean/chemotaxisbifurcation-fourieramplitude-coefficient-of-decomposition` `chemotaxis-bifurcation-lean/chemotaxisbifurcation-fourieramplitude-amplitude` `chemotaxis-bifurcation-lean/chemotaxisbifurcation-fourieramplitude-continuous-amplitude` `chemotaxis-bifurcation-lean/chemotaxisbifurcation-fourieramplitude-curve-amplitude` `chemotaxis-bifurcation-lean/chemotaxisbifurcation-fourieramplitude-curve-base-population` `chemotaxis-bifurcation-lean/chemotaxisbifurcation-weakh2cosinemode-mode-h2` `chemotaxis-bifurcation-lean/chemotaxisbifurcation-weakh2cosinemode-mode-neumann` `chemotaxis-bifurcation-lean/chemotaxisbifurcation-weakh2cosinemode-mode` `chemotaxis-bifurcation-lean/chemotaxisbifurcation-weakh2cosinemode-profile-mode` `chemotaxis-bifurcation-lean/chemotaxisbifurcation-weakh2cosinemode-mass-mode` `chemotaxis-bifurcation-lean/chemotaxisbifurcation-weakh2cosinemode-mode-mem-fixedmeanset` `chemotaxis-bifurcation-lean/chemotaxisbifurcation-weakh2cosinemode-coefficient-mode-kronecker` `chemotaxis-bifurcation-lean/chemotaxisbifurcation-weakh2cosinemode-coefficient-mode` `chemotaxis-bifurcation-lean/chemotaxisbifurcation-fouriercomplement-complement` `chemotaxis-bifurcation-lean/chemotaxisbifurcation-fouriercomplement-mem-complement-iff` `chemotaxis-bifurcation-lean/chemotaxisbifurcation-fouriercomplement-isclosed-complement` `chemotaxis-bifurcation-lean/chemotaxisbifurcation-fouriercomplement-modeline` `chemotaxis-bifurcation-lean/chemotaxisbifurcation-fouriercomplement-coefficient-modeline` `chemotaxis-bifurcation-lean/chemotaxisbifurcation-fouriercomplement-splitting` `chemotaxis-bifurcation-lean/chemotaxisbifurcation-fouriercomplement-splitting-amplitude` `chemotaxis-bifurcation-lean/chemotaxisbifurcation-fouriercomplement-splitting-remainder` `chemotaxis-bifurcation-lean/chemotaxisbifurcation-fouriercomplement-splitting-reconstruct` `chemotaxis-bifurcation-lean/chemotaxisbifurcation-fouriercomplement-decomposition-unique` `chemotaxis-bifurcation-lean/chemotaxisbifurcation-fouriercomplement-iscompl-span-complement`	`ChemotaxisBifurcation.parentComponent` `ChemotaxisBifurcation.unilateralRemainder` `ChemotaxisBifurcation.selectedComponent` `ChemotaxisBifurcation.isClosed_connectedComponentIn_of_isClosed` `ChemotaxisBifurcation.isClosed_sdiff_of_isOpen_preimage` `ChemotaxisBifurcation.parentComponent_isClosed` `ChemotaxisBifurcation.unilateralRemainder_isClosed` `ChemotaxisBifurcation.retainedWithBase_subset_parentComponent` `ChemotaxisBifurcation.retainedWithBase_subset_unilateralRemainder` `ChemotaxisBifurcation.retainedWithBase_subset_selectedComponent` `ChemotaxisBifurcation.base_mem_selectedComponent` `ChemotaxisBifurcation.selectedComponent_isClosed` `ChemotaxisBifurcation.selectedComponent_subset_solutionClosure` `ChemotaxisBifurcation.SelectedSolutionComponents.selected_properties` `ChemotaxisBifurcation.SelectedSolutionComponents.logistic_selected_properties` `ChemotaxisBifurcation.SelectedSolutionComponents.minimal_selected_properties` `ChemotaxisBifurcation.LocalBranchGeometry.insert_image_Ioo` `ChemotaxisBifurcation.LocalBranchGeometry.halfcurve_selected` `ChemotaxisBifurcation.LocalBranchGeometry.halfcurve_selector_independent` `ChemotaxisBifurcation.LocalBranchGeometry.negative_arc_relatively_open` `ChemotaxisBifurcation.ParametrizedSolutionComponents.selectedImage_of_local_curve` `ChemotaxisBifurcation.ParametrizedSolutionComponents.selectedImage_selector_independent` `ChemotaxisBifurcation.FourierAmplitude.coefficient` `ChemotaxisBifurcation.FourierAmplitude.continuous_coefficient` `ChemotaxisBifurcation.FourierAmplitude.coefficient_add` `ChemotaxisBifurcation.FourierAmplitude.coefficient_smul` `ChemotaxisBifurcation.FourierAmplitude.coefficientCLM` `ChemotaxisBifurcation.FourierAmplitude.coefficient_eq_projection` `ChemotaxisBifurcation.FourierAmplitude.coefficient_const` `ChemotaxisBifurcation.FourierAmplitude.isClosed_zero_coordinate` `ChemotaxisBifurcation.FourierAmplitude.coefficient_eq_cosineCoeff` `ChemotaxisBifurcation.FourierAmplitude.coefficient_sub_const` `ChemotaxisBifurcation.FourierAmplitude.coefficient_eq_zero_iff` `ChemotaxisBifurcation.FourierAmplitude.isClosed_orthogonal` `ChemotaxisBifurcation.FourierAmplitude.isClosed_minimal_orthogonal` `ChemotaxisBifurcation.FourierAmplitude.coefficient_of_decomposition` `ChemotaxisBifurcation.FourierAmplitude.amplitude` `ChemotaxisBifurcation.FourierAmplitude.continuous_amplitude` `ChemotaxisBifurcation.FourierAmplitude.curve_amplitude` `ChemotaxisBifurcation.FourierAmplitude.curve_base_population` `ChemotaxisBifurcation.WeakH2CosineMode.mode_H2` `ChemotaxisBifurcation.WeakH2CosineMode.mode_neumann` `ChemotaxisBifurcation.WeakH2CosineMode.mode` `ChemotaxisBifurcation.WeakH2CosineMode.profile_mode` `ChemotaxisBifurcation.WeakH2CosineMode.mass_mode` `ChemotaxisBifurcation.WeakH2CosineMode.mode_mem_fixedMeanSet` `ChemotaxisBifurcation.WeakH2CosineMode.coefficient_mode_kronecker` `ChemotaxisBifurcation.WeakH2CosineMode.coefficient_mode` `ChemotaxisBifurcation.FourierComplement.complement` `ChemotaxisBifurcation.FourierComplement.mem_complement_iff` `ChemotaxisBifurcation.FourierComplement.isClosed_complement` `ChemotaxisBifurcation.FourierComplement.modeLine` `ChemotaxisBifurcation.FourierComplement.coefficient_modeLine` `ChemotaxisBifurcation.FourierComplement.splitting` `ChemotaxisBifurcation.FourierComplement.splitting_amplitude` `ChemotaxisBifurcation.FourierComplement.splitting_remainder` `ChemotaxisBifurcation.FourierComplement.splitting_reconstruct` `ChemotaxisBifurcation.FourierComplement.decomposition_unique` `ChemotaxisBifurcation.FourierComplement.isCompl_span_complement`	verified verified verified verified verified verified verified verified verified verified verified verified verified verified verified verified verified verified verified verified verified verified verified verified verified verified verified verified verified verified verified verified verified verified verified verified verified verified verified verified verified verified verified verified verified verified verified verified verified verified verified verified verified verified verified verified verified verified verified	the actual admissible subtype V and its topology the solution closure base membership from the local branch relative openness of the removed punctured arc from local uniqueness connectedness and solution-closure containment of the retained arc with its base disjointness from the removed arc a selector on the retained arc not proved here: the unilateral alternatives and their bifurcation foundations	Conditional scope retained. Actual cosine complement, curved elliptic cubic response and conserved-mean coefficient extraction supply the scoped ingredients. Family/jet construction, operator identity and global foundations remain explicit. Public scope and supplied inputs: data/public-scope-ledger.json, paper3/relative-component-topology
Theorem 1.3(3)	Fixed mass and vanishing tails give a Dirac limit	Same assumptions	`chemotaxis-bifurcation-lean/chemotaxisbifurcation-endpointconcentration-closedinterval` `chemotaxis-bifurcation-lean/chemotaxisbifurcation-endpointconcentration-leftendpoint` `chemotaxis-bifurcation-lean/chemotaxisbifurcation-endpointconcentration-rightendpoint` `chemotaxis-bifurcation-lean/chemotaxisbifurcation-endpointconcentration-tendsto-mass-smul-dirac-of-vanishing-tails` `chemotaxis-bifurcation-lean/chemotaxisbifurcation-endpointconcentration-tendsto-integral-test-of-vanishing-tails` `chemotaxis-bifurcation-lean/chemotaxisbifurcation-endpointconcentration-tendsto-left-endpoint-on-icc` `chemotaxis-bifurcation-lean/chemotaxisbifurcation-endpointconcentration-tendsto-right-endpoint-on-icc` `chemotaxis-bifurcation-lean/chemotaxisbifurcation-endpointconcentration-peak-tendsto-attop-of-mass-tail-window-bounds` `chemotaxis-bifurcation-lean/chemotaxisbifurcation-physicalendpointconcentration-decreasing-actual-concentration` `chemotaxis-bifurcation-lean/chemotaxisbifurcation-physicalendpointconcentration-increasing-actual-concentration`	`ChemotaxisBifurcation.EndpointConcentration.ClosedInterval` `ChemotaxisBifurcation.EndpointConcentration.leftEndpoint` `ChemotaxisBifurcation.EndpointConcentration.rightEndpoint` `ChemotaxisBifurcation.EndpointConcentration.tendsto_mass_smul_dirac_of_vanishing_tails` `ChemotaxisBifurcation.EndpointConcentration.tendsto_integral_test_of_vanishing_tails` `ChemotaxisBifurcation.EndpointConcentration.tendsto_left_endpoint_on_Icc` `ChemotaxisBifurcation.EndpointConcentration.tendsto_right_endpoint_on_Icc` `ChemotaxisBifurcation.EndpointConcentration.peak_tendsto_atTop_of_mass_tail_window_bounds` `ChemotaxisBifurcation.PhysicalEndpointConcentration.decreasing_actual_concentration` `ChemotaxisBifurcation.PhysicalEndpointConcentration.increasing_actual_concentration`	verified verified verified verified verified verified verified verified verified verified	—	Exact public scope, hypotheses and exclusions: data/public-scope-ledger.json, row paper3/tail-mass-dirac-consumer. This display summary does not extend that scope. Source locator: p. 10, TeX line 933.
Lemma 4.1(1), Equation 4.1	Mass and moment bounds for stationary solutions of the non-minimal model	Same assumptions	`chemotaxis-bifurcation-lean/chemotaxisbifurcation-intervalmoments-logistic-interval-bounds` `chemotaxis-bifurcation-lean/chemotaxisbifurcation-intervalmoments-strict-power-integral` `chemotaxis-bifurcation-lean/chemotaxisbifurcation-intervalmoments-not-ae-eq-const` `chemotaxis-bifurcation-lean/chemotaxisbifurcation-intervalmoments-eq-zero-of-integral-eq-zero` `chemotaxis-bifurcation-lean/chemotaxisbifurcation-intervalmoments-eqon-of-ae-eq-const` `chemotaxis-bifurcation-lean/chemotaxisbifurcation-intervalmoments-intervalmeasure` `chemotaxis-bifurcation-lean/chemotaxisbifurcation-intervalmoments-intervalmeasure-real-univ` `chemotaxis-bifurcation-lean/chemotaxisbifurcation-intervalmoments-integral-eq-intervalintegral` `chemotaxis-bifurcation-lean/chemotaxisbifurcation-stationarymassbounds-logistic-moment-bounds` `chemotaxis-bifurcation-lean/chemotaxisbifurcation-stationarymassbounds-strict-power-average` `chemotaxis-bifurcation-lean/chemotaxisbifurcation-stationarymassidentity-classicalprofile-interval-bounds` `chemotaxis-bifurcation-lean/chemotaxisbifurcation-stationarymassidentity-logistic-mass-identity-of-stationary`	`ChemotaxisBifurcation.IntervalMoments.logistic_interval_bounds` `ChemotaxisBifurcation.IntervalMoments.strict_power_integral` `ChemotaxisBifurcation.IntervalMoments.not_ae_eq_const` `ChemotaxisBifurcation.IntervalMoments.eq_zero_of_integral_eq_zero` `ChemotaxisBifurcation.IntervalMoments.eqOn_of_ae_eq_const` `ChemotaxisBifurcation.IntervalMoments.intervalMeasure` `ChemotaxisBifurcation.IntervalMoments.intervalMeasure_real_univ` `ChemotaxisBifurcation.IntervalMoments.integral_eq_intervalIntegral` `ChemotaxisBifurcation.StationaryMassBounds.logistic_moment_bounds` `ChemotaxisBifurcation.StationaryMassBounds.strict_power_average` `ChemotaxisBifurcation.StationaryMassIdentity.ClassicalProfile.interval_bounds` `ChemotaxisBifurcation.StationaryMassIdentity.logistic_mass_identity_of_stationary`	verified verified verified verified verified verified verified verified verified verified verified verified	—	ClassicalProfile.interval_bounds proves all four strict extremum/moment conclusions for every given positive nonconstant classical stationary profile. The literal flux, equation and both u/v Neumann data derive mass balance; no independent mass identity remains. Verified within this entire classical-solution statement, without asserting existence. Source locator: p. 28, TeX line 2639.
Lemma 4.1(2), Equation 4.6	Moment step for 0 < gamma <= 1 + alpha	Same assumptions	`chemotaxis-bifurcation-lean/chemotaxisbifurcation-intervalmoments-logistic-power-integral-le` `chemotaxis-bifurcation-lean/chemotaxisbifurcation-stationarymassidentity-classicalprofile-power-moment`	`ChemotaxisBifurcation.IntervalMoments.logistic_power_integral_le` `ChemotaxisBifurcation.StationaryMassIdentity.ClassicalProfile.power_moment`	verified verified	—	The new direct ClassicalProfile.power_moment supplies the exact gamma-moment bound for0<gamma<=1+alpha from the actual stationary equation through interval_bounds; the higher moment is no longer independently assumed. Its current kernel type was printed and read. Source locator: p. 28, TeX line 2699.
Equation 4.14 (proof of Lemma 4.2(2))	Flux identity of the minimal model	Same assumptions	`chemotaxis-bifurcation-lean/chemotaxisbifurcation-minimalflux-minimal-flux-identity` `chemotaxis-bifurcation-lean/chemotaxisbifurcation-minimalflux-flux` `chemotaxis-bifurcation-lean/chemotaxisbifurcation-minimalflux-eq-left-of-hasderivat-zero` `chemotaxis-bifurcation-lean/chemotaxisbifurcation-classicalminimalestimates-flux-identity`	`ChemotaxisBifurcation.MinimalFlux.minimal_flux_identity` `ChemotaxisBifurcation.MinimalFlux.flux` `ChemotaxisBifurcation.MinimalFlux.eq_left_of_hasDerivAt_zero` `ChemotaxisBifurcation.ClassicalMinimalEstimates.flux_identity`	verified verified verified verified	—	ClassicalMinimalEstimates.flux_identity derives the literal flux identity from the actual a=b=0 stationary population equation and Neumann data. No first-integral assumption remains; classical derivatives and the original equation are standing solution data. Source locator: p. 30, TeX line 2793.
Lemma 4.2(1)	Mass and moment bounds for stationary solutions of the minimal model	Same assumptions	`chemotaxis-bifurcation-lean/chemotaxisbifurcation-intervalmoments-minimal-interval-bounds` `chemotaxis-bifurcation-lean/chemotaxisbifurcation-intervalmoments-eqon-const-of-le-of-integral-eq` `chemotaxis-bifurcation-lean/chemotaxisbifurcation-intervalmoments-eqon-const-of-ge-of-integral-eq` `chemotaxis-bifurcation-lean/chemotaxisbifurcation-intervalmoments-strict-power-integral` `chemotaxis-bifurcation-lean/chemotaxisbifurcation-classicalminimalestimates-interval-bounds`	`ChemotaxisBifurcation.IntervalMoments.minimal_interval_bounds` `ChemotaxisBifurcation.IntervalMoments.eqOn_const_of_le_of_integral_eq` `ChemotaxisBifurcation.IntervalMoments.eqOn_const_of_ge_of_integral_eq` `ChemotaxisBifurcation.IntervalMoments.strict_power_integral` `ChemotaxisBifurcation.ClassicalMinimalEstimates.interval_bounds`	verified verified verified verified verified	—	Actual prescribed-mass positive nonconstant classical solution supplies both strict extrema and strict second moment; prescribed mass is the ordinary model hypothesis. Source locator: p. 29, TeX line 2765.
Proof of Lemma 4.2(2) (applies Equation 4.6, p. 28, TeX line 2687)	Fixed-mass Jensen step	Same assumptions	`chemotaxis-bifurcation-lean/chemotaxisbifurcation-intervalmoments-minimal-power-integral-le` `chemotaxis-bifurcation-lean/chemotaxisbifurcation-stationarymassbounds-fixed-mass-power-integral` `chemotaxis-bifurcation-lean/chemotaxisbifurcation-stationarymassbounds-fixed-mean-power-average` `chemotaxis-bifurcation-lean/chemotaxisbifurcation-classicalminimalestimates-power-moment`	`ChemotaxisBifurcation.IntervalMoments.minimal_power_integral_le` `ChemotaxisBifurcation.StationaryMassBounds.fixed_mass_power_integral` `ChemotaxisBifurcation.StationaryMassBounds.fixed_mean_power_average` `ChemotaxisBifurcation.ClassicalMinimalEstimates.power_moment`	verified verified verified verified	—	ClassicalMinimalEstimates.power_moment proves the exact prescribed-mass concave moment estimate for all0<=r<=1. Prescribed mass is an explicit model hypothesis of the manuscript, not an unresolved analytic inference. In particular r=m-1 covers both endpoints m=1 and m=2. Source locator: p. 29, TeX line 2765.
Proof of Lemma 4.2(2), m=1 case of the variation-of-constants display	Exponential representation for m = 1	Same assumptions	`chemotaxis-bifurcation-lean/chemotaxisbifurcation-minimalflux-minimal-exp-representation` `chemotaxis-bifurcation-lean/chemotaxisbifurcation-minimalflux-eq-left-of-hasderivat-zero` `chemotaxis-bifurcation-lean/chemotaxisbifurcation-classicalminimalestimates-exp-representation`	`ChemotaxisBifurcation.MinimalFlux.minimal_exp_representation` `ChemotaxisBifurcation.MinimalFlux.eq_left_of_hasDerivAt_zero` `ChemotaxisBifurcation.ClassicalMinimalEstimates.exp_representation`	verified verified verified	—	Literal minimal PDE derives flux at m=1; integrating-factor continuity follows from actual signal regularity and1+v>0. The exact exponential representation is concluded. Source locator: p. 29, TeX line 2765.
Remark 1.3(2) (local-mass)	Uniformly small local mass	Same assumptions	`chemotaxis-bifurcation-lean/chemotaxisbifurcation-nodiracmass-window-mass-bounds` `chemotaxis-bifurcation-lean/chemotaxisbifurcation-nodiracmass-window-mass-tendstouniformly` `chemotaxis-bifurcation-lean/chemotaxisbifurcation-nodiracmass-window` `chemotaxis-bifurcation-lean/chemotaxisbifurcation-nodiracmass-window-integral-eq` `chemotaxis-bifurcation-lean/chemotaxisbifurcation-nodiracmass-tendstouniformly-zero-of-nonneg` `chemotaxis-bifurcation-lean/chemotaxisbifurcation-nodiracmass-uniform-mass-tendsto-zero` `chemotaxis-bifurcation-lean/chemotaxisbifurcation-localizedmassbounds-local-mass-le-power-moment` `chemotaxis-bifurcation-lean/chemotaxisbifurcation-localizedmassbounds-uniform-small-mass` `chemotaxis-bifurcation-lean/chemotaxisbifurcation-intervalmoments-logistic-interval-bounds` `chemotaxis-bifurcation-lean/chemotaxisbifurcation-localizedmassbounds-local-mass-le-uniform-bound` `chemotaxis-bifurcation-lean/chemotaxisbifurcation-stationarymassidentity-classicalprofile-window-mass-bounds` `chemotaxis-bifurcation-lean/chemotaxisbifurcation-stationarymassidentity-window-mass-decay-of-classical-profiles`	`ChemotaxisBifurcation.NoDiracMass.window_mass_bounds` `ChemotaxisBifurcation.NoDiracMass.window_mass_tendstoUniformly` `ChemotaxisBifurcation.NoDiracMass.window` `ChemotaxisBifurcation.NoDiracMass.window_integral_eq` `ChemotaxisBifurcation.NoDiracMass.tendstoUniformly_zero_of_nonneg` `ChemotaxisBifurcation.NoDiracMass.uniform_mass_tendsto_zero` `ChemotaxisBifurcation.LocalizedMassBounds.local_mass_le_power_moment` `ChemotaxisBifurcation.LocalizedMassBounds.uniform_small_mass` `ChemotaxisBifurcation.IntervalMoments.logistic_interval_bounds` `ChemotaxisBifurcation.LocalizedMassBounds.local_mass_le_uniform_bound` `ChemotaxisBifurcation.StationaryMassIdentity.ClassicalProfile.window_mass_bounds` `ChemotaxisBifurcation.StationaryMassIdentity.window_mass_decay_of_classical_profiles`	verified verified verified verified verified verified verified verified verified verified verified verified	—	ClassicalProfile.window_mass_bounds states both the exact Holder-type displayed inequality and its strict equilibrium envelope; mass balance is derived. window_mass_decay_of_classical_profiles proves uniform decay in the family index and center. This covers the quantitative local-mass row end to end for given profiles. Source locator: p. 11, TeX line 1019.
Theorem 1.3(3) (part-3-concentration)	Concentration at an endpoint along the global branch	Same assumptions	`chemotaxis-bifurcation-lean/chemotaxisbifurcation-intervalconcentration-tendsto-integral-left-of-antitoneon` `chemotaxis-bifurcation-lean/chemotaxisbifurcation-intervalconcentration-tendsto-integral-right-of-monotoneon` `chemotaxis-bifurcation-lean/chemotaxisbifurcation-intervalconcentration-tendsto-integral-left` `chemotaxis-bifurcation-lean/chemotaxisbifurcation-intervalconcentration-tendsto-integral-right` `chemotaxis-bifurcation-lean/chemotaxisbifurcation-intervalconcentration-tendsto-dirac-left` `chemotaxis-bifurcation-lean/chemotaxisbifurcation-intervalconcentration-tendsto-dirac-right` `chemotaxis-bifurcation-lean/chemotaxisbifurcation-intervalconcentration-peak-tendsto-attop-left` `chemotaxis-bifurcation-lean/chemotaxisbifurcation-intervalconcentration-peak-tendsto-attop-right` `chemotaxis-bifurcation-lean/chemotaxisbifurcation-intervalconcentration-max-tendsto-attop-left` `chemotaxis-bifurcation-lean/chemotaxisbifurcation-intervalconcentration-densityfinitemeasure` `chemotaxis-bifurcation-lean/chemotaxisbifurcation-intervalconcentration-densitymeasure` `chemotaxis-bifurcation-lean/chemotaxisbifurcation-intervalconcentration-densityonreal` `chemotaxis-bifurcation-lean/chemotaxisbifurcation-intervalconcentration-densityfinitemeasure-mass` `chemotaxis-bifurcation-lean/chemotaxisbifurcation-intervalconcentration-integral-densitymeasure` `chemotaxis-bifurcation-lean/chemotaxisbifurcation-intervalconcentration-compl-subset-of-left` `chemotaxis-bifurcation-lean/chemotaxisbifurcation-intervalconcentration-compl-subset-of-right` `chemotaxis-bifurcation-lean/chemotaxisbifurcation-intervalconcentration-tail-le-of-antitoneon` `chemotaxis-bifurcation-lean/chemotaxisbifurcation-intervalconcentration-head-le-of-monotoneon` `chemotaxis-bifurcation-lean/chemotaxisbifurcation-intervalconcentration-tendsto-tail-of-antitoneon` `chemotaxis-bifurcation-lean/chemotaxisbifurcation-intervalconcentration-tendsto-head-of-monotoneon` `chemotaxis-bifurcation-lean/chemotaxisbifurcation-intervalconcentration-testfunction` `chemotaxis-bifurcation-lean/chemotaxisbifurcation-endpointconcentration-tendsto-mass-smul-dirac-of-vanishing-tails` `chemotaxis-bifurcation-lean/chemotaxisbifurcation-endpointconcentration-tendsto-integral-test-of-vanishing-tails` `chemotaxis-bifurcation-lean/chemotaxisbifurcation-endpointconcentration-peak-tendsto-attop-of-mass-tail-window-bounds` `chemotaxis-bifurcation-lean/chemotaxisbifurcation-physicalendpointconcentration-decreasing-actual-concentration` `chemotaxis-bifurcation-lean/chemotaxisbifurcation-physicalendpointconcentration-increasing-actual-concentration`	`ChemotaxisBifurcation.IntervalConcentration.tendsto_integral_left_of_antitoneOn` `ChemotaxisBifurcation.IntervalConcentration.tendsto_integral_right_of_monotoneOn` `ChemotaxisBifurcation.IntervalConcentration.tendsto_integral_left` `ChemotaxisBifurcation.IntervalConcentration.tendsto_integral_right` `ChemotaxisBifurcation.IntervalConcentration.tendsto_dirac_left` `ChemotaxisBifurcation.IntervalConcentration.tendsto_dirac_right` `ChemotaxisBifurcation.IntervalConcentration.peak_tendsto_atTop_left` `ChemotaxisBifurcation.IntervalConcentration.peak_tendsto_atTop_right` `ChemotaxisBifurcation.IntervalConcentration.max_tendsto_atTop_left` `ChemotaxisBifurcation.IntervalConcentration.densityFiniteMeasure` `ChemotaxisBifurcation.IntervalConcentration.densityMeasure` `ChemotaxisBifurcation.IntervalConcentration.densityOnReal` `ChemotaxisBifurcation.IntervalConcentration.densityFiniteMeasure_mass` `ChemotaxisBifurcation.IntervalConcentration.integral_densityMeasure` `ChemotaxisBifurcation.IntervalConcentration.compl_subset_of_left` `ChemotaxisBifurcation.IntervalConcentration.compl_subset_of_right` `ChemotaxisBifurcation.IntervalConcentration.tail_le_of_antitoneOn` `ChemotaxisBifurcation.IntervalConcentration.head_le_of_monotoneOn` `ChemotaxisBifurcation.IntervalConcentration.tendsto_tail_of_antitoneOn` `ChemotaxisBifurcation.IntervalConcentration.tendsto_head_of_monotoneOn` `ChemotaxisBifurcation.IntervalConcentration.testFunction` `ChemotaxisBifurcation.EndpointConcentration.tendsto_mass_smul_dirac_of_vanishing_tails` `ChemotaxisBifurcation.EndpointConcentration.tendsto_integral_test_of_vanishing_tails` `ChemotaxisBifurcation.EndpointConcentration.peak_tendsto_atTop_of_mass_tail_window_bounds` `ChemotaxisBifurcation.PhysicalEndpointConcentration.decreasing_actual_concentration` `ChemotaxisBifurcation.PhysicalEndpointConcentration.increasing_actual_concentration`	verified verified verified verified verified verified verified verified verified verified verified verified verified verified verified verified verified verified verified verified verified verified verified verified verified verified	—	Exact public scope, hypotheses and exclusions: data/public-scope-ledger.json, row paper3/T:global-extension/part-3-concentration. This display summary does not extend that scope. Source locator: p. 10, TeX line 933.
Theorem 1.1	Two continuous branch curves of the reduced equation	Inputs supplied	`chemotaxis-bifurcation-lean/chemotaxisbifurcation-branchcurves-branch-curves` `chemotaxis-bifurcation-lean/chemotaxisbifurcation-branchcurves-center-ode-final-branch-curves` `chemotaxis-bifurcation-lean/chemotaxisbifurcation-branchcurves-branchroot-existsunique` `chemotaxis-bifurcation-lean/chemotaxisbifurcation-branchcurves-small-roots-classification` `chemotaxis-bifurcation-lean/chemotaxisbifurcation-branchcurves-branch-continuouson` `chemotaxis-bifurcation-lean/chemotaxisbifurcation-branchcurves-branch-tendsto-zero` `chemotaxis-bifurcation-lean/chemotaxisbifurcation-branchcurves-branch-zero` `chemotaxis-bifurcation-lean/chemotaxisbifurcation-branchcurves-branch-spec` `chemotaxis-bifurcation-lean/chemotaxisbifurcation-branchcurves-branch-eq-zero-of-not-side` `chemotaxis-bifurcation-lean/chemotaxisbifurcation-branchcurves-root-localize` `chemotaxis-bifurcation-lean/chemotaxisbifurcation-branchcurves-scaled-field-strictantion` `chemotaxis-bifurcation-lean/chemotaxisbifurcation-branchcurves-branch` `chemotaxis-bifurcation-lean/chemotaxisbifurcation-branchcurves-branchroot` `chemotaxis-bifurcation-lean/chemotaxisbifurcation-branchcurves-curvesmall` `chemotaxis-bifurcation-lean/chemotaxisbifurcation-branchcurves-branchradius` `chemotaxis-bifurcation-lean/chemotaxisbifurcation-branchcurves-amperr` `chemotaxis-bifurcation-lean/chemotaxisbifurcation-branchcurves-curvesmall-mem-nhds` `chemotaxis-bifurcation-lean/chemotaxisbifurcation-branchderivativeasymptotic-branch-derivative-error-bound` `chemotaxis-bifurcation-lean/chemotaxisbifurcation-branchderivativeasymptotic-branch-derivative-islittleo` `chemotaxis-bifurcation-lean/chemotaxisbifurcation-branchcurves-branchroot-existsunique-eventually` `chemotaxis-bifurcation-lean/chemotaxisbifurcation-branchderivativeasymptotic-equilibrium-derivative-error` `chemotaxis-bifurcation-lean/chemotaxisbifurcation-branchderivativeasymptotic-equilibrium-derivative-error-window`	`ChemotaxisBifurcation.BranchCurves.branch_curves` `ChemotaxisBifurcation.BranchCurves.center_ODE_final_branch_curves` `ChemotaxisBifurcation.BranchCurves.branchRoot_existsUnique` `ChemotaxisBifurcation.BranchCurves.small_roots_classification` `ChemotaxisBifurcation.BranchCurves.branch_continuousOn` `ChemotaxisBifurcation.BranchCurves.branch_tendsto_zero` `ChemotaxisBifurcation.BranchCurves.branch_zero` `ChemotaxisBifurcation.BranchCurves.branch_spec` `ChemotaxisBifurcation.BranchCurves.branch_eq_zero_of_not_side` `ChemotaxisBifurcation.BranchCurves.root_localize` `ChemotaxisBifurcation.BranchCurves.scaled_field_strictAntiOn` `ChemotaxisBifurcation.BranchCurves.branch` `ChemotaxisBifurcation.BranchCurves.BranchRoot` `ChemotaxisBifurcation.BranchCurves.CurveSmall` `ChemotaxisBifurcation.BranchCurves.branchRadius` `ChemotaxisBifurcation.BranchCurves.ampErr` `ChemotaxisBifurcation.BranchCurves.curveSmall_mem_nhds` `ChemotaxisBifurcation.BranchDerivativeAsymptotic.branch_derivative_error_bound` `ChemotaxisBifurcation.BranchDerivativeAsymptotic.branch_derivative_isLittleO` `ChemotaxisBifurcation.BranchCurves.branchRoot_existsUnique_eventually` `ChemotaxisBifurcation.BranchDerivativeAsymptotic.equilibrium_derivative_error` `ChemotaxisBifurcation.BranchDerivativeAsymptotic.equilibrium_derivative_error_window`	verified verified verified verified verified verified verified verified verified verified verified verified verified verified verified verified verified verified verified verified verified verified	identification of the scalar reduced field and its coefficients α>0 and β≠0 a common box with C≥0 and 0<r≤1 the stated value remainder bound HasDerivAt identifying Rs the stated derivative remainder bound continuity in η for every fixed small s. Center-manifold construction and lifting to PDE curves remain excluded	Exact public scope, hypotheses and exclusions: data/public-scope-ledger.json, row paper3/T:local-bifurcation/branch-curves. This display summary does not extend that scope. Source locator: p. 6, TeX line 580. arXiv v2 note: Step 5 of the v2 proof drops the derivative remainder estimate; see the ledger row’s arxiv_v2_note.
Lemma 2.1 and Equation 2.17	Cosine-series bridge for the Neumann phase space	Same assumptions	`chemotaxis-bifurcation-lean/chemotaxisbifurcation-cosinecoefficients-neumannw21` `chemotaxis-bifurcation-lean/chemotaxisbifurcation-cosinecoefficients-cosinecoeff` `chemotaxis-bifurcation-lean/chemotaxisbifurcation-cosinecoefficients-summable-norm-cosinecoeff` `chemotaxis-bifurcation-lean/chemotaxisbifurcation-cosinecoefficients-hassum-cosinecoeff` `chemotaxis-bifurcation-lean/chemotaxisbifurcation-cosinecoefficients-cosinecoeff-eq-neg-mul-secondderiv` `chemotaxis-bifurcation-lean/chemotaxisbifurcation-cosinecoefficients-abs-cosinecoeff-le` `chemotaxis-bifurcation-lean/chemotaxisbifurcation-cosinecoefficients-cosine-sine-sine-of-neumann` `chemotaxis-bifurcation-lean/chemotaxisbifurcation-cosinecoefficients-two-cosines-two-sines-of-neumann` `chemotaxis-bifurcation-lean/chemotaxisbifurcation-cosinecoefficients-cos-cos-cos-of-neumann` `chemotaxis-bifurcation-lean/chemotaxisbifurcation-cosinecoefficients-cos-cos-cos-cos-of-neumann` `chemotaxis-bifurcation-lean/chemotaxisbifurcation-cosinecoefficients-fouriercoeff-evenperiodic` `chemotaxis-bifurcation-lean/chemotaxisbifurcation-cosinecoefficients-integral-mul-cos-eq` `chemotaxis-bifurcation-lean/chemotaxisbifurcation-h2cosineidentities-representative-with-actual-coefficients` `chemotaxis-bifurcation-lean/chemotaxisbifurcation-h2cosineidentities-hassum-of-h2-continuous` `chemotaxis-bifurcation-lean/chemotaxisbifurcation-h2cosineidentities-cosine-sine-sine-of-h2` `chemotaxis-bifurcation-lean/chemotaxisbifurcation-h2cosineidentities-two-cosines-two-sines-of-h2` `chemotaxis-bifurcation-lean/chemotaxisbifurcation-h2cosineidentities-cos-cos-cos-of-h2` `chemotaxis-bifurcation-lean/chemotaxisbifurcation-h2cosineidentities-cos-cos-cos-cos-of-h2`	`ChemotaxisBifurcation.CosineCoefficients.NeumannW21` `ChemotaxisBifurcation.CosineCoefficients.cosineCoeff` `ChemotaxisBifurcation.CosineCoefficients.summable_norm_cosineCoeff` `ChemotaxisBifurcation.CosineCoefficients.hasSum_cosineCoeff` `ChemotaxisBifurcation.CosineCoefficients.cosineCoeff_eq_neg_mul_secondDeriv` `ChemotaxisBifurcation.CosineCoefficients.abs_cosineCoeff_le` `ChemotaxisBifurcation.CosineCoefficients.cosine_sine_sine_of_neumann` `ChemotaxisBifurcation.CosineCoefficients.two_cosines_two_sines_of_neumann` `ChemotaxisBifurcation.CosineCoefficients.cos_cos_cos_of_neumann` `ChemotaxisBifurcation.CosineCoefficients.cos_cos_cos_cos_of_neumann` `ChemotaxisBifurcation.CosineCoefficients.fourierCoeff_evenPeriodic` `ChemotaxisBifurcation.CosineCoefficients.integral_mul_cos_eq` `ChemotaxisBifurcation.H2CosineIdentities.representative_with_actual_coefficients` `ChemotaxisBifurcation.H2CosineIdentities.hasSum_of_H2_continuous` `ChemotaxisBifurcation.H2CosineIdentities.cosine_sine_sine_of_H2` `ChemotaxisBifurcation.H2CosineIdentities.two_cosines_two_sines_of_H2` `ChemotaxisBifurcation.H2CosineIdentities.cos_cos_cos_of_H2` `ChemotaxisBifurcation.H2CosineIdentities.cos_cos_cos_cos_of_H2`	verified verified verified verified verified verified verified verified verified verified verified verified verified verified verified verified verified verified	—	Exact public scope, hypotheses and exclusions: data/public-scope-ledger.json, row paper3/L:trig-integrals/phase-space-bridge. This display summary does not extend that scope. Source locator: p. 13, TeX line 1153.
Proof of Lemma 4.2(2), Equations 4.7-4.8	Signal bounds in the minimal model	Same assumptions	`chemotaxis-bifurcation-lean/chemotaxisbifurcation-spikeestimates-signal-flux-eq` `chemotaxis-bifurcation-lean/chemotaxisbifurcation-spikeestimates-signal-mass-eq` `chemotaxis-bifurcation-lean/chemotaxisbifurcation-spikeestimates-signal-gradient-le` `chemotaxis-bifurcation-lean/chemotaxisbifurcation-spikeestimates-signal-gradient-le-two` `chemotaxis-bifurcation-lean/chemotaxisbifurcation-spikeestimates-signal-sup-le` `chemotaxis-bifurcation-lean/chemotaxisbifurcation-spikeestimates-signal-second-l1-le` `chemotaxis-bifurcation-lean/chemotaxisbifurcation-spikeestimates-signal-sobolev-le` `chemotaxis-bifurcation-lean/chemotaxisbifurcation-localizedmassbounds-signal-parameter-factors` `chemotaxis-bifurcation-lean/chemotaxisbifurcation-classicalminimalestimates-signal-sobolev-bound`	`ChemotaxisBifurcation.SpikeEstimates.signal_flux_eq` `ChemotaxisBifurcation.SpikeEstimates.signal_mass_eq` `ChemotaxisBifurcation.SpikeEstimates.signal_gradient_le` `ChemotaxisBifurcation.SpikeEstimates.signal_gradient_le_two` `ChemotaxisBifurcation.SpikeEstimates.signal_sup_le` `ChemotaxisBifurcation.SpikeEstimates.signal_second_L1_le` `ChemotaxisBifurcation.SpikeEstimates.signal_sobolev_le` `ChemotaxisBifurcation.LocalizedMassBounds.signal_parameter_factors` `ChemotaxisBifurcation.ClassicalMinimalEstimates.signal_sobolev_bound`	verified verified verified verified verified verified verified verified verified	—	Actual second PDE and both Neumann conditions supply the exact signal sup-plus-L1 component bound and displayed constant; no separately assumed signal estimate. Source locator: p. 29, TeX line 2709.
Proof of Lemma 4.2(2): the uniform bounds on u and u_x from the flux identity (4.14), before the elliptic step to (4.13) (alternative estimate for 1<=m<2)	Sup bound for 0 < m < 2 in the minimal model	Same assumptions	`chemotaxis-bifurcation-lean/chemotaxisbifurcation-spikeestimates-minimal-sup-bounds` `chemotaxis-bifurcation-lean/chemotaxisbifurcation-spikeestimates-sensitivity-le` `chemotaxis-bifurcation-lean/chemotaxisbifurcation-spikeestimates-flux-abs-le` `chemotaxis-bifurcation-lean/chemotaxisbifurcation-spikeestimates-exists-le-mean` `chemotaxis-bifurcation-lean/chemotaxisbifurcation-spikeestimates-le-add-integral-of-abs-deriv-le` `chemotaxis-bifurcation-lean/chemotaxisbifurcation-classicalminimalestimates-sup-bounds`	`ChemotaxisBifurcation.SpikeEstimates.minimal_sup_bounds` `ChemotaxisBifurcation.SpikeEstimates.sensitivity_le` `ChemotaxisBifurcation.SpikeEstimates.flux_abs_le` `ChemotaxisBifurcation.SpikeEstimates.exists_le_mean` `ChemotaxisBifurcation.SpikeEstimates.le_add_integral_of_abs_deriv_le` `ChemotaxisBifurcation.ClassicalMinimalEstimates.sup_bounds`	verified verified verified verified verified verified	—	Literal minimal PDE derives flux; actual signal PDE derives gradient; M is the actual gamma moment. The complete original sharp power envelope and derivative estimate hold for0<m<2. Source locator: p. 30, TeX line 2793.
Proof of Lemma 4.2(2), m=1 case	Sup bound for m = 1 in the minimal model	Same assumptions	`chemotaxis-bifurcation-lean/chemotaxisbifurcation-spikeestimates-minimal-exp-sup-bound` `chemotaxis-bifurcation-lean/chemotaxisbifurcation-classicalminimalestimates-exp-sup-bound`	`ChemotaxisBifurcation.SpikeEstimates.minimal_exp_sup_bound` `ChemotaxisBifurcation.ClassicalMinimalEstimates.exp_sup_bound`	verified verified	—	Actual PDEs and prescribed mass derive flux, signal-gradient and integrating-factor regularity; the exact historical exponential supremum envelope follows for m=1. Source locator: p. 29, TeX line 2765.
Lemma 4.1(2), Equation 4.11 (alternative route for 1<=m<(alpha+2)/2)	Gradient bound chain in the non-minimal model	Same assumptions	`chemotaxis-bifurcation-lean/chemotaxisbifurcation-spikeestimates-logistic-gradient-le` `chemotaxis-bifurcation-lean/chemotaxisbifurcation-spikeestimates-logistic-energy-identity` `chemotaxis-bifurcation-lean/chemotaxisbifurcation-spikeestimates-logistic-energy-ineq` `chemotaxis-bifurcation-lean/chemotaxisbifurcation-spikeestimates-energyconstant` `chemotaxis-bifurcation-lean/chemotaxisbifurcation-spikeestimates-logistic-gradient-l2-le` `chemotaxis-bifurcation-lean/chemotaxisbifurcation-spikeestimates-logistic-sup-le` `chemotaxis-bifurcation-lean/chemotaxisbifurcation-spikeestimates-logistic-first-integral` `chemotaxis-bifurcation-lean/chemotaxisbifurcation-spikeestimates-logistic-f-bound` `chemotaxis-bifurcation-lean/chemotaxisbifurcation-spikeestimates-logistic-c1-bound` `chemotaxis-bifurcation-lean/chemotaxisbifurcation-spikeestimates-logistic-c1-chain` `chemotaxis-bifurcation-lean/chemotaxisbifurcation-spikeestimates-young-rpow` `chemotaxis-bifurcation-lean/chemotaxisbifurcation-spikeestimates-integral-abs-sq-le` `chemotaxis-bifurcation-lean/chemotaxisbifurcation-classicallogisticestimates-c1-bound` `chemotaxis-bifurcation-lean/chemotaxisbifurcation-classicallogisticestimates-c1-gronwall-bound` `chemotaxis-bifurcation-lean/chemotaxisbifurcation-spikeestimates-sup-le-of-derivative-power-bound`	`ChemotaxisBifurcation.SpikeEstimates.logistic_gradient_le` `ChemotaxisBifurcation.SpikeEstimates.logistic_energy_identity` `ChemotaxisBifurcation.SpikeEstimates.logistic_energy_ineq` `ChemotaxisBifurcation.SpikeEstimates.energyConstant` `ChemotaxisBifurcation.SpikeEstimates.logistic_gradient_L2_le` `ChemotaxisBifurcation.SpikeEstimates.logistic_sup_le` `ChemotaxisBifurcation.SpikeEstimates.logistic_first_integral` `ChemotaxisBifurcation.SpikeEstimates.logistic_F_bound` `ChemotaxisBifurcation.SpikeEstimates.logistic_C1_bound` `ChemotaxisBifurcation.SpikeEstimates.logistic_C1_chain` `ChemotaxisBifurcation.SpikeEstimates.young_rpow` `ChemotaxisBifurcation.SpikeEstimates.integral_abs_sq_le` `ChemotaxisBifurcation.ClassicalLogisticEstimates.c1_bound` `ChemotaxisBifurcation.ClassicalLogisticEstimates.c1_gronwall_bound` `ChemotaxisBifurcation.SpikeEstimates.sup_le_of_derivative_power_bound`	verified verified verified verified verified verified verified verified verified verified verified verified verified verified verified	—	Exact public scope, hypotheses and exclusions: data/public-scope-ledger.json, row paper3/L:spiky-solu-lm1/part-2-C1-chain. This display summary does not extend that scope. Source locator: p. 29, TeX line 2738.
Proof of Lemma 5.1, W^{2,q} step with r=1+alpha	W^{2,q} bound for the signal (step in the proof of Lemma 5.1)	Same assumptions	`chemotaxis-bifurcation-lean/chemotaxisbifurcation-spikeestimates-logistic-w2q-bound` `chemotaxis-bifurcation-lean/chemotaxisbifurcation-classicallogisticestimates-w2q-bound` `chemotaxis-bifurcation-lean/chemotaxisbifurcation-spikeestimates-signal-testing-rpow-pos`	`ChemotaxisBifurcation.SpikeEstimates.logistic_W2q_bound` `ChemotaxisBifurcation.ClassicalLogisticEstimates.w2q_bound` `ChemotaxisBifurcation.SpikeEstimates.signal_testing_rpow_pos`	verified verified verified	—	retained auxiliary quantitative W2q deduction for actual given classical profiles: actual testing, Holder, Minkowski and population moment premises are all discharged in ClassicalLogisticEstimates.w2q_bound. The old part3 name is historical; frozen v2 Lemma4.1(p28) has no part3. Do not present this auxiliary as a current numbered part3 theorem. Source locator: p. 34, TeX line 3155.
Remark 1.3(2) (no-atom-limit)	No atom in the limit measure	Same assumptions	`chemotaxis-bifurcation-lean/chemotaxisbifurcation-noatomlimit-densityfinitemeasure-singleton-eq-zero` `chemotaxis-bifurcation-lean/chemotaxisbifurcation-noatomlimit-not-tendsto-smul-dirac` `chemotaxis-bifurcation-lean/chemotaxisbifurcation-noatomlimit-not-subseq-tendsto-smul-dirac` `chemotaxis-bifurcation-lean/chemotaxisbifurcation-noatomlimit-measure-singleton-eq-zero-of-small-balls` `chemotaxis-bifurcation-lean/chemotaxisbifurcation-noatomlimit-densityfinitemeasure-ball` `chemotaxis-bifurcation-lean/chemotaxisbifurcation-noatomlimit-ball-eq-preimage` `chemotaxis-bifurcation-lean/chemotaxisbifurcation-noatomlimit-smul-dirac-singleton` `chemotaxis-bifurcation-lean/chemotaxisbifurcation-stationarymassidentity-no-atoms-of-classical-profiles` `chemotaxis-bifurcation-lean/chemotaxisbifurcation-stationarymassidentity-no-dirac-subsequence-of-classical-profiles`	`ChemotaxisBifurcation.NoAtomLimit.densityFiniteMeasure_singleton_eq_zero` `ChemotaxisBifurcation.NoAtomLimit.not_tendsto_smul_dirac` `ChemotaxisBifurcation.NoAtomLimit.not_subseq_tendsto_smul_dirac` `ChemotaxisBifurcation.NoAtomLimit.measure_singleton_eq_zero_of_small_balls` `ChemotaxisBifurcation.NoAtomLimit.densityFiniteMeasure_ball` `ChemotaxisBifurcation.NoAtomLimit.ball_eq_preimage` `ChemotaxisBifurcation.NoAtomLimit.smul_dirac_singleton` `ChemotaxisBifurcation.StationaryMassIdentity.no_atoms_of_classical_profiles` `ChemotaxisBifurcation.StationaryMassIdentity.no_dirac_subsequence_of_classical_profiles`	verified verified verified verified verified verified verified verified verified	—	Exact public scope, hypotheses and exclusions: data/public-scope-ledger.json, row paper3/R:no-delta-concentration/no-atom-limit. This display summary does not extend that scope. Source locator: p. 11, TeX line 1019.
Lemma 5.1 (deductions)	Deductions of the constant-limit lemma	Same assumptions	`chemotaxis-bifurcation-lean/chemotaxisbifurcation-spikelimit-minimal-spike-limit` `chemotaxis-bifurcation-lean/chemotaxisbifurcation-spikelimit-limit-eq-const` `chemotaxis-bifurcation-lean/chemotaxisbifurcation-spikelimit-weaklimit-ae-zero` `chemotaxis-bifurcation-lean/chemotaxisbifurcation-spikelimit-ae-mul-eq-zero-of-intervals` `chemotaxis-bifurcation-lean/chemotaxisbifurcation-spikelimit-energy-const` `chemotaxis-bifurcation-lean/chemotaxisbifurcation-spikelimit-eq-const-of-energy` `chemotaxis-bifurcation-lean/chemotaxisbifurcation-spikelimit-deriv-eq-zero-of-extremum` `chemotaxis-bifurcation-lean/chemotaxisbifurcation-spikelimit-flux-test-bound` `chemotaxis-bifurcation-lean/chemotaxisbifurcation-spikelimit-tendsto-integral-rpow-zero` `chemotaxis-bifurcation-lean/chemotaxisbifurcation-spikelimit-rpow-le-three-term` `chemotaxis-bifurcation-lean/chemotaxisbifurcation-spikelimit-tendsto-zero-of-mul-le` `chemotaxis-bifurcation-lean/chemotaxisbifurcation-spikelimit-kappa-le-of-le` `chemotaxis-bifurcation-lean/chemotaxisbifurcation-spikelimit-exists-sign-pos` `chemotaxis-bifurcation-lean/chemotaxisbifurcation-classicalspikesubsequence-exists-constant-signal-and-weak-tests` `chemotaxis-bifurcation-lean/chemotaxisbifurcation-signalcompactness-exists-c1-subsequence-of-w2q-bound` `chemotaxis-bifurcation-lean/chemotaxisbifurcation-signaldirectlimit-gradient-eq-zero-of-local-signal-ode` `chemotaxis-bifurcation-lean/chemotaxisbifurcation-signaldirectlimit-constant-limit-without-weak-source` `chemotaxis-bifurcation-lean/chemotaxisbifurcation-signalpowermoment-w2q-bound-of-power-moment` `chemotaxis-bifurcation-lean/chemotaxisbifurcation-signalpowermoment-exists-c1-subsequence-of-power-moment` `chemotaxis-bifurcation-lean/chemotaxisbifurcation-spikelimit-source-integral-tendsto-zero-of-nonzero-limit-gradient`	`ChemotaxisBifurcation.SpikeLimit.minimal_spike_limit` `ChemotaxisBifurcation.SpikeLimit.limit_eq_const` `ChemotaxisBifurcation.SpikeLimit.weakLimit_ae_zero` `ChemotaxisBifurcation.SpikeLimit.ae_mul_eq_zero_of_intervals` `ChemotaxisBifurcation.SpikeLimit.energy_const` `ChemotaxisBifurcation.SpikeLimit.eq_const_of_energy` `ChemotaxisBifurcation.SpikeLimit.deriv_eq_zero_of_extremum` `ChemotaxisBifurcation.SpikeLimit.flux_test_bound` `ChemotaxisBifurcation.SpikeLimit.tendsto_integral_rpow_zero` `ChemotaxisBifurcation.SpikeLimit.rpow_le_three_term` `ChemotaxisBifurcation.SpikeLimit.tendsto_zero_of_mul_le` `ChemotaxisBifurcation.SpikeLimit.kappa_le_of_le` `ChemotaxisBifurcation.SpikeLimit.exists_sign_pos` `ChemotaxisBifurcation.ClassicalSpikeSubsequence.exists_constant_signal_and_weak_tests` `ChemotaxisBifurcation.SignalCompactness.exists_C1_subsequence_of_W2q_bound` `ChemotaxisBifurcation.SignalDirectLimit.gradient_eq_zero_of_local_signal_ode` `ChemotaxisBifurcation.SignalDirectLimit.constant_limit_without_weak_source` `ChemotaxisBifurcation.SignalPowerMoment.W2q_bound_of_power_moment` `ChemotaxisBifurcation.SignalPowerMoment.exists_C1_subsequence_of_power_moment` `ChemotaxisBifurcation.SpikeLimit.source_integral_tendsto_zero_of_nonzero_limit_gradient`	verified verified verified verified verified verified verified verified verified verified verified verified verified verified verified verified verified verified verified verified	—	Exact public scope, hypotheses and exclusions: data/public-scope-ledger.json, row paper3/L:minimal-spike-limit/deductions. This display summary does not extend that scope. Source locator: p. 34, TeX line 3155.
Theorem 1.4 (deductions)	Deductions of the spike theorem	Same assumptions	`chemotaxis-bifurcation-lean/chemotaxisbifurcation-spikelimit-spike-gradient-blowup` `chemotaxis-bifurcation-lean/chemotaxisbifurcation-spikelimit-blowup-contradiction` `chemotaxis-bifurcation-lean/chemotaxisbifurcation-spikelimit-le-of-local-gradient-bound` `chemotaxis-bifurcation-lean/chemotaxisbifurcation-spikelimit-spike-limit-constant-le` `chemotaxis-bifurcation-lean/chemotaxisbifurcation-spikelimit-spike-limit-nonminimal` `chemotaxis-bifurcation-lean/chemotaxisbifurcation-spikelimit-gradient-blowup-subseq` `chemotaxis-bifurcation-lean/chemotaxisbifurcation-spikelimit-exponent-admissible` `chemotaxis-bifurcation-lean/chemotaxisbifurcation-spikelimit-power-integral-le-of-le-one` `chemotaxis-bifurcation-lean/chemotaxisbifurcation-spikelimit-power-integral-le-of-one-le` `chemotaxis-bifurcation-lean/chemotaxisbifurcation-spikelimit-eqon-const-of-integral-eq` `chemotaxis-bifurcation-lean/chemotaxisbifurcation-classicalspikeblowup-minimal-gradient-blowup` `chemotaxis-bifurcation-lean/chemotaxisbifurcation-classicalspikeblowup-logistic-gradient-blowup-of-eventual-peak` `chemotaxis-bifurcation-lean/chemotaxisbifurcation-classicalspikeblowup-logistic-spike-all-tests-of-eventual-peak`	`ChemotaxisBifurcation.SpikeLimit.spike_gradient_blowup` `ChemotaxisBifurcation.SpikeLimit.blowup_contradiction` `ChemotaxisBifurcation.SpikeLimit.le_of_local_gradient_bound` `ChemotaxisBifurcation.SpikeLimit.spike_limit_constant_le` `ChemotaxisBifurcation.SpikeLimit.spike_limit_nonminimal` `ChemotaxisBifurcation.SpikeLimit.gradient_blowup_subseq` `ChemotaxisBifurcation.SpikeLimit.exponent_admissible` `ChemotaxisBifurcation.SpikeLimit.power_integral_le_of_le_one` `ChemotaxisBifurcation.SpikeLimit.power_integral_le_of_one_le` `ChemotaxisBifurcation.SpikeLimit.eqOn_const_of_integral_eq` `ChemotaxisBifurcation.ClassicalSpikeBlowup.minimal_gradient_blowup` `ChemotaxisBifurcation.ClassicalSpikeBlowup.logistic_gradient_blowup_of_eventual_peak` `ChemotaxisBifurcation.ClassicalSpikeBlowup.logistic_spike_all_tests_of_eventual_peak`	verified verified verified verified verified verified verified verified verified verified verified verified verified	—	Exact public scope, hypotheses and exclusions: data/public-scope-ledger.json, row paper3/T:spiky-solu-thm/deductions. This display summary does not extend that scope. Source locator: p. 11, TeX line 991.
Theorem 1.3(1)-(3)	Logical deductions of the global extension theorem	Inputs supplied	`chemotaxis-bifurcation-lean/chemotaxisbifurcation-globalbranch-part3-global` `chemotaxis-bifurcation-lean/chemotaxisbifurcation-globalbranch-part2-ssup-eq-top` `chemotaxis-bifurcation-lean/chemotaxisbifurcation-globalbranch-not-iscompact-of-alternatives` `chemotaxis-bifurcation-lean/chemotaxisbifurcation-globalbranch-iscompact-slice` `chemotaxis-bifurcation-lean/chemotaxisbifurcation-globalbranch-unbounded-of-not-iscompact` `chemotaxis-bifurcation-lean/chemotaxisbifurcation-globalbranch-ssup-eq-top-of-unbounded` `chemotaxis-bifurcation-lean/chemotaxisbifurcation-globalbranch-selectedimage-properties` `chemotaxis-bifurcation-lean/chemotaxisbifurcation-globalbranch-mode-one-strictantion` `chemotaxis-bifurcation-lean/chemotaxisbifurcation-globalbranch-mode-not-monotoneon` `chemotaxis-bifurcation-lean/chemotaxisbifurcation-globalbranch-mode-eq-one-of-monotone-limit` `chemotaxis-bifurcation-lean/chemotaxisbifurcation-globalbranch-not-monotone-of-higher-mode` `chemotaxis-bifurcation-lean/chemotaxisbifurcation-globalbranch-integral-mul-mode-one-pos` `chemotaxis-bifurcation-lean/chemotaxisbifurcation-globalbranch-integral-mul-mode-one-neg` `chemotaxis-bifurcation-lean/chemotaxisbifurcation-globalbranch-part3-strictanti` `chemotaxis-bifurcation-lean/chemotaxisbifurcation-globalbranch-part3-strictmono` `chemotaxis-bifurcation-lean/chemotaxisbifurcation-globalbranch-not-altothertrivial` `chemotaxis-bifurcation-lean/chemotaxisbifurcation-globalbranch-not-altcomplement` `chemotaxis-bifurcation-lean/chemotaxisbifurcation-globalbranch-globalalternatives` `chemotaxis-bifurcation-lean/chemotaxisbifurcation-globalbranch-altnoncompact` `chemotaxis-bifurcation-lean/chemotaxisbifurcation-globalbranch-altothertrivial` `chemotaxis-bifurcation-lean/chemotaxisbifurcation-globalbranch-altcomplement` `chemotaxis-bifurcation-lean/chemotaxisbifurcation-boundedsolutionslices-logistic-component-unbounded` `chemotaxis-bifurcation-lean/chemotaxisbifurcation-boundedsolutionslices-minimal-component-unbounded` `chemotaxis-bifurcation-lean/chemotaxisbifurcation-selectedsolutioncomponents-logistic-selected-unbounded` `chemotaxis-bifurcation-lean/chemotaxisbifurcation-selectedsolutioncomponents-minimal-selected-unbounded` `chemotaxis-bifurcation-lean/chemotaxisbifurcation-parametrizedsolutioncomponents-logistic-unbounded-of-local-curve` `chemotaxis-bifurcation-lean/chemotaxisbifurcation-parametrizedsolutioncomponents-minimal-unbounded-of-local-curve` `chemotaxis-bifurcation-lean/chemotaxisbifurcation-fourieramplitude-logistic-unbounded-of-fourier-curve` `chemotaxis-bifurcation-lean/chemotaxisbifurcation-fourieramplitude-minimal-unbounded-of-fourier-curve` `chemotaxis-bifurcation-lean/chemotaxisbifurcation-fouriercomplement-canonicalremainder` `chemotaxis-bifurcation-lean/chemotaxisbifurcation-fouriercomplement-continuous-canonicalremainder` `chemotaxis-bifurcation-lean/chemotaxisbifurcation-fouriercomplement-canonical-profile-expansion` `chemotaxis-bifurcation-lean/chemotaxisbifurcation-fouriercomplement-curve-canonical-expansion`	`ChemotaxisBifurcation.GlobalBranch.part3_global` `ChemotaxisBifurcation.GlobalBranch.part2_sSup_eq_top` `ChemotaxisBifurcation.GlobalBranch.not_isCompact_of_alternatives` `ChemotaxisBifurcation.GlobalBranch.isCompact_slice` `ChemotaxisBifurcation.GlobalBranch.unbounded_of_not_isCompact` `ChemotaxisBifurcation.GlobalBranch.sSup_eq_top_of_unbounded` `ChemotaxisBifurcation.GlobalBranch.selectedImage_properties` `ChemotaxisBifurcation.GlobalBranch.mode_one_strictAntiOn` `ChemotaxisBifurcation.GlobalBranch.mode_not_monotoneOn` `ChemotaxisBifurcation.GlobalBranch.mode_eq_one_of_monotone_limit` `ChemotaxisBifurcation.GlobalBranch.not_monotone_of_higher_mode` `ChemotaxisBifurcation.GlobalBranch.integral_mul_mode_one_pos` `ChemotaxisBifurcation.GlobalBranch.integral_mul_mode_one_neg` `ChemotaxisBifurcation.GlobalBranch.part3_strictAnti` `ChemotaxisBifurcation.GlobalBranch.part3_strictMono` `ChemotaxisBifurcation.GlobalBranch.not_altOtherTrivial` `ChemotaxisBifurcation.GlobalBranch.not_altComplement` `ChemotaxisBifurcation.GlobalBranch.GlobalAlternatives` `ChemotaxisBifurcation.GlobalBranch.AltNoncompact` `ChemotaxisBifurcation.GlobalBranch.AltOtherTrivial` `ChemotaxisBifurcation.GlobalBranch.AltComplement` `ChemotaxisBifurcation.BoundedSolutionSlices.logistic_component_unbounded` `ChemotaxisBifurcation.BoundedSolutionSlices.minimal_component_unbounded` `ChemotaxisBifurcation.SelectedSolutionComponents.logistic_selected_unbounded` `ChemotaxisBifurcation.SelectedSolutionComponents.minimal_selected_unbounded` `ChemotaxisBifurcation.ParametrizedSolutionComponents.logistic_unbounded_of_local_curve` `ChemotaxisBifurcation.ParametrizedSolutionComponents.minimal_unbounded_of_local_curve` `ChemotaxisBifurcation.FourierAmplitude.logistic_unbounded_of_fourier_curve` `ChemotaxisBifurcation.FourierAmplitude.minimal_unbounded_of_fourier_curve` `ChemotaxisBifurcation.FourierComplement.canonicalRemainder` `ChemotaxisBifurcation.FourierComplement.continuous_canonicalRemainder` `ChemotaxisBifurcation.FourierComplement.canonical_profile_expansion` `ChemotaxisBifurcation.FourierComplement.curve_canonical_expansion`	verified verified verified verified verified verified verified verified verified verified verified verified verified verified verified verified verified verified verified verified verified verified verified verified verified verified verified verified verified verified verified verified verified	Shi–Wang unilateral alternatives for the actual selected branches identification of the ambient space, solution set S and admissible set V relative closedness and containment in V and closure S ambient admissibility closure S contained in V precompactness of every bounded-sensitivity slice from the applicable parameter-dependent PDE estimates and compact embedding connectedness and base membership of the selected component relative clopenness of the correctly oriented monotone locus the continuous additive profile representation and constant equilibrium orthogonality of W to the first cosine mode local simple-eigenvalue expansions when applying the higher-mode perturbation lemma	Conditional scope retained. Actual cosine complement, curved elliptic cubic response and conserved-mean coefficient extraction supply the scoped ingredients. Family/jet construction, operator identity and global foundations remain explicit. Public scope and supplied inputs: data/public-scope-ledger.json, paper3/T:global-extension/parts-1-3-logic
Equation (2.43) (remainder-from-jet)	Remainder bounds from the point jet	Inputs supplied	`chemotaxis-bifurcation-lean/chemotaxisbifurcation-remainderfromjet-mixed-interface-of-jet` `chemotaxis-bifurcation-lean/chemotaxisbifurcation-remainderfromjet-final-interface-of-jet` `chemotaxis-bifurcation-lean/chemotaxisbifurcation-remainderfromjet-final-value-bound-iff` `chemotaxis-bifurcation-lean/chemotaxisbifurcation-remainderfromjet-jet-branch-eventually` `chemotaxis-bifurcation-lean/chemotaxisbifurcation-remainderfromjet-jet-branch-curves` `chemotaxis-bifurcation-lean/chemotaxisbifurcation-remainderfromjet-jethyp-zero` `chemotaxis-bifurcation-lean/chemotaxisbifurcation-remainderfromjet-jethyp` `chemotaxis-bifurcation-lean/chemotaxisbifurcation-remainderfromjet-jetrs` `chemotaxis-bifurcation-lean/chemotaxisbifurcation-remainderfromjet-value-bound` `chemotaxis-bifurcation-lean/chemotaxisbifurcation-remainderfromjet-s-bound-final` `chemotaxis-bifurcation-lean/chemotaxisbifurcation-remainderfromjet-value-bound-final` `chemotaxis-bifurcation-lean/chemotaxisbifurcation-remainderfromjet-deriv-zero-of-sq-bound` `chemotaxis-bifurcation-lean/chemotaxisbifurcation-remainderfromjet-abs-sub-le-of-deriv-bound`	`ChemotaxisBifurcation.RemainderFromJet.mixed_interface_of_jet` `ChemotaxisBifurcation.RemainderFromJet.final_interface_of_jet` `ChemotaxisBifurcation.RemainderFromJet.final_value_bound_iff` `ChemotaxisBifurcation.RemainderFromJet.jet_branch_eventually` `ChemotaxisBifurcation.RemainderFromJet.jet_branch_curves` `ChemotaxisBifurcation.RemainderFromJet.jetHyp_zero` `ChemotaxisBifurcation.RemainderFromJet.JetHyp` `ChemotaxisBifurcation.RemainderFromJet.jetRs` `ChemotaxisBifurcation.RemainderFromJet.value_bound` `ChemotaxisBifurcation.RemainderFromJet.s_bound_final` `ChemotaxisBifurcation.RemainderFromJet.value_bound_final` `ChemotaxisBifurcation.RemainderFromJet.deriv_zero_of_sq_bound` `ChemotaxisBifurcation.RemainderFromJet.abs_sub_le_of_deriv_bound`	verified verified verified verified verified verified verified verified verified verified verified verified verified	C⁴ regularity of the actual reduced remainder on an open neighborhood R(η,0)=0 on a small parameter interval the five specified point-jet cancellations from the Fourier computation identification of the reduced field with αηs−βs³+R and α>0, β≠0 axis cancellation R_s(η,0)=0 additionally for the Eq. 2.43 bound center-manifold existence and transfer of scalar conclusions to the PDE are outside this row	Exact public scope, hypotheses and exclusions: data/public-scope-ledger.json, row paper3/E:center-ODE-final/remainder-from-jet. This display summary does not extend that scope. Source locator: p. 20, TeX line 1961.
Theorem 1.3(2)-(3), ambient-limit proof paragraphs	Ambient closure of the admissible set	Inputs supplied	`chemotaxis-bifurcation-lean/chemotaxisbifurcation-ambientclosure-closure-subset-admissible` `chemotaxis-bifurcation-lean/chemotaxisbifurcation-ambientclosure-closure-subset-admissible-minimal` `chemotaxis-bifurcation-lean/chemotaxisbifurcation-ambientclosure-closure-subset-admissible-logistic` `chemotaxis-bifurcation-lean/chemotaxisbifurcation-ambientclosure-closure-subset-limitconditions` `chemotaxis-bifurcation-lean/chemotaxisbifurcation-ambientclosure-zero-trivial-not-mem-closure` `chemotaxis-bifurcation-lean/chemotaxisbifurcation-ambientclosure-exists-ge-mean` `chemotaxis-bifurcation-lean/chemotaxisbifurcation-ambientclosure-logistic-exists-ge-ustar` `chemotaxis-bifurcation-lean/chemotaxisbifurcation-ambientclosure-logistic-zero-sensitivity-eq` `chemotaxis-bifurcation-lean/chemotaxisbifurcation-ambientclosure-minimal-zero-sensitivity-eq` `chemotaxis-bifurcation-lean/chemotaxisbifurcation-ambientclosure-limit-coeffs-bounded` `chemotaxis-bifurcation-lean/chemotaxisbifurcation-ambientclosure-admissibleset` `chemotaxis-bifurcation-lean/chemotaxisbifurcation-ambientclosure-part2-ssup-eq-top-of-ambient` `chemotaxis-bifurcation-lean/chemotaxisbifurcation-ambientclosure-part3-global-of-ambient` `chemotaxis-bifurcation-lean/chemotaxisbifurcation-ambientclosure-isclosed-setof-forall-nonneg` `chemotaxis-bifurcation-lean/chemotaxisbifurcation-ambientclosure-isclosed-setof-exists-ge` `chemotaxis-bifurcation-lean/chemotaxisbifurcation-weakh2ambientclosure-logistic-closure-subset-admissible` `chemotaxis-bifurcation-lean/chemotaxisbifurcation-weakh2ambientclosure-minimal-closure-subset-admissible` `chemotaxis-bifurcation-lean/chemotaxisbifurcation-weakh2ambientclosure-meanzerotranslation` `chemotaxis-bifurcation-lean/chemotaxisbifurcation-weakh2ambientclosure-positivemeanzerotranslation` `chemotaxis-bifurcation-lean/chemotaxisbifurcation-intervalstrongpositivity-positive-of-nonnegative` `chemotaxis-bifurcation-lean/chemotaxisbifurcation-relativecompactness-iscompact-closure-of-subsequence` `chemotaxis-bifurcation-lean/chemotaxisbifurcation-boundedsolutionslices-logistic-slice-subsequence` `chemotaxis-bifurcation-lean/chemotaxisbifurcation-boundedsolutionslices-minimal-slice-subsequence` `chemotaxis-bifurcation-lean/chemotaxisbifurcation-boundedsolutionslices-logistic-iscompact-closure-slice` `chemotaxis-bifurcation-lean/chemotaxisbifurcation-boundedsolutionslices-minimal-iscompact-closure-slice` `chemotaxis-bifurcation-lean/chemotaxisbifurcation-parametrizedsolutioncomponents-logistic-of-local-curve` `chemotaxis-bifurcation-lean/chemotaxisbifurcation-parametrizedsolutioncomponents-minimal-of-local-curve` `chemotaxis-bifurcation-lean/chemotaxisbifurcation-fourieramplitude-logistic-of-fourier-curve` `chemotaxis-bifurcation-lean/chemotaxisbifurcation-fourieramplitude-minimal-of-fourier-curve` `chemotaxis-bifurcation-lean/chemotaxisbifurcation-fouriercomplement-remainder-mass` `chemotaxis-bifurcation-lean/chemotaxisbifurcation-fouriercomplement-remainder-mem-fixedmean-iff` `chemotaxis-bifurcation-lean/chemotaxisbifurcation-fouriercomplement-existsunique-fixedmean-decomposition`	`ChemotaxisBifurcation.AmbientClosure.closure_subset_admissible` `ChemotaxisBifurcation.AmbientClosure.closure_subset_admissible_minimal` `ChemotaxisBifurcation.AmbientClosure.closure_subset_admissible_logistic` `ChemotaxisBifurcation.AmbientClosure.closure_subset_limitConditions` `ChemotaxisBifurcation.AmbientClosure.zero_trivial_not_mem_closure` `ChemotaxisBifurcation.AmbientClosure.exists_ge_mean` `ChemotaxisBifurcation.AmbientClosure.logistic_exists_ge_uStar` `ChemotaxisBifurcation.AmbientClosure.logistic_zero_sensitivity_eq` `ChemotaxisBifurcation.AmbientClosure.minimal_zero_sensitivity_eq` `ChemotaxisBifurcation.AmbientClosure.limit_coeffs_bounded` `ChemotaxisBifurcation.AmbientClosure.admissibleSet` `ChemotaxisBifurcation.AmbientClosure.part2_sSup_eq_top_of_ambient` `ChemotaxisBifurcation.AmbientClosure.part3_global_of_ambient` `ChemotaxisBifurcation.AmbientClosure.isClosed_setOf_forall_nonneg` `ChemotaxisBifurcation.AmbientClosure.isClosed_setOf_exists_ge` `ChemotaxisBifurcation.WeakH2AmbientClosure.logistic_closure_subset_admissible` `ChemotaxisBifurcation.WeakH2AmbientClosure.minimal_closure_subset_admissible` `ChemotaxisBifurcation.WeakH2AmbientClosure.meanZeroTranslation` `ChemotaxisBifurcation.WeakH2AmbientClosure.positiveMeanZeroTranslation` `ChemotaxisBifurcation.IntervalStrongPositivity.positive_of_nonnegative` `ChemotaxisBifurcation.RelativeCompactness.isCompact_closure_of_subsequence` `ChemotaxisBifurcation.BoundedSolutionSlices.logistic_slice_subsequence` `ChemotaxisBifurcation.BoundedSolutionSlices.minimal_slice_subsequence` `ChemotaxisBifurcation.BoundedSolutionSlices.logistic_isCompact_closure_slice` `ChemotaxisBifurcation.BoundedSolutionSlices.minimal_isCompact_closure_slice` `ChemotaxisBifurcation.ParametrizedSolutionComponents.logistic_of_local_curve` `ChemotaxisBifurcation.ParametrizedSolutionComponents.minimal_of_local_curve` `ChemotaxisBifurcation.FourierAmplitude.logistic_of_fourier_curve` `ChemotaxisBifurcation.FourierAmplitude.minimal_of_fourier_curve` `ChemotaxisBifurcation.FourierComplement.remainder_mass` `ChemotaxisBifurcation.FourierComplement.remainder_mem_fixedMean_iff` `ChemotaxisBifurcation.FourierComplement.existsUnique_fixedMean_decomposition`	verified verified verified verified verified verified verified verified verified verified verified verified verified verified verified verified verified verified verified verified verified verified verified verified verified verified verified verified verified verified verified verified	identification of the manuscript F=0 weak-H2 stationary solution sets and actual branch points with the classical solution sets used by the closure wrappers, at the correct constrained parameters actual component relative closedness, inclusion in the admissible set and in closure S, and set-level compactness of bounded-sensitivity slices required by the retained global consumers the part (2) noncompactness hypothesis; the part (3) global alternatives, distinguished constant/complement and orthogonality, and strict orientation/local branch foundations; these are not constructed by the analytic closure proof	Conditional scope retained. Actual cosine complement, curved elliptic cubic response and conserved-mean coefficient extraction supply the scoped ingredients. Family/jet construction, operator identity and global foundations remain explicit. Public scope and supplied inputs: data/public-scope-ledger.json, paper3/L:ambient-closure/deductions
Theorem 1.3(3), Equation 4.18, full range 1 <= m <= 2	ODE content of the monotone-locus argument	Inputs supplied	`chemotaxis-bifurcation-lean/chemotaxisbifurcation-monotonelocusgeneral-stationarysolution` `chemotaxis-bifurcation-lean/chemotaxisbifurcation-monotonelocusgeneral-isconston` `chemotaxis-bifurcation-lean/chemotaxisbifurcation-monotonelocusgeneral-coeff` `chemotaxis-bifurcation-lean/chemotaxisbifurcation-monotonelocusgeneral-stationarysolution-continuouson-u` `chemotaxis-bifurcation-lean/chemotaxisbifurcation-monotonelocusgeneral-stationarysolution-continuouson-v` `chemotaxis-bifurcation-lean/chemotaxisbifurcation-monotonelocusgeneral-stationarysolution-deriv-z` `chemotaxis-bifurcation-lean/chemotaxisbifurcation-monotonelocusgeneral-stationarysolution-continuouson-coeff` `chemotaxis-bifurcation-lean/chemotaxisbifurcation-monotonelocusgeneral-stationarysolution-eq-const-of-zero` `chemotaxis-bifurcation-lean/chemotaxisbifurcation-monotonelocusgeneral-stationarysolution-factor-pos` `chemotaxis-bifurcation-lean/chemotaxisbifurcation-monotonelocusgeneral-stationarysolution-pos-l-of-not-const` `chemotaxis-bifurcation-lean/chemotaxisbifurcation-monotonelocusgeneral-stationarysolution-z-ne-zero-at` `chemotaxis-bifurcation-lean/chemotaxisbifurcation-monotonelocusgeneral-stationarysolution-z-ne-zero-left` `chemotaxis-bifurcation-lean/chemotaxisbifurcation-monotonelocusgeneral-stationarysolution-z-ne-zero-right` `chemotaxis-bifurcation-lean/chemotaxisbifurcation-monotonelocusgeneral-stationarysolution-sig-neg-of-antitoneon` `chemotaxis-bifurcation-lean/chemotaxisbifurcation-monotonelocusgeneral-stationarysolution-sig-pos-of-monotoneon` `chemotaxis-bifurcation-lean/chemotaxisbifurcation-monotonelocusgeneral-stationarysolution-strictantion-of-sig-neg` `chemotaxis-bifurcation-lean/chemotaxisbifurcation-monotonelocusgeneral-stationarysolution-strictmonoon-of-sig-pos` `chemotaxis-bifurcation-lean/chemotaxisbifurcation-monotonelocusgeneral-stationarysolution-strictantion-of-antitoneon` `chemotaxis-bifurcation-lean/chemotaxisbifurcation-monotonelocusgeneral-stationarysolution-strictmonoon-of-monotoneon` `chemotaxis-bifurcation-lean/chemotaxisbifurcation-monotonelocusgeneral-isclopen-decreasinglocus` `chemotaxis-bifurcation-lean/chemotaxisbifurcation-monotonelocusgeneral-isclopen-increasinglocus` `chemotaxis-bifurcation-lean/chemotaxisbifurcation-monotonelocusgeneral-part3-strictanti-of-ode` `chemotaxis-bifurcation-lean/chemotaxisbifurcation-monotonelocusgeneral-part3-strictmono-of-ode` `chemotaxis-bifurcation-lean/chemotaxisbifurcation-monotonelocus-linear-eq-zero` `chemotaxis-bifurcation-lean/chemotaxisbifurcation-monotonelocus-abs-le-mul-min` `chemotaxis-bifurcation-lean/chemotaxisbifurcation-monotonelocus-exists-margin` `chemotaxis-bifurcation-lean/chemotaxisbifurcation-monotonelocus-neg-of-perturb` `chemotaxis-bifurcation-lean/chemotaxisbifurcation-monotonelocus-two-div-mul-min-le-sin` `chemotaxis-bifurcation-lean/chemotaxisbifurcation-monotonelocus-exists-margin-pos` `chemotaxis-bifurcation-lean/chemotaxisbifurcation-weakh2monotonelocus-isclopen-decreasinglocus-of-weakh2` `chemotaxis-bifurcation-lean/chemotaxisbifurcation-weakh2monotonelocus-isclopen-increasinglocus-of-weakh2` `chemotaxis-bifurcation-lean/chemotaxisbifurcation-weakh2monotonelocus-part3-strictanti-of-weakh2` `chemotaxis-bifurcation-lean/chemotaxisbifurcation-weakh2monotonelocus-part3-strictmono-of-weakh2`	`ChemotaxisBifurcation.MonotoneLocusGeneral.StationarySolution` `ChemotaxisBifurcation.MonotoneLocusGeneral.IsConstOn` `ChemotaxisBifurcation.MonotoneLocusGeneral.coeff` `ChemotaxisBifurcation.MonotoneLocusGeneral.StationarySolution.continuousOn_u` `ChemotaxisBifurcation.MonotoneLocusGeneral.StationarySolution.continuousOn_v` `ChemotaxisBifurcation.MonotoneLocusGeneral.StationarySolution.deriv_z` `ChemotaxisBifurcation.MonotoneLocusGeneral.StationarySolution.continuousOn_coeff` `ChemotaxisBifurcation.MonotoneLocusGeneral.StationarySolution.eq_const_of_zero` `ChemotaxisBifurcation.MonotoneLocusGeneral.StationarySolution.factor_pos` `ChemotaxisBifurcation.MonotoneLocusGeneral.StationarySolution.pos_L_of_not_const` `ChemotaxisBifurcation.MonotoneLocusGeneral.StationarySolution.z_ne_zero_at` `ChemotaxisBifurcation.MonotoneLocusGeneral.StationarySolution.z_ne_zero_left` `ChemotaxisBifurcation.MonotoneLocusGeneral.StationarySolution.z_ne_zero_right` `ChemotaxisBifurcation.MonotoneLocusGeneral.StationarySolution.sig_neg_of_antitoneOn` `ChemotaxisBifurcation.MonotoneLocusGeneral.StationarySolution.sig_pos_of_monotoneOn` `ChemotaxisBifurcation.MonotoneLocusGeneral.StationarySolution.strictAntiOn_of_sig_neg` `ChemotaxisBifurcation.MonotoneLocusGeneral.StationarySolution.strictMonoOn_of_sig_pos` `ChemotaxisBifurcation.MonotoneLocusGeneral.StationarySolution.strictAntiOn_of_antitoneOn` `ChemotaxisBifurcation.MonotoneLocusGeneral.StationarySolution.strictMonoOn_of_monotoneOn` `ChemotaxisBifurcation.MonotoneLocusGeneral.isClopen_decreasingLocus` `ChemotaxisBifurcation.MonotoneLocusGeneral.isClopen_increasingLocus` `ChemotaxisBifurcation.MonotoneLocusGeneral.part3_strictAnti_of_ode` `ChemotaxisBifurcation.MonotoneLocusGeneral.part3_strictMono_of_ode` `ChemotaxisBifurcation.MonotoneLocus.linear_eq_zero` `ChemotaxisBifurcation.MonotoneLocus.abs_le_mul_min` `ChemotaxisBifurcation.MonotoneLocus.exists_margin` `ChemotaxisBifurcation.MonotoneLocus.neg_of_perturb` `ChemotaxisBifurcation.MonotoneLocus.two_div_mul_min_le_sin` `ChemotaxisBifurcation.MonotoneLocus.exists_margin_pos` `ChemotaxisBifurcation.WeakH2MonotoneLocus.isClopen_decreasingLocus_of_weakH2` `ChemotaxisBifurcation.WeakH2MonotoneLocus.isClopen_increasingLocus_of_weakH2` `ChemotaxisBifurcation.WeakH2MonotoneLocus.part3_strictAnti_of_weakH2` `ChemotaxisBifurcation.WeakH2MonotoneLocus.part3_strictMono_of_weakH2`	verified verified verified verified verified verified verified verified verified verified verified verified verified verified verified verified verified verified verified verified verified verified verified verified verified verified verified verified verified verified verified verified verified	ordinary given-component membership and actual classical-PDE profile correspondence; global branch existence/continuation and connected-component foundations remain outside this consumer hConst: local constant-limit bifurcation representation; hStar: local half-branch parametrization at the distinguished point; the full weak-H2 population embedding, actual ODE identification, signal C2 topology and pointwise continuity are derived	Exact public scope, hypotheses and exclusions: data/public-scope-ledger.json, row paper3/T:global-extension/monotone-locus. This display summary does not extend that scope. Source locator: p. 32, TeX line 2980.
Lemma 2.1 and Equation 2.17 (phase-space-H2)	Neumann H^2 phase space as cosine series	Same assumptions	`chemotaxis-bifurcation-lean/chemotaxisbifurcation-weakderivative1d-istestfunction` `chemotaxis-bifurcation-lean/chemotaxisbifurcation-weakderivative1d-hasweakderiv` `chemotaxis-bifurcation-lean/chemotaxisbifurcation-weakderivative1d-h2` `chemotaxis-bifurcation-lean/chemotaxisbifurcation-weakderivative1d-neumanntrace` `chemotaxis-bifurcation-lean/chemotaxisbifurcation-weakderivative1d-ae-eq-const-of-integral-mul-deriv-eq-zero` `chemotaxis-bifurcation-lean/chemotaxisbifurcation-weakderivative1d-hasweakderiv-ae-eq-primitive` `chemotaxis-bifurcation-lean/chemotaxisbifurcation-weakderivative1d-h2-exists-neumannw21` `chemotaxis-bifurcation-lean/chemotaxisbifurcation-weakderivative1d-h2-summable-norm-cosinecoeff` `chemotaxis-bifurcation-lean/chemotaxisbifurcation-weakderivative1d-h2-hassum-cosinecoeff` `chemotaxis-bifurcation-lean/chemotaxisbifurcation-weakderivative1d-eqon-of-ae-eq-continuouson` `chemotaxis-bifurcation-lean/chemotaxisbifurcation-weakderivative1d-intervalintegrable-of-memlp`	`ChemotaxisBifurcation.WeakDerivative1D.IsTestFunction` `ChemotaxisBifurcation.WeakDerivative1D.HasWeakDeriv` `ChemotaxisBifurcation.WeakDerivative1D.H2` `ChemotaxisBifurcation.WeakDerivative1D.NeumannTrace` `ChemotaxisBifurcation.WeakDerivative1D.ae_eq_const_of_integral_mul_deriv_eq_zero` `ChemotaxisBifurcation.WeakDerivative1D.HasWeakDeriv.ae_eq_primitive` `ChemotaxisBifurcation.WeakDerivative1D.H2.exists_neumannW21` `ChemotaxisBifurcation.WeakDerivative1D.H2.summable_norm_cosineCoeff` `ChemotaxisBifurcation.WeakDerivative1D.H2.hasSum_cosineCoeff` `ChemotaxisBifurcation.WeakDerivative1D.eqOn_of_ae_eq_continuousOn` `ChemotaxisBifurcation.WeakDerivative1D.intervalIntegrable_of_memLp`	verified verified verified verified verified verified verified verified verified verified verified	—	Exact public scope, hypotheses and exclusions: data/public-scope-ledger.json, row paper3/L:trig-integrals/phase-space-H2. This display summary does not extend that scope. Source locator: p. 13, TeX line 1153.
Equation (2.43) (axis-condition)	Axis condition for the remainder (jet conditions alone do not suffice)	Inputs supplied	`chemotaxis-bifurcation-lean/chemotaxisbifurcation-remainderaxis-iteratedfderiv-succ-eq-of-line` `chemotaxis-bifurcation-lean/chemotaxisbifurcation-remainderaxis-cexr` `chemotaxis-bifurcation-lean/chemotaxisbifurcation-remainderaxis-uncurry-cexr` `chemotaxis-bifurcation-lean/chemotaxisbifurcation-remainderaxis-contdiff-cexr` `chemotaxis-bifurcation-lean/chemotaxisbifurcation-remainderaxis-cex-d-s` `chemotaxis-bifurcation-lean/chemotaxisbifurcation-remainderaxis-cex-d-eta-s` `chemotaxis-bifurcation-lean/chemotaxisbifurcation-remainderaxis-cex-d-ss` `chemotaxis-bifurcation-lean/chemotaxisbifurcation-remainderaxis-cex-d3` `chemotaxis-bifurcation-lean/chemotaxisbifurcation-remainderaxis-jethyp-cex` `chemotaxis-bifurcation-lean/chemotaxisbifurcation-remainderaxis-jetrs-cex` `chemotaxis-bifurcation-lean/chemotaxisbifurcation-remainderaxis-cex-not-final` `chemotaxis-bifurcation-lean/chemotaxisbifurcation-remainderaxis-jethyp-not-sufficient` `chemotaxis-bifurcation-lean/chemotaxisbifurcation-remainderaxis-sigman0` `chemotaxis-bifurcation-lean/chemotaxisbifurcation-remainderaxis-sigman0-chistar` `chemotaxis-bifurcation-lean/chemotaxisbifurcation-remainderaxis-sigman0-shift` `chemotaxis-bifurcation-lean/chemotaxisbifurcation-remainderaxis-remainderof` `chemotaxis-bifurcation-lean/chemotaxisbifurcation-remainderaxis-reducedfield-remainderof` `chemotaxis-bifurcation-lean/chemotaxisbifurcation-remainderaxis-trivialbranchlinearization` `chemotaxis-bifurcation-lean/chemotaxisbifurcation-remainderaxis-axis-of-reduction` `chemotaxis-bifurcation-lean/chemotaxisbifurcation-remainderaxis-model-final-interface` `chemotaxis-bifurcation-lean/chemotaxisbifurcation-remainderaxis-model-branch-curves` `chemotaxis-bifurcation-lean/chemotaxisbifurcation-remainderaxis-normalform-reduction` `chemotaxis-bifurcation-lean/chemotaxisbifurcation-remainderaxis-cex-violates-reduction`	`ChemotaxisBifurcation.RemainderAxis.iteratedFDeriv_succ_eq_of_line` `ChemotaxisBifurcation.RemainderAxis.cexR` `ChemotaxisBifurcation.RemainderAxis.uncurry_cexR` `ChemotaxisBifurcation.RemainderAxis.contDiff_cexR` `ChemotaxisBifurcation.RemainderAxis.cex_d_s` `ChemotaxisBifurcation.RemainderAxis.cex_d_eta_s` `ChemotaxisBifurcation.RemainderAxis.cex_d_ss` `ChemotaxisBifurcation.RemainderAxis.cex_d3` `ChemotaxisBifurcation.RemainderAxis.jetHyp_cex` `ChemotaxisBifurcation.RemainderAxis.jetRs_cex` `ChemotaxisBifurcation.RemainderAxis.cex_not_final` `ChemotaxisBifurcation.RemainderAxis.jetHyp_not_sufficient` `ChemotaxisBifurcation.RemainderAxis.sigmaN0` `ChemotaxisBifurcation.RemainderAxis.sigmaN0_chiStar` `ChemotaxisBifurcation.RemainderAxis.sigmaN0_shift` `ChemotaxisBifurcation.RemainderAxis.remainderOf` `ChemotaxisBifurcation.RemainderAxis.reducedField_remainderOf` `ChemotaxisBifurcation.RemainderAxis.TrivialBranchLinearization` `ChemotaxisBifurcation.RemainderAxis.axis_of_reduction` `ChemotaxisBifurcation.RemainderAxis.model_final_interface` `ChemotaxisBifurcation.RemainderAxis.model_branch_curves` `ChemotaxisBifurcation.RemainderAxis.normalForm_reduction` `ChemotaxisBifurcation.RemainderAxis.cex_violates_reduction`	verified verified verified verified verified verified verified verified verified verified verified verified verified verified verified verified verified verified verified verified verified verified verified	identification of p with a positive physical equilibrium in the logistic or fixed-mass minimal model identification x=λ_n₀>0 and of the modal threshold with χ* at the selected critical mode existence of the reduced field in the manuscript’s Fourier amplitude and original time coordinate C⁴ regularity on an open neighborhood containing a closed box with 0<r≤1 R(η,0)=0 throughout that box the five origin jets R_s=R_ηs=R_ss=R_ηss=R_sss=0, including identification of β_n₀ with the cubic coefficient TrivialBranchLinearization throughout \|η\|≤r β_n₀≠0 for the branch conclusions	Exact public scope, hypotheses and exclusions: data/public-scope-ledger.json, row paper3/E:center-ODE-final/axis-condition. This display summary does not extend that scope. Source locator: p. 20, TeX line 1961.
Equation (2.22) (projected-remainder)	Projection of the fourth-order remainder onto a cosine mode	Same assumptions	`chemotaxis-bifurcation-lean/chemotaxisbifurcation-projectedremainder-projected-remainder-bound` `chemotaxis-bifurcation-lean/chemotaxisbifurcation-projectedremainder-projected-remainder-bound-of-absolutelycontinuous` `chemotaxis-bifurcation-lean/chemotaxisbifurcation-projectedremainder-projected-remainder-bound-quartic` `chemotaxis-bifurcation-lean/chemotaxisbifurcation-projectedremainder-projected-remainder-bound-norm` `chemotaxis-bifurcation-lean/chemotaxisbifurcation-projectedremainder-projected-remainder-bound-deriv` `chemotaxis-bifurcation-lean/chemotaxisbifurcation-projectedremainder-projected-bound-of-ibp` `chemotaxis-bifurcation-lean/chemotaxisbifurcation-projectedremainder-integral-deriv-mul-cos` `chemotaxis-bifurcation-lean/chemotaxisbifurcation-projectedremainder-abs-integral-le-of-abs-le` `chemotaxis-bifurcation-lean/chemotaxisbifurcation-projectedremainder-projected-remainder-bound-example` `chemotaxis-bifurcation-lean/chemotaxisbifurcation-projectedremainder-freq` `chemotaxis-bifurcation-lean/chemotaxisbifurcation-projectedremainder-freq-nonneg` `chemotaxis-bifurcation-lean/chemotaxisbifurcation-projectedremainder-freq-mul-l` `chemotaxis-bifurcation-lean/chemotaxisbifurcation-projectedremainder-cos-freq` `chemotaxis-bifurcation-lean/chemotaxisbifurcation-modalremainder-population-normalized-bound` `chemotaxis-bifurcation-lean/chemotaxisbifurcation-modalremainder-population-remainder-quartic` `chemotaxis-bifurcation-lean/chemotaxisbifurcation-populationmodalresidual-actual-nonlinear-operator-decomposition` `chemotaxis-bifurcation-lean/chemotaxisbifurcation-populationmodalresidual-actual-population-projection-quartic-uniform` `chemotaxis-bifurcation-lean/chemotaxisbifurcation-rpow-quadratic-remainder`	`ChemotaxisBifurcation.ProjectedRemainder.projected_remainder_bound` `ChemotaxisBifurcation.ProjectedRemainder.projected_remainder_bound_of_absolutelyContinuous` `ChemotaxisBifurcation.ProjectedRemainder.projected_remainder_bound_quartic` `ChemotaxisBifurcation.ProjectedRemainder.projected_remainder_bound_norm` `ChemotaxisBifurcation.ProjectedRemainder.projected_remainder_bound_deriv` `ChemotaxisBifurcation.ProjectedRemainder.projected_bound_of_ibp` `ChemotaxisBifurcation.ProjectedRemainder.integral_deriv_mul_cos` `ChemotaxisBifurcation.ProjectedRemainder.abs_integral_le_of_abs_le` `ChemotaxisBifurcation.ProjectedRemainder.projected_remainder_bound_example` `ChemotaxisBifurcation.ProjectedRemainder.freq` `ChemotaxisBifurcation.ProjectedRemainder.freq_nonneg` `ChemotaxisBifurcation.ProjectedRemainder.freq_mul_L` `ChemotaxisBifurcation.ProjectedRemainder.cos_freq` `ChemotaxisBifurcation.ModalRemainder.population_normalized_bound` `ChemotaxisBifurcation.ModalRemainder.population_remainder_quartic` `ChemotaxisBifurcation.PopulationModalResidual.actual_nonlinear_operator_decomposition` `ChemotaxisBifurcation.PopulationModalResidual.actual_population_projection_quartic_uniform` `ChemotaxisBifurcation.rpow_quadratic_remainder`	verified verified verified verified verified verified verified verified verified verified verified verified verified verified verified verified verified verified	—	Exact public scope, hypotheses and exclusions: data/public-scope-ledger.json, row paper3/E:ode-eq0/projected-remainder. This display summary does not extend that scope. Source locator: p. 17, TeX line 1586. arXiv v2 note: v2 keeps the flux-form remainder decomposition only as a TeX comment; see the ledger row’s arxiv_v2_note.
Equations 2.18-2.19	Normalized signal Taylor remainder	Same assumptions	`chemotaxis-bifurcation-lean/chemotaxisbifurcation-modalremainder-signalremainder` `chemotaxis-bifurcation-lean/chemotaxisbifurcation-modalremainder-signalremainder-zero` `chemotaxis-bifurcation-lean/chemotaxisbifurcation-modalremainder-signalremainder-pos` `chemotaxis-bifurcation-lean/chemotaxisbifurcation-modalremainder-signalremainder-eq-of-balance` `chemotaxis-bifurcation-lean/chemotaxisbifurcation-modalremainder-cosinecoeff-zero-bound` `chemotaxis-bifurcation-lean/chemotaxisbifurcation-modalremainder-cosinecoeff-pos-bound` `chemotaxis-bifurcation-lean/chemotaxisbifurcation-modalremainder-signalremainder-zero-bound` `chemotaxis-bifurcation-lean/chemotaxisbifurcation-modalremainder-signalremainder-pos-bound` `chemotaxis-bifurcation-lean/chemotaxisbifurcation-modalremainder-signalremainder-quartic` `chemotaxis-bifurcation-lean/chemotaxisbifurcation-modalremainder-summable-norm-signalremainder` `chemotaxis-bifurcation-lean/chemotaxisbifurcation-signalmodalresidual-modalresidual-eq-of-physical-signal` `chemotaxis-bifurcation-lean/chemotaxisbifurcation-signalmodalresidual-modalresidual-quartic` `chemotaxis-bifurcation-lean/chemotaxisbifurcation-signalmodalresidual-summable-modalresidual`	`ChemotaxisBifurcation.ModalRemainder.signalRemainder` `ChemotaxisBifurcation.ModalRemainder.signalRemainder_zero` `ChemotaxisBifurcation.ModalRemainder.signalRemainder_pos` `ChemotaxisBifurcation.ModalRemainder.signalRemainder_eq_of_balance` `ChemotaxisBifurcation.ModalRemainder.cosineCoeff_zero_bound` `ChemotaxisBifurcation.ModalRemainder.cosineCoeff_pos_bound` `ChemotaxisBifurcation.ModalRemainder.signalRemainder_zero_bound` `ChemotaxisBifurcation.ModalRemainder.signalRemainder_pos_bound` `ChemotaxisBifurcation.ModalRemainder.signalRemainder_quartic` `ChemotaxisBifurcation.ModalRemainder.summable_norm_signalRemainder` `ChemotaxisBifurcation.SignalModalResidual.modalResidual_eq_of_physical_signal` `ChemotaxisBifurcation.SignalModalResidual.modalResidual_quartic` `ChemotaxisBifurcation.SignalModalResidual.summable_modalResidual`	verified verified verified verified verified verified verified verified verified verified verified verified verified	—	actual nonlinear signal-profile modal residual: exact zero/positive normalization, actual source Taylor estimate, original elliptic projected balance, summability, and full physical-signal equilibrium wrapper are derived. Ordinary given-profile regularity/PDE/small-amplitude inputs remain; no center-manifold or full Fourier-convolution existence is claimed. Source locator: p. 16, TeX line 1458.

One line per paper result of coverage.yaml. Ledger: the status lean-pkg claims ledger gives each claim, in the order of the claims; only verified means the recorded receipts close the claim.

Back to Verification.