cert
plain-language theorem explainer
Packages a Flory-exponent certificate: domain cost vanishes at matched nonzero scales, stays nonnegative for positive monomer and end-to-end scales, and the canonical threshold is positive. Polymer or RS lattice workers cite it as the inhabited witness that the φ-lattice cost setup is well-posed. Proof is a three-field structure assembly from preexisting lemmas.
Claim. There is a Flory-exponent certificate: for every nonzero real $r$, the domain cost at matched scales $(r,r)$ is zero; for all positive monomer and end-to-end scales $m,e$, the domain cost is nonnegative; and the canonical threshold is strictly positive.
background
The module treats polymer end-to-end scaling $R \propto N^\nu$ on the Recognition Science $\varphi$-lattice in three dimensions, with the structural claim $\nu = 1/\varphi \approx 0.618$ (classical Flory $\approx 0.588$). Status is a structural theorem with no sorry and no axioms; the $\varphi$-step exponent is tied to 3D recognition-lattice self-avoidance.
FloryExponentCert is the local certificate bundle: equilibrium vanishing of domain cost on the diagonal, nonnegativity off it for positive scales, and positivity of a canonical threshold. Domain cost is the RS cost functional restricted to monomer versus end-to-end scale pairs; at equilibrium (equal nonzero scales) it hits zero, matching the J-cost minimum at identity.
Upstream, cost_nonneg from ObserverForcing states that the cost of any recognition event is nonnegative via Jcost_nonneg on a positive state. The in-module siblings domainCost_at_equilibrium, domainCost_nonneg, and canonicalThreshold_pos discharge the three certificate fields.
proof idea
One-line structure construction, not a tactic proof. The definition fills FloryExponentCert by pointing each field at an already-proved sibling: cost_at_eq from domainCost_at_equilibrium, cost_nonneg from domainCost_nonneg, and threshold_pos from canonicalThreshold_pos. No further algebraic reduction; inhabitance is pure assembly of those three facts.
why it matters
Gives the inhabited certificate that the polymer module's cost-and-threshold interface is satisfied, so downstream Flory-exponent arguments can assume a well-posed nonnegative domain cost with a positive threshold and vanishing equilibrium. The module frames this as structural support for $\nu = 1/\varphi$ from 3D $\varphi$-lattice self-avoidance (forcing-chain landmarks T6 $\varphi$ and T8 $D=3$). No used_by edges are recorded yet; the sibling cert_inhabited is the natural consumer. Does not itself derive the numerical exponent; it only certifies the cost setup the exponent argument sits on.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.