%% CAS_F0000_VERIFY.m — Geometric scaling lemmas (axiomatic layer)
%  Pillar : Geometry (root layer — F0001–F0031 are downstream consequences)
%  Scope  : Dilation r → λr on embedded surface Σ ⊂ R³
%  Chain  : metric g → second fundamental form b → shape operator S = g⁻¹b
%           → curvatures → determinant → area element → γ scaling
%  Status : Axiomatic — CAS verifies the scaling algebra; the lemmas
%           themselves are standard differential geometry.
%  Hardening: isAlways(..., 'Unknown', 'false') on every symbolic assertion
%            symvar-based presence checks; solver and has-function avoided

clear; clc;
fprintf('\n=== CAS F0000 : Geometric scaling lemmas (axiomatic layer) ===\n\n');

%% ── Symbols ──────────────────────────────────────────────────
syms lam real positive                   % dilation parameter λ
syms gamma_s real positive               % γ factor (display-area context)
syms V ell real positive                 % volume, characteristic length

% 2×2 symmetric metric and second fundamental form (surface geometry)
syms g11 g12 g22 real
syms b11 b12 b22 real

% Non-degeneracy: metric is invertible (regular immersion)
g_det_expr = g11*g22 - g12^2;
assumeAlso(g_det_expr ~= 0);

% 3×3 Jacobian entries (for determinant scaling)
syms y1 y2 y3 y4 y5 y6 y7 y8 y9 real
syms e1 e2 e3 e4 e5 e6 e7 e8 e9 real

%% ── A. Inputs ────────────────────────────────────────────────
%  Embedded surface Σ ⊂ R³ with regular immersion r(u,v).
%  Dilation: r_λ(u,v) = λ r(u,v).
%  Induced metric: g_ij = ∂r/∂u^i · ∂r/∂u^j  →  g_λ = λ² g
%  Second fundamental form: b_ij = −∂r/∂u^i · ∂n/∂u^j  →  b_λ = λ b
%  Shape operator: S = g⁻¹ b  →  S_λ = (1/λ) S
%  Jacobian: D_q X = λ D_q Y + D_q E  →  det scaling

%% ── Step 1: γ scaling identity (display area) ────────────────
%  ℓ' = ℓ/γ,  A_d = V/ℓ,  A_d' = V/ℓ'
%  ⇒ A_d' = V/(ℓ/γ) = γ V/ℓ = γ A_d
A_d  = V / ell;
ell_p = ell / gamma_s;
A_d_p = V / ell_p;
res1 = simplify(A_d_p - gamma_s * A_d);
assert(isAlways(res1 == 0, 'Unknown', 'false'), ...
    'FAIL Step 1: A_d'' ≠ γ A_d');
fprintf('Step 1  PASS — γ scaling: A_d'' = γ·A_d (display area identity)\n');

%% ── Step 2: Metric dilation g_λ = λ² g (2×2 matrix) ─────────
g_mat = [g11 g12; g12 g22];             % symmetric metric
g_lam = lam^2 * g_mat;                  % dilated metric
% Verify all 4 elements
res2 = simplify(g_lam - lam^2 * g_mat);
for r = 1:2
    for c = 1:2
        assert(isAlways(res2(r,c) == 0, 'Unknown', 'false'), ...
            sprintf('FAIL Step 2: g_lam(%d,%d) ≠ λ²·g(%d,%d)', r, c, r, c));
    end
end
fprintf('Step 2  PASS — Metric dilation: g_λ = λ²·g (all 4 components)\n');

%% ── Step 3: Second fundamental form dilation b_λ = λ b ───────
b_mat = [b11 b12; b12 b22];             % symmetric second fundamental form
b_lam = lam * b_mat;                    % dilated second fundamental form
res3 = simplify(b_lam - lam * b_mat);
for r = 1:2
    for c = 1:2
        assert(isAlways(res3(r,c) == 0, 'Unknown', 'false'), ...
            sprintf('FAIL Step 3: b_lam(%d,%d) ≠ λ·b(%d,%d)', r, c, r, c));
    end
end
fprintf('Step 3  PASS — Second fundamental form: b_λ = λ·b (all 4 components)\n');

%% ── Step 4: Shape operator scaling S_λ = (1/λ) S (matrix) ───
%  S = g⁻¹ b,  S_λ = g_λ⁻¹ b_λ = (λ²g)⁻¹(λb) = (1/λ) g⁻¹ b = S/λ
S_mat   = inv(g_mat) * b_mat;
S_lam   = inv(g_lam) * b_lam;
S_expected = S_mat / lam;
res4 = simplify(S_lam - S_expected);
for r = 1:2
    for c = 1:2
        assert(isAlways(res4(r,c) == 0, 'Unknown', 'false'), ...
            sprintf('FAIL Step 4: S_lam(%d,%d) ≠ S(%d,%d)/λ', r, c, r, c));
    end
end
fprintf('Step 4  PASS — Shape operator: S_λ = S/λ (all 4 components)\n');

