fix(proof-suite): wrap free Parameters in Sections for S3 + S5

S3_second_law.v: four Parameters (State, state_eq_dec, kernel, log2)
were global axioms outside any section. Wrapped in Section S3Proof.
and converted to Variable — coqc exit 0 confirmed.

S5_shannon_source_coding.v: three Parameters (Symbol, symbol_eq_dec,
log2) likewise outside any section. Wrapped in Section S5Proof. and
converted to Variable — coqc exit 0 confirmed.

S1/S2/E3/E5 already have Parameters inside named sections
(Mechanics/Electrostatics/BeamMechanics/Carriers) — exempt per
panic-attack ProofDrift Section Carrier rule.

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

Author: hyperpolymath

proofs/canonical-proof-suite/S3_second_law.v

@@ -64,8 +64,13 @@ Open Scope Q_scope.
    §1  Finite state alphabet
    ==================================================================== *)
 
-Parameter State : Type.
-Parameter state_eq_dec : forall x y : State, {x = y} + {x <> y}.
+(* All abstract types and functions are section variables so no global
+   Parameter axioms are introduced — every theorem is automatically
+   universally quantified over them when the section closes. *)
+Section S3Proof.
+
+Variable State : Type.
+Variable state_eq_dec : forall x y : State, {x = y} + {x <> y}.
 
 Lemma state_eq_dec_refl : forall x : State,
   exists p : x = x, state_eq_dec x x = left p.
@@ -106,7 +111,7 @@ Definition distribution_prob (d : Distribution) (s : State) : Q :=
    We represent it as a function State -> State -> Q for simplicity;
    row-stochasticity is a separate hypothesis. *)
 
-Parameter kernel : State -> State -> Q.
+Variable kernel : State -> State -> Q.
 
 (* Detailed balance against a stationary distribution pi:
      pi(i) * P(j | i) = pi(j) * P(i | j). *)
@@ -128,7 +133,7 @@ Definition kernel_rows_sum_to_one (support_list : list State) : Prop :=
 
 (* Abstract log2 parameter — see module header for the deferred
    real-valued layer. *)
-Parameter log2 : Q -> Q.
+Variable log2 : Q -> Q.
 
 Definition entropy_term (p : Q) : Q := - (p * log2 p).
 
@@ -288,3 +293,5 @@ Proof. intro d. unfold h_functional. reflexivity. Qed.
    End of scaffold. The headline symbol is intentionally not declared
    here; see the module header for the deferred work.
    ==================================================================== *)
+
+End S3Proof.

proofs/canonical-proof-suite/S5_shannon_source_coding.v

@@ -81,8 +81,13 @@ Open Scope Q_scope.
    byte-alphabets, or any other finite type.
    ==================================================================== *)
 
-Parameter Symbol : Type.
-Parameter symbol_eq_dec : forall x y : Symbol, {x = y} + {x <> y}.
+(* Section variables avoid global Parameter axioms — each theorem is
+   universally quantified over Symbol, symbol_eq_dec, and log2
+   automatically when the section closes. *)
+Section S5Proof.
+
+Variable Symbol : Type.
+Variable symbol_eq_dec : forall x y : Symbol, {x = y} + {x <> y}.
 
 (* The decider on a symbol with itself takes the left branch. We
    state this in the existential form because the proof term carried
@@ -185,7 +190,7 @@ Definition expected_length (c : PrefixCode) (d : Distribution) : Q :=
             snd sp * nat_to_Q (code_length c (fst sp)))
          (support d)).
 
-Parameter log2 : Q -> Q.
+Variable log2 : Q -> Q.
 
 Definition entropy_term (p : Q) : Q := - (p * log2 p).
 
@@ -415,3 +420,5 @@ Qed.
    resulting per-symbol bound into the theorem above to recover
    the unconditional Shannon source-coding inequality
    E[|c|] >= H(d). *)
+
+End S5Proof.