docs: move research dossier into docs/ and update cross-references

docs/mathematical_analysis.md

@@ -0,0 +1,142 @@
+# Mathematical analysis
+
+Status: analytical derivations below are proved under their stated assumptions. They are not claims of new mathematics. No real-data performance claim has been verified. Numerical checks are reported separately in `results/`.
+
+## A. What a conflict edge actually means
+
+Let C(X) be a finite candidate set, w_i a real score, and H=(C,E) a conflict graph. Maximum-weight independent selection is
+
+\[
+\max_{z\in\{0,1\}^{|C|}}\sum_i w_i z_i,\qquad z_i+z_j\le1\quad(ij\in E).
+\]
+
+An edge is valid only if its endpoints cannot both be accepted under the task's definition of distinct true detections. Two alternative explanations of the *same* measurement can justify exclusivity when an explicit generative/association assumption establishes this. Spatial nearness, similar intensities, shared background, or a learned similarity alone cannot.
+
+**Necessary feasibility condition.** If T contains one correct candidate for each true object, all those detections can be retained only if H[T] is edgeless. This is also sufficient for T to be feasible, but not for an optimizer to select T. Proof: a single internal edge violates an inequality; without such edges all inequalities for the indicator of T hold.
+
+**Counterexample 1 (adjacency).** Two real targets at (10,10) and (10,12), scores 0.9 and 0.8, and a proximity-conflict radius of 3 force the output to contain at most one. Recall is at most 1/2, even with perfect candidate scores.
+
+**Counterexample 2 (valid graph does not guarantee recall).** A true candidate of weight 1 conflicts with a spurious alternative of weight 2. Even if the conflict is valid as a one-measurement association constraint, the optimal set selects the wrong hypothesis. Constraints ensure consistency, not correctness.
+
+A sufficient optimality condition is: T is independent, true weights are strictly positive, and all false weights strictly negative. Then T is the unique optimum. This assumption is essentially already-perfect classification and offers no realistic detection guarantee. Positive isolated false candidates are always selected; independent-set selection alone cannot reject them.
+
+### Quadratic penalty and relaxation
+
+Consider F(z)=Σw_i z_i−λΣ_(ij∈E)z_i z_j. For λ>max(0,max_i w_i), every binary maximizer is independent. If a selected node has a selected neighbor, deleting it changes F by −w_i+λd_selected(i)>0. Thus a violating solution cannot maximize F. On independent sets the objectives coincide.
+
+This is an exact penalty result for binary optimization, not an efficient algorithm: general MWIS remains NP-hard. A triangle with edge constraints relaxed to z∈[0,1]^3 admits z=(1/2,1/2,1/2), objective 1.5 for unit weights, versus integral optimum 1. Clique inequalities improve this relaxation but do not generally describe the stable-set polytope. Rounding can break both feasibility and recall. Gumbel sampling, unrolled optimization, or implicit differentiation changes optimization mechanics, not the validity of edges. A straight-through gradient is biased and gives no discrete optimality guarantee.
+
+### Defensible replacement
+
+Use a bipartite candidate-to-object/hypothesis assignment, or multi-source reconstruction y=Σ_j a_j h(·−μ_j)+b+ε, with a_j≥0 and a point-spread-function model. Distinct nearby μ_j are allowed. For training, ground truth supplies distinct identities; at inference that privilege disappears. Restrict hard conflict edges to verified duplicate measurement hypotheses and keep uncertain edges as soft learned features. Test on close pairs at separations 0.5,1,2,3,5 pixels, multiple amplitudes and PSF widths, with source-level labels. Below resolution, identifiability requires additional assumptions; coincident equal-PSF sources cannot be uniquely separated from their summed amplitude in one image.
+
+## B. Define risk before choosing a loss
+
+For a prediction set S and true objects G, construct a bipartite eligibility graph using a fixed matching rule. Let ν(S,G) be maximum matching cardinality. Define
+
+\[
+TP=\nu(S,G),\quad FP=|S|-\nu(S,G),\quad FN=|G|-\nu(S,G).
+\]
+
+Primary desired risk is R_count=E[FP per image], not pixel error, precision, false discovery rate, nor probability of any false alarm. Also report R_any=P(FP≥1). With a deterministic proposal cap K, R_any≤R_count≤K R_any. These quantities must never share an unlabeled “Fa” column.
+
+The ideal objective minimizes expected size-weighted missed objects subject to R_count≤α. This is nonconvex and nondifferentiable. Optimizing a surrogate constraint empirically does not prove the population constraint. Weighted BCE, Focal, Dice and IoU do not automatically solve the constrained problem. NWD compares Gaussian box surrogates and does not count spurious objects; changing from boxes to masks changes the task.
+
+### Frozen object pool makes monotonicity well-defined
+
+Freeze the proposal generator, its base segmentation threshold, cap K, masks, centroids and eligibility rule. Learn a candidate gate score s_i. At threshold t retain the entire candidate if s_i≥t; never resegment its pixels as t changes.
+
+**Proposition B1 (matching deficiency monotonicity).** If S⊆T are subsets of the same frozen pool with unchanged eligibility, FP(S)≤FP(T). Adding one candidate increases maximum matching size by either 0 or 1, so |S|−ν changes by either 1 or 0. Induct over additions. TP also cannot decrease under addition.
+
+**Why a pixel threshold fails this assumption.** On an all-background image, three horizontally adjacent pixels with probabilities (0.9,0.6,0.9) form one false object at threshold 0.5 and two at threshold 0.8. Raising the threshold increases object FP. Thresholding pixels does not produce nested object sets. Generic monotone CRC cannot be applied without addressing this; finite-family LTT-style testing can handle nonmonotone risks with multiplicity correction.
+
+### Differentiable upper bound tied to matching
+
+On each training image, choose a deterministic maximum matching in the full frozen pool. Designate the matched candidate endpoints as P, one distinct candidate per matched object, and all remaining candidates as N. Every subset of P remains injectively matchable. Consequently, for any selected S,
+
+\[
+FP(S)\le |S\cap N|.
+\]
+
+At gate logit threshold b=0 (probability 0.5), use
+
+\[
+U_\tau(s)=\sum_{i\in N}\frac{\operatorname{softplus}(s_i/\tau)}{\log 2}.
+\]
+
+Since softplus(u)≥log 2 for u≥0, 1{s_i≥0}≤softplus(s_i/τ)/log 2. Thus FP(S_0)≤U_τ pointwise. This includes duplicate detections, not just background-labeled pixels. Ordinary sigmoid soft counts are **not** upper bounds: σ(0)=1/2 while 1{0≥0}=1.
+
+Train with L_pos=Σ_(i∈P) w_i softplus(−s_i)/max(1,|P|), w_i=clip(1/√a_i,0.1,1), where a_i is the matched ground-truth component area in native pixels, and empirical mean constraint E_train U_τ≤α_train. The Lagrangian is L_pos+λ(E_train U_τ−α_train), λ≥0. A projected dual-ascent update increases λ on constraint violations; gradient descent updates gate parameters. No global convergence claim is made for a neural gate. The prototype uses an MLP; a GNN is an ablation, not an assumption.
+
+Limitations: canonical labels penalize alternative valid matches, possibly reducing recall. The assignment is frozen rather than differentiated. Empty or incomplete proposal pools limit attainable recall. A fully merged pair remains one candidate. Area weighting can amplify annotation noise. The pointwise bound is conservative and is only asserted at the training threshold; calibration measures actual FP at every chosen test threshold. Jointly changing the proposal backbone invalidates frozen assignments and the calibration certificate. This is a staged prototype, **not an end-to-end differentiable component extractor**.
+
+### Finite-family calibration certificate (known statistical machinery)
+
+Freeze all learned parameters and preprocessing using training/development data. Before looking at calibration labels, fix M finite gate thresholds. Use n independent, identically distributed calibration images from the deployment distribution. For threshold j and k=1,…,K, let Z_ijk=1{FP_ij≥k}. Its mean p_jk is a Bernoulli tail probability. Obtain a one-sided Clopper–Pearson upper bound u_jk with error probability δ/(M K). Set
+
+\[
+U_j=\sum_{k=1}^K u_{jk}.
+\]
+
+Because E FP_j=Σ_k p_jk and a union bound covers all MK pairs, with probability at least 1−δ over the calibration sample, **every** threshold j satisfies E FP_j≤U_j. Choose any j with U_j≤α, including a data-dependent utility maximizer within this certified set. This gives a PAC-style high-probability statement about population expected count; it is not a guarantee that each image has ≤α false objects. The CP formula is BetaQuantile(1−ε; r+1,n−r) for r<n, and 1 for r=n.
+
+The explicit reject-all policy has known risk zero and is a valid fallback without a statistical estimate. Report it as certification failure for useful detection, not a successful detector. For R_any, use only k=1 and δ/M. Do not substitute that certificate for R_count. Other bounded-loss inequalities or LTT tests may improve efficiency; the theorem above is deliberately elementary and conservative.
+
+**Sample scarcity.** With zero observed false alarms for one Bernoulli event, upper bound =1−ε^(1/n). Certifying α requires n≥ceil(log ε/log(1−α)). For M=101, δ=.05, α=.01 this requires 758 independent zero-error calibration units. With K=64 count tails, even the zero-FP case needs 75,321 units at α=.01 under this conservative certificate. Existing small benchmarks cannot substantiate arbitrary stringent distribution-free count budgets. At n=80, even zero observed errors is not enough for a 1% any-alarm certificate with that grid. Bootstrap intervals do not repair insufficient independent exposure.
+
+Adjacent frames are not iid calibration units. For videos calibrate independent sequences using a predeclared sequence risk and cap, or state a defensible dependence model. Exchangeability alone does not justify independent-binomial CP intervals. Distribution shift, reused calibration labels for training/model selection, incomplete annotations, post-calibration resizing, or changing K breaks the stated guarantee. Calibration uncertainty and run-to-run training variation are distinct.
+
+### Additional checks on size/location claims
+
+The published SLS area weight uses min/max area and a variance term. With areas 1 and 1+d and population variance d²/4, w=(1+d²/4)/(1+d+d²/4). Its derivative has sign d²/4−1: it decreases then increases. This independently confirms that a global monotonic-decrease interpretation is false; B3 already investigates this issue, so the observation is not claimed as new. It does not by itself prove that the complete SLS loss is nonmonotone along every prediction path.
+
+A polar-coordinate centroid penalty measured from the image origin is not translation invariant: positions (1,0),(2,0) give a radial ratio penalty 1/2; translating both by 100 in x gives 1/102. Use normalized relative displacement for a translation-invariant localization ablation. These facts are mathematical checks, not evidence that a replacement trains better.
+
+## C. Temporal path formulation and failure modes
+
+For frame candidates V_t and forward motion-gated edges, score a path π by Σ_t ℓ_t(v_t)−Σ_t c(v_(t−1),v_t). The recurrence
+
+D_t(v)=ℓ_t(v)+max_(u→v)[D_(t−1)(u)−c(u,v)]
+
+finds the best complete path in a DAG in O(|V|+|E|), provided state contains all information required by transition costs. Acceleration needs an augmented state (previous pair or velocity), not just current position. Replace max by τ log Σ exp(·/τ) for a differentiable path-partition recurrence; at path level max score≤τ logΣ_π exp(score(π)/τ)≤max score+τ log(number of feasible paths). This smooths inference; it neither proves correct detection nor introduces a new general DP method.
+
+For multiple targets, flow conservation with unit node capacity can enforce candidate nonreuse; min-cost flow is a natural baseline. It does not resolve a candidate that already merges two objects. Birth/death and missing observations need explicit transitions and costs; the prototype DP test is complete-path-only, not a full tracker.
+
+If independent frame evidence has signal mean μ and noise variance σ², summing T correctly aligned observations gives SNR √T μ/σ. With equicorrelated noise ρ, gain becomes √(T/[1+(T−1)ρ]); at ρ=1 there is no gain. Alignment bias and PSF blur reduce signal mean. A coherent moving clutter streak can have a higher path score than the target. Maximizing over many noise paths increases false alarms through a multiple-comparisons effect; a √T claim without trajectory-search correction is misleading.
+
+Use camera-compensated displacement r=x_t−W_(t−1→t)(x_(t−1)) and Mahalanobis cost rᵀΣ⁻¹r, with positive-definite uncertainty Σ. These are modeling choices, not guarantees. Compensation can erase a stationary target or create edges from parallax; uncertain motion gates can omit the correct path. Evaluate identity compensation, known synthetic compensation, estimated compensation and deliberately wrong compensation separately. True subpixel claims require PSF-integrated synthetic source positions or real subpixel ground truth, not just tiny binary masks.
+
+## Claim ledger
+
+| Claim | Status |
+|---|---|
+| Proximity conflict edges preserve recall | False; explicit two-target counterexample |
+| Binary quadratic penalty recovers independent feasible optimizers for sufficiently large λ | Proved above; computational hardness remains |
+| Pixel threshold produces monotone object FP | False; splitting counterexample |
+| Frozen-set matching deficiency is monotone | Proved above |
+| Canonical-assignment softplus count bounds selected FP | Proved pointwise under fixed eligibility |
+| Calibration tail-sum bound controls population count risk | Proved under iid units, frozen finite family and fixed cap |
+| Proposed training improves recall at a certified budget | Untested hypothesis |
+| Path aggregation universally provides √T improvement | False without alignment/independence and search correction |
+| Any proposed combination is genuinely new | Not proved; full-text novelty gate remains |
+
+## Audit extension: fixed-sequence calibration and sample burden
+
+The existing tail-sum Bonferroni procedure is valid but conservative. [Learn then Test](https://arxiv.org/html/2110.01052v5), sections 2.2–2.3, already develops bounded-loss tests and fixed-sequence testing. The implementation adds this known alternative; it is not a proposed novel theorem. Its order is thresholds 1 down to 0, fixed independently of the calibration labels. Stop permanently at the first failed test.
+
+For count risk let Z_i=FP_i/K in [0,1], a=alpha/K and zbar their mean. Use p=exp(-n kl(min(zbar,a),a)), where kl is binary relative entropy. For any-alarm risk, sum 1{FP_i>0} is binomial under iid units; use its lower-tail CDF at alpha. Test each at delta. No CP binomial test is applied directly to fractional count observations. Endpoint alpha=0 yields no empirical certificate; alpha equal to the support bound is deterministically valid.
+
+**Verification of the guarantee.** Bounded Z satisfies E exp(-t Z) <= 1-mu+mu exp(-t), by the chord bound for a convex exponential, where mu=EZ. Independence and Markov's inequality then give P(zbar<=x) <= exp(-n kl(x,mu)) for x<mu. For the unsafe null mu>a this is at most the bound evaluated at a, yielding a valid lower-tail p-value. In the predetermined testing order, let j0 be the first unsafe threshold. Any unsafe acceptance requires accepting j0; this has probability at most delta. Dependence among threshold tests does not affect that implication. Choosing any accepted threshold is safe outside this event; if none pass, the explicit empty predictor has risk zero. This proof requires iid deployment units, a frozen pipeline and a bounded candidate count. It does not establish distribution-shift protection or a guarantee for a learned training loss.
+
+| Zero-event calculation, alpha=.01, delta=.05, K=64, M=101 | Required independent n |
+|---|---:|
+| Bonferroni any-alarm CP | 758 |
+| Fixed-sequence any-alarm exact test | 299 |
+| Bonferroni sum of K count-tail CP bounds | 75,321 |
+| Fixed-sequence normalized-count KL test | 19,172 |
+
+Thus 758 and 75,321 are not universal sample requirements. For the fixed-sequence zero case, n=ceil(log(delta)/log(1-alpha)) for any risk, or replace alpha by alpha/K for count risk. These calculations are executed in results/math_checks.json. They describe the all-zero data case, not expected power or observed detector performance.
+
+A remaining obstruction is rare bursts: FP=K with probability q and 0 otherwise. If q>alpha/K, mean count risk is unsafe, yet n samples are all zero with probability (1-q)^n. Any deterministic procedure that certifies this fixed detector on every all-zero observation must account for that event. This counterexample explains why the cap matters; it does not prove every adaptive procedure has the table's sample requirement. Reducing K changes the detector and may remove true targets.
+
+Do not inspect calibration results and then choose between Bonferroni and fixed sequence at full delta each. Predeclare the choice, or divide error across procedures. Fixed sequence returns a certified budget; it does not confer simultaneous confidence coverage on unused pointwise bounds.