z_rung_NV
plain-language theorem explainer
The declaration assigns the natural number 7 as the Z-rung for NV-center qubits under the BIT-coupling model. Quantum-computing researchers calibrating decoherence times across substrate families would cite this constant when fixing the exponent in a T2 ratio. The assignment is a direct constant definition with no further computation or lemmas.
Claim. The Z-rung assigned to the NV-center qubit class is $7$.
background
In the Decoherence from BIT module the Z-rung is an integer label on each qubit substrate class that determines the exponent k in the forced relation T2(class_a)/T2(class_b) = phi^k. The rung function itself appears in upstream definitions such as rung : OreClass -> Nat in AsteroidOreSpectroscopy and the noncomputable rung : Fermion -> Int in RSBridge.Anchor, both of which map physical classes onto the phi-ladder integers used by the mass and calibration machinery. The module treats every specific class-to-rung map as a hypothesis-grade empirical input rather than a derived theorem.
proof idea
This is a direct definition that sets the constant z_rung_NV to the literal natural number 7. No lemmas or tactics are invoked; the body is simply the numeral assignment.
why it matters
The definition supplies the NV-center rung hypothesis required by the structural theorem T2_ratio_is_phi_power, which fixes the integer exponent for any cross-class T2 ratio once the two rungs are known. It therefore completes one of the per-class calibration targets listed in the module's Track F1 plan. The assignment touches the open empirical question of whether the chosen rung values remain stable under improved T2 measurements on NV ensembles.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.