ZenoProtection
plain-language theorem explainer
ZenoProtection records a target quantum state together with its measurement frequency and expected fidelity under frequent observation. Workers modeling measurement-induced state stabilization in quantum information or memory devices would cite the structure when linking ledger actualization to the watched-pot suppression of transitions. The declaration is a bare record constructor with three fields and no computational reduction.
Claim. A record consisting of a string identifier for the protected quantum state, a real number giving the measurement frequency in hertz, and a real number giving the expected state fidelity after repeated measurements.
background
The Quantum.ZenoEffect module derives the quantum Zeno effect from Recognition Science ledger actualization. Each measurement commits a ledger entry that resets the evolving state, while evolution between measurements remains probabilistic. The supplied module document states that frequent actualization keeps the system pinned to the measured state, yielding the limit P_final → 0 as the number of measurements N → ∞ for the transition probability P(t) = sin²(Ωt/2).
proof idea
The declaration is a structure definition containing only field declarations. No lemmas or tactics are invoked; the record is assembled directly from the three components target_state, measurement_rate, and fidelity.
why it matters
The structure supplies the data container needed for the patent opportunity of Zeno-based quantum memory protection listed in the module header. It supports the QF-010 program goal of obtaining the Zeno effect from ledger actualization and sits upstream of sibling declarations such as quantum_zeno_effect and zeno_from_ledger_actualization. The construction aligns with the Recognition Science emphasis on measurement as ledger commitment rather than an external postulate.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.