coeffMag_foldPlusOneStep
plain-language theorem explainer
The lemma shows that the magnitude quantization of a Galerkin coefficient after one fold-plus-one update equals the 32-bit clamped original magnitude plus one. Researchers bridging discrete 2D Galerkin expansions to LNAL voxel encodings would cite it for update consistency in fluid simulations. The tactic proof introduces the signed integer encoding of the coefficient, applies the clamp positivity result, reduces via floor of absolute cast, and resolves the absolute value by sign cases.
Claim. Let $u$ be a state of real coefficients indexed by a finite set of 2D modes up to truncation level $N$ and by two vector components. For any such index $i$, the magnitude quantization of the coefficient after the one-step update equals the 32-bit integer clamp of the original magnitude plus one.
background
The module states the one-step simulation bridge between the discrete 2D Galerkin model and spatial LNAL execution semantics at milestone M3, packaging claims as an explicit SimulationHypothesis without axioms or sorries. GalerkinState N is the Euclidean space of real coefficients over the finite set of modes (integer pairs from -N to N) and two components. The magnitude quantization of a real coefficient is the floor of its absolute value; the sign encoding returns -1 or +1 according to the sign of the input. The one-step update encodes the coefficient as a signed integer whose absolute value is the clamped new magnitude.
proof idea
The tactic proof sets the coefficient to x and shows that its magnitude plus one is at least 1. It defines m as the clamped magnitude and z as the signed integer via the sign encoding. Positivity of m is obtained from the clamp positivity lemma. Simplification reduces the new magnitude to the floor of the absolute value of the cast z. The floor-abs-intCast lemma converts this to the absolute value of z, after which case analysis on the sign of x shows that the absolute value equals m.
why it matters
The result is invoked by the voxel-step consistency lemma that equates LNAL voxel execution of the fold program to the encoded updated state. It supplies one concrete piece of the discrete dynamics bridge inside the SimulationHypothesis for the ClassicalBridge.Fluids module. In the Recognition Science setting it ensures that magnitude updates remain compatible with the quantized encoding used for classical limits, consistent with the discrete tier structure noted in the nucleosynthesis tiers upstream.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.