%% ── Step 5: Gaussian curvature K_λ = K/λ² ───────────────────
%  K = det(S),  K_λ = det(S_λ) = det(S/λ) = (1/λ²) det(S) = K/λ²
K_orig = det(S_mat);
K_lam  = det(S_lam);
res5 = simplify(K_lam - K_orig / lam^2);
assert(isAlways(res5 == 0, 'Unknown', 'false'), ...
    'FAIL Step 5: K_λ ≠ K/λ²');
fprintf('Step 5  PASS — Gaussian curvature: K_λ = K/λ²\n');

%% ── Step 6: Mean curvature H_λ = H/λ ────────────────────────
%  H = tr(S)/2,  H_λ = tr(S_λ)/2 = tr(S/λ)/2 = H/λ
H_orig = trace(S_mat) / 2;
H_lam  = trace(S_lam) / 2;
res6 = simplify(H_lam - H_orig / lam);
assert(isAlways(res6 == 0, 'Unknown', 'false'), ...
    'FAIL Step 6: H_λ ≠ H/λ');
fprintf('Step 6  PASS — Mean curvature: H_λ = H/λ\n');

%% ── Step 7: Determinant identity det(λY+E) = λ³ det(Y+E/λ) ─
%  3×3 concrete symbolic matrices
Y_mat = [y1 y2 y3; y4 y5 y6; y7 y8 y9];
E_mat = [e1 e2 e3; e4 e5 e6; e7 e8 e9];
lhs7 = det(lam * Y_mat + E_mat);
rhs7 = lam^3 * det(Y_mat + E_mat / lam);
res7 = simplify(expand(lhs7) - expand(rhs7));
assert(isAlways(res7 == 0, 'Unknown', 'false'), ...
    'FAIL Step 7: det(λY+E) ≠ λ³·det(Y+E/λ)');
fprintf('Step 7  PASS — Determinant factoring: det(λY+E) = λ³·det(Y+E/λ)\n');

%% ── Step 8: Pure dilation det(λY) = λ³ det(Y) ──────────────
lhs8 = det(lam * Y_mat);
rhs8 = lam^3 * det(Y_mat);
res8 = simplify(lhs8 - rhs8);
assert(isAlways(res8 == 0, 'Unknown', 'false'), ...
    'FAIL Step 8: det(λY) ≠ λ³·det(Y)');
fprintf('Step 8  PASS — Pure dilation: det(λY) = λ³·det(Y)\n');

%% ── Step 9: Area element scaling √det(g_λ) = λ² √det(g) ────
%  For 2×2 metric: det(g_λ) = det(λ²g) = λ⁴ det(g)
%  → √det(g_λ) = λ² √det(g)
det_g     = det(g_mat);
det_g_lam = det(g_lam);
%  Verify det(g_λ) = λ⁴ det(g)
res9 = simplify(det_g_lam - lam^4 * det_g);
assert(isAlways(res9 == 0, 'Unknown', 'false'), ...
    'FAIL Step 9: det(g_λ) ≠ λ⁴·det(g)');
fprintf('Step 9  PASS — Area element: det(g_λ) = λ⁴·det(g) → √det scales as λ²\n');

%% ── Step 10: Inverse metric scaling g_λ⁻¹ = (1/λ²) g⁻¹ ────
inv_g     = inv(g_mat);
inv_g_lam = inv(g_lam);
res10 = simplify(inv_g_lam - inv_g / lam^2);
for r = 1:2
    for c = 1:2
        assert(isAlways(res10(r,c) == 0, 'Unknown', 'false'), ...
            sprintf('FAIL Step 10: g_lam_inv(%d,%d) ≠ g_inv(%d,%d)/λ²', r, c, r, c));
    end
end
fprintf('Step 10 PASS — Inverse metric: g_λ⁻¹ = g⁻¹/λ² (all 4 components)\n');

%% ── Step 11: Self-test — wrong metric exponent detected ──────
%  Wrong assumption: g_λ = λ³·g (instead of λ²·g)
%  Then S_wrong = (λ³g)⁻¹(λb) = (1/λ³)g⁻¹(λb) = (1/λ²) g⁻¹b = S/λ²
%  This gives S/λ² ≠ S/λ (the correct scaling)
g_wrong = lam^3 * g_mat;
S_wrong = inv(g_wrong) * b_lam;      % b_lam = λb is still correct
S_correct_scaling = S_mat / lam;
res11 = simplify(S_wrong - S_correct_scaling);
%  At least one element must be nonzero
any_nonzero = false;
for r = 1:2
    for c = 1:2
        if ~isAlways(res11(r,c) == 0, 'Unknown', 'false')
            any_nonzero = true;
            break;
        end
    end
    if any_nonzero, break; end
end
assert(any_nonzero, ...
    'FAIL Step 11: wrong metric exponent λ³ not detected');
fprintf('Step 11 PASS — Wrong metric exponent (λ³ instead of λ²) detected\n');

%% ── Summary ─────────────────────────────────────────────────
fprintf('\n✓ ALL 11 ASSERTIONS PASSED — F0000 audit complete.\n');
fprintf('  Geometric scaling chain: g→λ²g, b→λb, S→S/λ, K→K/λ², H→H/λ\n');
fprintf('  Determinant: det(λY+E)=λ³det(Y+E/λ), area element scales as λ²\n');
fprintf('  This layer is axiomatic root for F0001–F0031.\n');