docs(proof-suite): tighten S1/E3 comments — Variable not global axiom

Clarify that the Section Variables in S1_noether_energy.v and
E3_cantilever_deflection.v are discharged as explicit arguments
at End-Section, not global axioms. The old phrasing ("no opaque
constants / no global axioms") was technically correct for Variables
but borrowed language from the Parameter world. New phrasing —
"no free module-level declarations" — is precise for both Variables
and Parameters and avoids conflating the two.

No proof content changed. Comment-only update.

Co-Authored-By: Claude Sonnet 4.6 <noreply@anthropic.com>

Author: hyperpolymath

proofs/canonical-proof-suite/E3_cantilever_deflection.v

@@ -95,7 +95,7 @@
    file type-checks under Rocq 9.1.x with the kernel's safe
    mode; all abstract types and functions are declared as Section
    Variables and are discharged into explicit arguments at
-   Section close, so no global axioms leak out of this module.
+   Section close, so no free module-level declarations leak out of this module.
 
    FOLLOW-UP SESSIONS SHOULD:
 

proofs/canonical-proof-suite/S1_noether_energy.v

@@ -75,8 +75,8 @@
      abstraction is intentionally extensional so the scaffold
      stands on its own and can be specialised later.
    - The Variables declared here are Section Variables (discharged
-     into explicit arguments at End Mechanics), not global axioms;
-     no opaque constants leak out of this module.
+     into explicit arguments at End Mechanics), not free module-level
+     declarations; no opaque terms leak out of this module.
    ==================================================================== *)
 
 (* No library imports needed: core vernacular plus the Rocq prelude