Updated: 2026-09-06
The formalization covers the calendar-time first-report model, the likelihood factorization in Theorem 1 and Appendix Theorem 2, Lemma 1, Proposition 1, and the principal likelihood formulas.
Formalization gap: Lemma 2 and the Appendix D.8.2 shifted-process claim remain uncredited, and their proof repair is deferred. Their current proofs use incompatible arrival-time premises. Explanation.
FINAL_CLOSURE_RECEIPT.md.The mathematical scope covers the paper’s incident-birth, lifetime, report, first-report, observed-window, Poisson-regression, and zero-inflated models; the selected named theoretical results; and the displayed formulas that define or specialize their likelihoods. Empirical estimates, dataset reconstruction, simulations, figures, software behavior, and the causal validity of the NYC and Chicago administrative timestamps are not mathematical theorem targets.
| Result | Comparison with source |
|---|---|
| Reporting delay | Exact. |
| Lemma 1 | Process clarified: first reports inside a calendar-time window form the thinned-and-displaced Poisson process, including zero detection. Reading. |
| Proposition 1 | Restricted construction: two reporting/incident-rate pairs share one positive observed first-report rate. Domain. |
| Lemma 2; Appendix D.8.2 | Deferred; uncredited. The current arrival-time premises are incompatible. Conditioning. |
| Theorem 1; Appendix Theorem 2 | Exact. |
| Equation (3) | Endpoint convention: nonnegative rates and positive exposure include the zero-count maximum-likelihood estimate. Domain. |
| Equations (2), (4)–(7), (33)–(34) | Exact. |
Lemma 2 and Appendix D.8.2 require a consistent model of conditioning on an observed first report. The current premises combine an unconditional exponential first-arrival law with a fixed finite upper bound on that arrival. Both appendix claims remain outside the selected formalization surface; their proof repair is deferred. The main likelihood-factorization proof uses a separate causal observation model. This is a formalization gap, not a counterexample to the paper’s claims.
Proposition 1’s checked construction uses a positive observed first-report rate; Lemma 1 separately includes the zero-detection process. The memo states this restriction.
The Appendix B.2 clarification gives the two local algebra corrections and explains why the stated likelihood factorization is preserved.
The checked first-report process uses stationary homogeneous incident births. A nonstationary extension would require the corresponding nonhomogeneous marked-displacement theorem. Covariate-indexed report intensities, other duration laws, and alternate causal endpoint policies can reuse the same model separation once their process laws and definedness conditions are supplied.
The memo specifies calendar-time first reports and Equation (3)’s nonnegative-rate endpoint. Section 6 states Proposition 1’s positive-rate scope, and Section 7 links the two likelihood-algebra corrections.
Section 5 records the formalization gap in Lemma 2 and Appendix D.8.2.
The selected review surface contains eight transparent source-claim Specs, eight paired proof endpoints, fourteen source-mapped paper prerequisites, and two source-mapped reusable-library prerequisites. The compact source-facing surface is PaperInterface.lean, and the paired proof routes are collected in ProofInterface.lean.
The current machine-readable evidence is:
Each of the eight selected source claims has one semantic target and one proof endpoint; the proof endpoint is not counted as a second paper claim.
The source-defined premise families are:
The reporting-process roots have passed their independent semantic review. The incompatible arrival-time premises described in Section 5 remain confined to the deferred, uncredited Lemma 2 and Appendix D.8.2 claims.
| Paper item | Current disposition |
|---|---|
| Homogeneous reporting delay | Mean of the exponential report-delay law is
1/lambda. |
| Equation (2) | Exact Poisson count mass. |
| Equation (3) | Count-over-exposure estimator and global maximum on the explicit domain. |
| Equations (4)–(5) | Exact exponential Poisson-regression link. |
| Equation (6) | Regression likelihood with a rate-independent residual. |
| Equation (7) | Structural-zero and ordinary-Poisson branches, plus the independent-family product. |
| Equations (30)–(31) | Corrected first post-start gap and residual multiplier used in the Appendix proof. |
| Equations (33)–(34) | Exact NYC and Chicago three-way minimum endpoint definitions. |
The rate-times-exposure parameter and the forward homogeneous Poisson process are the source-mapped reusable definitions. The process root specifies Poisson increments at deterministic times; the finite observation model uses positive-rate independent exponential gaps. Neither asserts a Poisson count law at an arbitrary process-dependent random endpoint. The full checked dependency graph also retains the exponential and Poisson process models, observation windows, finite jump timelines, and their measure-theoretic and probability foundations.
The Dependency DAG records the source models, Conditions 1–2, checked claim clusters and two uncredited appendix claims, likelihood consequences, city endpoint formulas, and the empirical scope boundary. The rendered PDF was visually inspected after the scope update: labels and arrowheads are legible, reading order is clear, and no node, edge, or legend overlaps another node.
The fourteen source-mapped paper prerequisites cover incident births and lifetimes, reporting intensity and calendar-time first reports, the nonidentifiability construction, selected starts and causal endpoints, regression and zero-inflated likelihoods, and the NYC and Chicago observation endpoints. Their exact source connections and declaration bodies are in the paper prerequisite ledger and packet.
| Paper claim | Transparent semantic target | Proof endpoint |
|---|---|---|
| Homogeneous reporting-delay mean | sourceHomogeneousReportingDelayMeanSpec |
sourceHomogeneousReportingDelayMean |
| Theorem 1 / Appendix Theorem 2 | sourceTheorem1LikelihoodDecompositionSpec |
sourceTheorem1LikelihoodDecomposition |
| Equation (2) | sourceEquation2PoissonCountPMFSpec |
sourceEquation2PoissonCountPMF |
| Equation (3) | sourceEquation3MaximumLikelihoodEstimateSpec |
sourceEquation3MaximumLikelihoodEstimate |
| Equation (6) | sourceEquation6PoissonRegressionLikelihoodSpec |
sourceEquation6PoissonRegressionLikelihood |
| Equation (7) | sourceZeroInflatedLikelihoodExtensionSpec |
sourceZeroInflatedLikelihoodExtension |
| Lemma 1 | sourceLemma1CalendarTimeDurationObservedProcessSpec |
sourceLemma1CalendarTimeDurationObservedProcess |
| Proposition 1 | sourceProposition1CalendarTimeNonidentifiabilitySpec |
sourceProposition1CalendarTimeNonidentifiability |
| Lemma 2 | Deferred; not selected | No proof credit |
| Appendix D.8.2 shifted process | Deferred; not selected | No proof credit |
The selected surface has eight source claims, fourteen paper-specific semantic prerequisites, and two material library prerequisites. Existing judgments are reused only when their exact source and semantic inputs are unchanged. The changed reporting-process roots have passed independent semantic review. The two deferred appendix claims receive no source-coverage credit.
Human annotation is optional; no human review is fabricated or inferred from semantic screening.
The exact statements, source inputs, reasons, and reviewer fields are available in the linked JSON ledgers in Section 12 and in the human review packet.
The eight selected direct claims form the paper-result review denominator. The source map also retains model declarations, Appendix proof support, observed-data context, and the link between Theorem 1 and its Appendix Theorem 2 restatement. Lemma 2 and the Appendix D.8.2 claim remain visible as source claims with explicit scope exclusions and no proof or coverage credit. The fourteen paper prerequisites and two library prerequisites are semantic inputs rather than additional paper-result rows.