quadratic1D_zero_valid
plain-language theorem explainer
Zero is the sole valid state under the strain-ledger predicate in the one-dimensional quadratic model. Researchers constructing concrete RRF examples for continuous optimization would cite this result to anchor base-case verification. The proof is a direct term that pairs the equilibrium theorem at zero with the closed-ledger property.
Claim. In the quadratic model on the real line with strain functional $J(x)=x^2$, the state $0$ satisfies both balanced strain and closed ledger, hence lies in the valid set of the combined strain-ledger structure.
background
The quadratic model takes State as the real line and defines the strain functional by the squared Euclidean norm. An octave packages this functional with observation channels. The isValid predicate on a strain-ledger declares a state valid exactly when strain is balanced and the ledger is closed.
proof idea
The proof is a term-mode construction that directly supplies the pair consisting of the equilibrium theorem for the quadratic strain at zero together with the closed-ledger fact instantiated at zero.
why it matters
This theorem supplies the base valid state for the quadratic model, which serves as a minimal example of an RRF structure admitting continuous optimization. It closes the verification that the zero state satisfies the full validity predicate in the combined strain-ledger. The result remains internal to the model and does not engage the Recognition Science constants or the forcing chain.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.