RSStringLandscapeRS
plain-language theorem explainer
Packages three structural properties used in the RS comparison with the string landscape: diagonal domain cost vanishes off zero, domain cost is nonnegative on positive pairs, and the canonical threshold is positive. Downstream certificates inhabit this record to mark the landscape comparison as a zero-sorry structural theorem. Pure definitional packaging of field obligations; no proof body.
Claim. A record of three properties: (i) for every nonzero real $r$, the domain cost of the pair $(r,r)$ equals $0$; (ii) for all positive reals $m,e$, the domain cost of $(m,e)$ is nonnegative; (iii) the canonical threshold is strictly positive.
background
The module contrasts the string-theory vacuum count (~$10^{500}$) with Recognition Science estimates built from powers of $\varphi$ (e.g. $\varphi^{\varphi^D}$ with $D=3$, or gap-scaled ladders). Status is structural: zero sorry, zero axiom.
domainCost is the local cost on a pair of positive reals (mass/energy-style arguments). The first field forces the diagonal to sit at the cost minimum away from zero; the second is the nonnegativity law. Upstream, ObserverForcing already has cost_nonneg: every recognition event has nonnegative cost via Jcost_nonneg on a positive state. The third field requires the module's canonicalThreshold to be positive, the cutoff used when comparing landscape scales.
The structure is the interface that a concrete certificate must fill; it does not itself compute vacuum counts.
proof idea
Definitional structure with three fields and no proof body. Inhabitation is deferred to the sibling cert, which assigns domainCost_at_eq, domainCost_nonneg, and canonicalThreshold_pos to the three fields. Those siblings carry the actual algebraic content (diagonal vanishing of domain cost, nonnegativity, positivity of the threshold).
why it matters
Gives a named, checkable interface for the RS-side of the string-landscape comparison in Foundation. Downstream, cert builds a concrete inhabitant and cert_inhabited proves Nonempty RSStringLandscapeRS, closing the module's structural claim (0 sorry, 0 axiom).
In the broader framework this sits beside the forcing chain (T5 J-uniqueness, T6 $\varphi$, T8 $D=3$) and the J-cost nonnegativity law: the landscape comparison is framed as cost and threshold structure rather than a dynamical vacuum-counting theorem. It does not resolve the physical size of the landscape; it certifies that the RS cost/threshold package is well-formed for that comparison.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.