omena_abstract_value/
cascade_family.rs

1use crate::{ABSTRACT_VALUE_CASCADE_FAMILY_CLAIM_LEVEL_V0, AbstractPropertyValueV0};
2use serde::Serialize;
3use std::collections::{BTreeMap, BTreeSet};
4
5/// Research-staged cascade-family substrate for M6 positioning.
6///
7/// This is intentionally framing-neutral: it records context-indexed value
8/// families and restriction morphisms without claiming a sheaf/cosheaf theorem
9/// or committing paper-stage terminology.
10#[derive(Debug, Clone, PartialEq, Eq, Serialize)]
11#[serde(rename_all = "camelCase")]
12pub struct CascadeValueFamilyV0 {
13    pub schema_version: &'static str,
14    pub product: &'static str,
15    pub framing: &'static str,
16    pub claim_level: &'static str,
17    pub property_name: String,
18    pub supported_readings: Vec<&'static str>,
19    pub context_value_count: usize,
20    pub restriction_map_count: usize,
21    pub property_consistent: bool,
22    pub dangling_restriction_count: usize,
23    pub theorem_claimed: bool,
24    pub members: Vec<CascadeValueFamilyMemberV0>,
25    pub restriction_maps: Vec<CascadeRestrictionMapV0>,
26}
27
28#[derive(Debug, Clone, PartialEq, Eq, PartialOrd, Ord, Serialize)]
29#[serde(rename_all = "camelCase")]
30pub struct CascadeContextV0 {
31    pub id: String,
32    #[serde(skip_serializing_if = "Option::is_none")]
33    pub parent_id: Option<String>,
34    pub selectors: Vec<String>,
35    pub conditions: Vec<String>,
36    pub layers: Vec<String>,
37}
38
39#[derive(Debug, Clone, PartialEq, Eq, Serialize)]
40#[serde(rename_all = "camelCase")]
41pub struct CascadeValueFamilyMemberV0 {
42    pub context: CascadeContextV0,
43    pub value: AbstractPropertyValueV0,
44}
45
46#[derive(Debug, Clone, PartialEq, Eq, PartialOrd, Ord, Serialize)]
47#[serde(rename_all = "camelCase")]
48pub struct CascadeRestrictionMapV0 {
49    pub parent_context_id: String,
50    pub child_context_id: String,
51    pub morphism: CascadeMorphismV0,
52}
53
54#[derive(Debug, Clone, PartialEq, Eq, PartialOrd, Ord, Serialize)]
55#[serde(rename_all = "camelCase")]
56pub struct CascadeMorphismV0 {
57    pub kind: &'static str,
58    pub direction: &'static str,
59    pub preserves_property_name: bool,
60    pub evidence: Vec<&'static str>,
61}
62
63#[derive(Debug, Clone, PartialEq, Eq, Serialize)]
64#[serde(rename_all = "camelCase")]
65pub struct CascadeStalkEvaluationV0 {
66    pub schema_version: &'static str,
67    pub product: &'static str,
68    pub claim_level: &'static str,
69    pub property_name: String,
70    pub requested_context_id: String,
71    pub requested_context_exists: bool,
72    #[serde(skip_serializing_if = "Option::is_none")]
73    pub resolved_context_id: Option<String>,
74    pub restriction_path: Vec<String>,
75    pub used_restriction_map_count: usize,
76    pub bounded_by_context_count: usize,
77    pub bounded_resolution_ready: bool,
78    pub theorem_claimed: bool,
79    #[serde(skip_serializing_if = "Option::is_none")]
80    pub value: Option<AbstractPropertyValueV0>,
81    pub resolved: bool,
82    #[serde(skip_serializing_if = "Option::is_none")]
83    pub blocked_reason: Option<&'static str>,
84}
85
86#[derive(Debug, Clone, PartialEq, Eq, Serialize)]
87#[serde(rename_all = "camelCase")]
88pub struct CascadeRestrictionCycleSummaryV0 {
89    pub schema_version: &'static str,
90    pub product: &'static str,
91    pub claim_level: &'static str,
92    pub cycle_detection_model: &'static str,
93    pub context_count: usize,
94    pub restriction_map_count: usize,
95    pub cycle_count: usize,
96    pub cycles: Vec<CascadeRestrictionCycleV0>,
97    pub theorem_claimed: bool,
98}
99
100#[derive(Debug, Clone, PartialEq, Eq, PartialOrd, Ord, Serialize)]
101#[serde(rename_all = "camelCase")]
102pub struct CascadeRestrictionCycleV0 {
103    pub path: Vec<String>,
104}
105
106pub fn summarize_cascade_value_family_v0(
107    property_name: impl Into<String>,
108    members: Vec<CascadeValueFamilyMemberV0>,
109    restriction_maps: Vec<CascadeRestrictionMapV0>,
110) -> CascadeValueFamilyV0 {
111    let property_name = property_name.into();
112    let mut members = members;
113    members.sort_by(|left, right| left.context.id.cmp(&right.context.id));
114    members.dedup_by(|left, right| left.context.id == right.context.id);
115
116    let mut restriction_maps = restriction_maps;
117    restriction_maps.sort();
118    restriction_maps.dedup();
119
120    let context_ids = members
121        .iter()
122        .map(|member| member.context.id.as_str())
123        .collect::<BTreeSet<_>>();
124    let property_consistent = members
125        .iter()
126        .all(|member| property_value_name(&member.value) == property_name);
127    let dangling_restriction_count = restriction_maps
128        .iter()
129        .filter(|restriction| {
130            !context_ids.contains(restriction.parent_context_id.as_str())
131                || !context_ids.contains(restriction.child_context_id.as_str())
132        })
133        .count();
134    let restriction_map_count = restriction_maps.len();
135
136    CascadeValueFamilyV0 {
137        schema_version: "0",
138        product: "omena-abstract-value.cascade-value-family",
139        framing: "framingNeutralCascadeFamily",
140        claim_level: ABSTRACT_VALUE_CASCADE_FAMILY_CLAIM_LEVEL_V0,
141        property_name,
142        supported_readings: vec!["presheafCompatible", "cosheafCompatible"],
143        context_value_count: members.len(),
144        restriction_map_count,
145        property_consistent,
146        dangling_restriction_count,
147        theorem_claimed: false,
148        members,
149        restriction_maps,
150    }
151}
152
153pub fn derive_cascade_restriction_maps_v0(
154    members: &[CascadeValueFamilyMemberV0],
155) -> Vec<CascadeRestrictionMapV0> {
156    let context_ids = members
157        .iter()
158        .map(|member| member.context.id.as_str())
159        .collect::<BTreeSet<_>>();
160    let mut maps = members
161        .iter()
162        .filter_map(|member| {
163            let parent_id = member.context.parent_id.as_deref()?;
164            context_ids
165                .contains(parent_id)
166                .then(|| CascadeRestrictionMapV0 {
167                    parent_context_id: parent_id.to_string(),
168                    child_context_id: member.context.id.clone(),
169                    morphism: cascade_context_refinement_morphism_v0(),
170                })
171        })
172        .collect::<Vec<_>>();
173    maps.sort();
174    maps.dedup();
175    maps
176}
177
178pub fn cascade_context_refinement_morphism_v0() -> CascadeMorphismV0 {
179    CascadeMorphismV0 {
180        kind: "contextRefinement",
181        direction: "parentToChildRestriction",
182        preserves_property_name: true,
183        evidence: vec![
184            "contextIndexedValueFamily",
185            "parentChildCascadeContext",
186            "noSheafTheoremClaim",
187        ],
188    }
189}
190
191pub fn cascade_value_for_context<'a>(
192    family: &'a CascadeValueFamilyV0,
193    context_id: &str,
194) -> Option<&'a AbstractPropertyValueV0> {
195    family
196        .members
197        .iter()
198        .find(|member| member.context.id == context_id)
199        .map(|member| &member.value)
200}
201
202pub fn cascade_family_context_values(
203    family: &CascadeValueFamilyV0,
204) -> BTreeMap<String, AbstractPropertyValueV0> {
205    family
206        .members
207        .iter()
208        .map(|member| (member.context.id.clone(), member.value.clone()))
209        .collect()
210}
211
212pub fn evaluate_cascade_stalk_v0(
213    family: &CascadeValueFamilyV0,
214    context_id: &str,
215) -> CascadeStalkEvaluationV0 {
216    let values = cascade_family_context_values(family);
217    let requested_context_exists = values.contains_key(context_id);
218    let parent_by_child = family
219        .restriction_maps
220        .iter()
221        .map(|restriction| {
222            (
223                restriction.child_context_id.clone(),
224                restriction.parent_context_id.clone(),
225            )
226        })
227        .collect::<BTreeMap<_, _>>();
228    let mut restriction_path = Vec::new();
229    let mut current = context_id.to_string();
230    let bound = family.context_value_count.max(1);
231
232    for _ in 0..=bound {
233        restriction_path.push(current.clone());
234        if let Some(value) = values.get(&current)
235            && !property_value_is_bottom(value)
236        {
237            return CascadeStalkEvaluationV0 {
238                schema_version: "0",
239                product: "omena-abstract-value.cascade-stalk-evaluation",
240                claim_level: "fixtureWitnessBoundedCascadeStalkEvaluation",
241                property_name: family.property_name.clone(),
242                requested_context_id: context_id.to_string(),
243                requested_context_exists,
244                resolved_context_id: Some(current),
245                used_restriction_map_count: restriction_path.len().saturating_sub(1),
246                bounded_by_context_count: bound,
247                bounded_resolution_ready: true,
248                theorem_claimed: false,
249                value: Some(value.clone()),
250                resolved: true,
251                blocked_reason: None,
252                restriction_path,
253            };
254        }
255        let Some(parent) = parent_by_child.get(&current) else {
256            break;
257        };
258        current = parent.clone();
259    }
260
261    CascadeStalkEvaluationV0 {
262        schema_version: "0",
263        product: "omena-abstract-value.cascade-stalk-evaluation",
264        claim_level: "fixtureWitnessBoundedCascadeStalkEvaluation",
265        property_name: family.property_name.clone(),
266        requested_context_id: context_id.to_string(),
267        requested_context_exists,
268        resolved_context_id: None,
269        restriction_path,
270        used_restriction_map_count: 0,
271        bounded_by_context_count: bound,
272        bounded_resolution_ready: true,
273        theorem_claimed: false,
274        value: None,
275        resolved: false,
276        blocked_reason: Some("no non-bottom value found along bounded restriction path"),
277    }
278}
279
280pub fn summarize_cascade_restriction_cycles_v0(
281    family: &CascadeValueFamilyV0,
282) -> CascadeRestrictionCycleSummaryV0 {
283    let context_ids = family
284        .members
285        .iter()
286        .map(|member| member.context.id.clone())
287        .collect::<BTreeSet<_>>();
288    let mut adjacency = BTreeMap::<String, Vec<String>>::new();
289    for restriction in &family.restriction_maps {
290        adjacency
291            .entry(restriction.parent_context_id.clone())
292            .or_default()
293            .push(restriction.child_context_id.clone());
294    }
295    for targets in adjacency.values_mut() {
296        targets.sort();
297        targets.dedup();
298    }
299
300    let mut cycles = BTreeSet::<CascadeRestrictionCycleV0>::new();
301    for start in &context_ids {
302        collect_restriction_cycles_from(
303            start,
304            start,
305            &adjacency,
306            &mut Vec::new(),
307            &mut cycles,
308            family.context_value_count.max(1),
309        );
310    }
311    let cycles = cycles.into_iter().collect::<Vec<_>>();
312    CascadeRestrictionCycleSummaryV0 {
313        schema_version: "0",
314        product: "omena-abstract-value.cascade-restriction-cycle-summary",
315        claim_level: "fixtureWitnessBoundedRestrictionCycleDetection",
316        cycle_detection_model: "boundedRestrictionCycleWitnessNotCohomologyTheorem",
317        context_count: family.context_value_count,
318        restriction_map_count: family.restriction_map_count,
319        cycle_count: cycles.len(),
320        cycles,
321        theorem_claimed: false,
322    }
323}
324
325fn collect_restriction_cycles_from(
326    start: &str,
327    current: &str,
328    adjacency: &BTreeMap<String, Vec<String>>,
329    path: &mut Vec<String>,
330    cycles: &mut BTreeSet<CascadeRestrictionCycleV0>,
331    bound: usize,
332) {
333    if path.len() > bound {
334        return;
335    }
336    path.push(current.to_string());
337    if let Some(children) = adjacency.get(current) {
338        for child in children {
339            if child == start && path.len() > 1 {
340                let mut cycle = path.clone();
341                cycle.push(start.to_string());
342                cycles.insert(CascadeRestrictionCycleV0 {
343                    path: canonical_restriction_cycle(cycle),
344                });
345            } else if !path.contains(child) {
346                collect_restriction_cycles_from(start, child, adjacency, path, cycles, bound);
347            }
348        }
349    }
350    path.pop();
351}
352
353fn canonical_restriction_cycle(mut cycle: Vec<String>) -> Vec<String> {
354    if cycle.len() <= 2 {
355        return cycle;
356    }
357    cycle.pop();
358    let Some((start_index, _)) = cycle
359        .iter()
360        .enumerate()
361        .min_by(|left, right| left.1.cmp(right.1))
362    else {
363        return cycle;
364    };
365    let mut canonical = (0..cycle.len())
366        .map(|offset| cycle[(start_index + offset) % cycle.len()].clone())
367        .collect::<Vec<_>>();
368    canonical.push(canonical[0].clone());
369    canonical
370}
371
372fn property_value_is_bottom(value: &AbstractPropertyValueV0) -> bool {
373    matches!(value, AbstractPropertyValueV0::Bottom { .. })
374}
375
376fn property_value_name(value: &AbstractPropertyValueV0) -> &str {
377    match value {
378        AbstractPropertyValueV0::Bottom { property_name }
379        | AbstractPropertyValueV0::Exact { property_name, .. }
380        | AbstractPropertyValueV0::FiniteSet { property_name, .. }
381        | AbstractPropertyValueV0::CustomPropertyReference { property_name, .. }
382        | AbstractPropertyValueV0::Top { property_name } => property_name,
383    }
384}
omena_abstract_value/cascade_family.rs

omena_abstract_value/
cascade_family.rs
