Skip to content

Five source records, four conditional receipts

Published measures stay distinct. The model stays a model.

The source preserves each paper's actual OR, RR, or HR and endpoint, then separately defines five bounded scenario coefficients and editorial weights. Lean checks range, formal cons monotonicity, pairwise definition equivalence, and permutation invariance—not causality, intervention safety, clinical comparability, or a personal outcome.

5
scenario inputs
4
named receipts
OR / RR / HR
evidence measures
connectmoveeat wellpurposestrength
Holt-Lunstad 2010 — survival OR 1.50 (95% CI 1.42–1.59)Arem 2015 — all-cause HR 0.69 (95% CI 0.67–0.70) at 7.5 to <15 MET-h/weekCorrected PREDIMED — primary CVD HR 0.69/0.72; all-cause HR 0.90 (0.69–1.18) / 1.12 (0.86–1.47)Cohen 2016 — adjusted pooled all-cause RR 0.83 (95% CI 0.75–0.91)Momma 2022 — RR 0.85 (0.79–0.93) any-vs-none; RR 0.83 (0.79–0.86) near 40 min/week; very-low certainty

Evidence records

Each receipt is conditional on the formal scenario-input contract. None proves empirical causality, clinical comparability, intervention safety, or a personal health outcome.

CONDITIONAL THEOREM

Katie.Verify.katie5_index_in_range

0 < compositeIndex katie5 ∧ compositeIndex katie5 ≤ 1

Katie/Verify.lean:130
CONDITIONAL THEOREM

Katie.Hazard.compositeIndex_cons_le

Consing an already-bounded ScenarioInput weakly reduces the defined composite index.

Katie/Hazard.lean:95
CONDITIONAL THEOREM

Katie.Selection.minimize_logIndex_iff_maximize_score

The pairwise composite-log-index ordering is the reverse of the defined total-score ordering.

Katie/Selection.lean:57
CONDITIONAL THEOREM

Katie.Verify.katie5_order_invariant

Permuting the same five formal inputs leaves the defined composite index unchanged.

Katie/Verify.lean:161