cert
plain-language theorem explainer
The definition cert assembles a VarveCert structure asserting that the summer-to-winter varve thickness ratio exceeds one, lies inside the empirical interval (1.1, 2.5), and produces zero cost when the two thicknesses are equal. Stratigraphers and Recognition Science modelers cite it to connect observed sediment couplets to the phi minimum of the J-cost function. The construction is a direct record that invokes three upstream theorems to populate the structure fields.
Claim. Let $r$ be the summer-to-winter varve thickness ratio. The object cert is the structure satisfying $1 < r$, $1.1 < r < 2.5$, and $varveCost(t,t)=0$ for all $t≠0$.
background
Varves are annual sediment couplets consisting of a light summer layer and a dark winter layer. The module predicts that the ratio of summer to winter thickness equals phi, the value that minimizes the recognition cost J under symmetric seasonal forcing, and places this ratio inside the empirical band (1.1, 2.5) drawn from Zolitschka 2007 and De Geer records. The structure VarveCert collects the three required assertions: the ratio exceeds unity, falls inside the observed band, and the cost function vanishes on equal thicknesses.
proof idea
The definition is a direct record construction that supplies the three fields of VarveCert by naming the corresponding theorems: varveSummerWinterRatio_gt_one for the first field, varveSummerWinterRatio_in_empirical_band for the second, and varveCost_at_ratio for the third.
why it matters
This definition supplies the canonical certificate that the RS-predicted ratio phi lies inside the empirical varve band and yields zero cost at equal thicknesses. It completes the structural theorem for the stratigraphy module, whose falsifier is any continuous varve record whose time-averaged ratio falls outside (1.1, 2.5). The construction ties the phi-ladder minimum to observable sediment data.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.