logicaffeine_proof/
thermal_replay.rs

1//! Thermal-map replay — the independent judge of a claimed steady-state temperature map.
2//!
3//! The crown unification: the thermal solve `G·ΔT = P` IS the linear-system mathematics the
4//! relaxation lane certifies ([`crate::relax_replay`]) — one trust pattern, two physical
5//! planes. The claim is NEUTRAL data: a conductance edge list, ground (boundary)
6//! conductances, power injections, and the claimed per-node temperature rise — all exact
7//! rationals. [`check_thermal_claim`] reassembles the Laplacian ITSELF from the primitive
8//! edges (it never trusts an assembled matrix), re-multiplies exactly, and demands
9//! `G·ΔT = P` as an EQUALITY — the producer solved exactly, so nothing less certifies.
10//! Fail-closed throughout: malformed shapes, non-positive conductances, negative injections,
11//! a node with no path to any ground (heat with nowhere to go), or a negative claimed rise
12//! are rejections, never a verdict.
13
14use logicaffeine_base::numeric::Rational;
15
16/// The neutral thermal claim a stack's thermal solve emits.
17#[derive(Clone, Debug, PartialEq)]
18pub struct ThermalClaim {
19    /// Node count (ΔT is per node, kelvin above ambient).
20    pub n: usize,
21    /// Undirected conductance edges `(a, b, g)` in W/K, `g > 0`.
22    pub edges: Vec<(usize, usize, Rational)>,
23    /// Boundary conductances to ambient `(node, g)` in W/K, `g > 0`.
24    pub grounds: Vec<(usize, Rational)>,
25    /// Power injections `(node, watts)`, non-negative.
26    pub injections: Vec<(usize, Rational)>,
27    /// The claimed steady-state rise above ambient, per node.
28    pub delta_t: Vec<Rational>,
29}
30
31/// What a TRUE map says. The junction-limit judgment belongs to the cooling phase's
32/// consumer — the verdict reports the physics, it does not editorialize.
33#[derive(Clone, Debug, PartialEq)]
34pub struct ThermalVerdict {
35    pub hottest_node: usize,
36    pub hottest_delta_t: Rational,
37}
38
39/// THE judge. `Some(verdict)` iff the claim is well-formed, physically coherent, and the
40/// reassembled `G·ΔT` equals `P` EXACTLY at every node.
41pub fn check_thermal_claim(claim: &ThermalClaim) -> Option<ThermalVerdict> {
42    let n = claim.n;
43    if n == 0 || claim.delta_t.len() != n {
44        return None;
45    }
46    for (a, b, g) in &claim.edges {
47        if *a >= n || *b >= n || a == b || !g.is_positive() {
48            return None;
49        }
50    }
51    for (node, g) in &claim.grounds {
52        if *node >= n || !g.is_positive() {
53            return None;
54        }
55    }
56    if claim.grounds.is_empty() {
57        return None; // heat with nowhere to go — no steady state exists
58    }
59    for (node, w) in &claim.injections {
60        if *node >= n || w.is_negative() {
61            return None;
62        }
63    }
64    // Positivity: with non-negative injections, no node sits below ambient.
65    if claim.delta_t.iter().any(|t| t.is_negative()) {
66        return None;
67    }
68
69    // Connectivity: every node must reach a grounded node through the edge list.
70    let mut adj = vec![Vec::new(); n];
71    for (a, b, _) in &claim.edges {
72        adj[*a].push(*b);
73        adj[*b].push(*a);
74    }
75    let mut reached = vec![false; n];
76    let mut queue: Vec<usize> = claim.grounds.iter().map(|(g, _)| *g).collect();
77    for g in &queue {
78        reached[*g] = true;
79    }
80    while let Some(v) = queue.pop() {
81        for w in &adj[v] {
82            if !reached[*w] {
83                reached[*w] = true;
84                queue.push(*w);
85            }
86        }
87    }
88    if reached.iter().any(|r| !r) {
89        return None;
90    }
91
92    // Reassemble the Laplacian row-action INDEPENDENTLY and demand exact balance:
93    //   Σ_edges g·(ΔT_i − ΔT_j) + g_ground·ΔT_i = P_i  at every node i.
94    let mut balance: Vec<Rational> = vec![Rational::zero(); n];
95    for (a, b, g) in &claim.edges {
96        let diff = claim.delta_t[*a].sub(&claim.delta_t[*b]);
97        balance[*a] = balance[*a].add(&g.mul(&diff));
98        balance[*b] = balance[*b].sub(&g.mul(&diff));
99    }
100    for (node, g) in &claim.grounds {
101        balance[*node] = balance[*node].add(&g.mul(&claim.delta_t[*node]));
102    }
103    let mut p: Vec<Rational> = vec![Rational::zero(); n];
104    for (node, w) in &claim.injections {
105        p[*node] = p[*node].add(w);
106    }
107    if balance.iter().zip(&p).any(|(bi, pi)| bi != pi) {
108        return None;
109    }
110
111    let hottest = (0..n).max_by(|a, b| claim.delta_t[*a].cmp(&claim.delta_t[*b]))?;
112    Some(ThermalVerdict {
113        hottest_node: hottest,
114        hottest_delta_t: claim.delta_t[hottest].clone(),
115    })
116}
logicaffeine_proof/thermal_replay.rs

logicaffeine_proof/
thermal_replay.rs
