continuousOn_dynamicStructureProfile
plain-language theorem explainer
If a real field profile q is continuous on the unit interval, the induced structure profile G(x)=1+(q(x))^2 is continuous there as well. Gravity continuum-smearing arguments cite this to pass continuity from q into the dynamic inverse-metric shape before invoking banked weighted quadrature. The proof unfolds the model definition and adds continuity of a constant to the square of a continuous map.
Claim. Let $q:\mathbb{R}\to\mathbb{R}$ be continuous on the closed unit interval $[0,1]$. Then the induced structure profile $x\mapsto 1+(q(x))^2$ is continuous on $[0,1]$.
background
This module (Wave C2 R3) extends the banked fixed-background continuum reach so the structure-function profile is induced by a continuum field profile q through the same algebraic law that appears in the dynamic lattice bracket: G(x)=1+(q x)^2. That G is the continuum shape of the concrete dynamic inverse metric along q, and the package is witnessed by the HamDyn family built from that inverse metric.
The model definition dynamicStructureProfile packages exactly G(x)=1+(q(x))^2. Admissible profiles are those continuous on Icc 0 1; the module deliberately does not demand global Continuity. Upstream sampling and phase infrastructure (eight-tick phases, continuum sampling onto periodic lattices) sit in the gravity analysis stack, but this lemma only needs elementary continuity calculus on the unit interval.
Honesty constraints from the module: this is the smearing half of the continuum story; the sampled-lapse Wronskian rate-h limit stays open in the ledger terminal, and gap5 constraint recovery is not flipped here.
proof idea
Term-mode proof. Unfold the model definition so the goal is continuity of x ↦ 1 + (q x)^2 on Icc 0 1. Apply continuousOn_const.add to the sum of the constant map 1 and the square of q. Continuity of the square is obtained from the hypothesis ContinuousOn q (Icc 0 1) via ContinuousOn.pow with exponent 2. No further lemmas are required.
why it matters
Binding continuity lemma for the dynamic continuum-smearing rung. Downstream, dynamic_weighted_continuum_reach uses it so every continuous-on-[0,1] field profile induces a DynamicWeightedContinuumReach by composing through 1+q^2 into the banked fixed-background quadrature. That reach is the first component of the R3 headline residual typedResidual_gap5_dynamic_continuum_smearing.
Further out, dynamic_bracket_shape_continuum_limit (Dirac algebra continuum module) quotes the same G=1+q^2 shape when proving that sampled-and-scaled freestanding dynamic-bracket shape sums converge to the continuum Dirac hypersurface-deformation density. The lemma therefore sits on the path from lattice dynamic brackets to continuum structure functions, without claiming the still-open full dirac_algebra_continuum_limit ledger name or any rate-h Wronskian binding.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.