UCF/GUTT™ Organizational Network Analysis (ONA)
See Relationships Mathematically
When the decision matters, the methodology must hold up. UCF/GUTT provides auditable, mathematically grounded relationship analysis — not black-box predictions.
Scope note: 'Formally verified' applies to the audited Coq library artifact only. The Python demo/UI wrappers and any OCaml/Haskell extraction are not audit-covered unless explicitly stated.
Demo mode: Spec-aligned Python reference implementation (not formally verified).
Verified mode (licensed): Coq source + audited verification recipe (AUDIT.md) + semantic coverage map (CLAIMS.md) for v1.6.0 — 21 files, 18,153 lines; zero axioms used by audited exports; zero admitted proofs. The verified claim applies to the Coq library artifact at the tagged commit SHA. (OCaml/Haskell extraction available separately; not covered by this audit.)
Reproduce verification via AUDIT.md; scope is in CLAIMS.md.
What Is This?
This interactive demo lets you explore relational mathematics — a fundamentally different approach to understanding team dynamics, organizational health, and even geopolitical relations.
Traditional tools say "Our AI predicts 73% conflict risk." We say "A mixed-signal relationship is present by mathematical definition (at least one positive channel and at least one negative channel)." Traditional tools use black-box algorithms and heuristics. We use transparent, formally defined predicates; in licensed verified mode, the framework's certified components are backed by machine-checked Coq artifacts and an audit trail (AUDIT.md / CLAIMS.md). They say "Trust our model." We say "Verify the proof yourself."
In the licensed verified artifact, conflict detection isn't a prediction — it's the application of formally defined predicates grounded in the audited Coq library. The demo implements the same specifications; the licensed version provides the mathematical guarantees via the Coq source and audit trail.
Advantages Over Traditional ONA/SNA
Traditional organizational and social network analysis tools rely on heuristics, AI models, and statistical methods. UCF/GUTT takes a fundamentally different approach: deductive predicates backed by machine-verified proofs. Where conventional tools offer probabilistic assessments like "73% conflict risk," UCF/GUTT provides deterministic predicate results with respect to the formal definition and the provided inputs — conflict either EXISTS by mathematical definition, or it doesn't.
This distinction matters for transparency and defensibility. Traditional tools operate as black boxes; you trust their output without understanding the reasoning. UCF/GUTT exposes auditable mathematics traceable directly to Coq proofs. The verification gap is significant: conventional tools typically offer limited formal guarantees, while UCF/GUTT's licensed artifact provides 18,153 lines of a formally verified Coq library, with zero axioms used by audited exports (per Print Assumptions) and zero admitted proofs (per grep scan).
The framework also scales differently. Traditional ONA often struggles beyond team-level analysis, requiring different models at different scales. UCF/GUTT predicates are scale-invariant — the same mathematical definitions that detect conflict between Bob and Carol apply identically to relations between nation-states. This architectural choice, combined with the formal verification foundation, creates a competitive moat estimated at $10–30M and 5+ years to replicate.
What You Can Do
Interactive Team Playground — Work with 5 team members (Alice, Bob, Carol, David, Eve) across 6 relationship channels: Collaboration, Communication, Trust, Influence, Social, and Reporting. Drag sliders from -1 (antagonistic) to +1 (cooperative) and watch conflicts appear and resolve in real-time.
Analysis Views— See team health scores, connectivity metrics, and sentiment balance in the Overview. The Conflicts tab shows automatically detected mixed-signal relationships. The Matrix provides a visual relationship map across all channels. Details lets you deep dive into any pair's relationship profile.
Geopolitical Preview — Explore how the same math applies to international relations with 4 fictional nations across Trade, Military, Diplomatic, Intelligence, Cultural, and Resource channels. The same conflict and harmony predicates work at any scale.
How It Works
Every relationship has multiple dimensions. Bob might collaborate well with Carol (+0.7 collaboration) but not trust her (-0.5 trust). The traditional approach says "It's complicated."
Our approach says conflict(Bob, Carol) = TRUE — because there exists a positive channel (collaboration = +0.7) AND there exists a negative channel (trust = -0.5). This isn't a prediction. It's a definition. In the licensed verified artifact, that definition is grounded in the audited Coq library with certified underlying infrastructure.
Key Predicates: Conflict means mixed signals exist across channels (some positive, some negative). Harmony means all active channels point the same direction. Support means at least one active relationship exists. Seriality means no orphaned entities — everyone is connected to something.
What's certified in Coq: The underlying relational infrastructure — weighted relations (type, support, magnitude, composition rules), number systems, categorical structure, and core propositions including universal connectivity (seriality). The conflict/harmony predicates in the demo are spec-defined; the licensed mode provides the Coq source with this certified infrastructure and the audit trail to verify it. If/when conflict/harmony are certified as explicit Coq objects, CLAIMS.md will list their theorem names.
Real-World Deployment
The demo shows interactive exploration; production deployment follows a straightforward workflow:
Collect — Gather multi-channel relationship data via pulse surveys, HRIS exports, 360-review instruments, or manual entry. Each channel (Collaboration, Trust, etc.) maps to a [-1, +1] intensity score per directed pair.
Analyze — Load data (CSV/JSON) into the licensed tool. The engine applies formally defined predicates to detect conflicts, measure harmony, and compute aggregate health metrics.
Report — Generate verified analysis reports (see sample PDF in Downloads). Results include conflict inventory, severity rankings, and prioritized recommendations.
Iterate — Track relationship evolution over time with temporal snapshots (licensed feature). Measure intervention effectiveness with before/after comparisons.
Integrate — API bindings available for programmatic access. Custom adapters for Slack, Teams, Workday, or proprietary systems scoped in Enterprise tier.
What the Demo Does NOT Include
Important: This is a capability preview. The demo uses simplified Python implementations that follow the formal specifications.
Included in the demo: Basic conflict and harmony detection, interactive visualization, team and geopolitical playgrounds.
NOT included in demo (requires license): The Coq source code (18,153 lines), OCaml extraction, Nested Relational Tensors (NRT), Dimensional Sphere of Relation (DSoR), temporal evolution tracking, scenario modeling, cascade effect simulation, commercial use rights, and the ability to claim "formally verified" status (per AUDIT.md).
The key difference: In demo mode, our Python code follows the formal specification. In licensed mode, you get the audited Coq source (18,153 lines, machine-verified) plus the verification recipe to confirm it yourself. For evaluation and learning, the demo is perfect. For production use, you need the licensed version to get mathematical guarantees of correctness, audit trails to formal proofs, and defense against "how do you know it's right?" questions. (Extraction to OCaml/Haskell is available but not covered by the current audit.)
Who Is This For?
Organizational Development — Map team dynamics with mathematical precision. Identify hidden conflicts before they escalate. Track relationship health over time with the licensed version.
HR and People Analytics — Evidence-based conflict detection with defensible methodology for sensitive decisions. Integration with existing HRIS available with licensing.
Management Consulting — Differentiate with formally verified analysis. Provide clients with mathematically grounded insights. White-label licensing available.
Research and Academia — Rigorous methodology for organizational studies with reproducible, formally defined metrics. Citation-ready: zero axioms used by audited exports, zero admits, machine-verified.
Government and Intelligence — Geopolitical relationship modeling, alliance and rivalry network analysis, stability assessment with formal guarantees.
What "Formally Verified" Means
The UCF/GUTT Coq library (v1.6.0) contains 18,153 lines of Coq source (definitions + theorems + proofs). The verification claims are precise:
- Zero axioms used by audited exports (per Print Assumptions — 183+ checks return "Closed under the global context")
- Zero project-defined axioms or parameters (per grep scan)
- Zero admitted proofs (per grep scan)
- Kernel checked (coqchk) on core modules
- Axiom-bearing stdlib modules excluded: Classical, Choice, FunctionalExtensionality, ProofIrrelevance, axiomatic Reals not imported
The Coq proofs provide logical consistency (definitions don't contradict each other) and auditability (anyone can verify the proofs themselves via the 6-command recipe in AUDIT.md). When executable code is extracted from Coq definitions, you get a strong correspondence between spec and implementation; the v1.6.0 audit covers compilation, assumption closure, and kernel checking of the Coq artifact.
Other tools can claim to detect conflict. UCF/GUTT can uniquely back this release with machine-verified Coq foundations and an audit trail for the library artifact; where a predicate is certified, its exact Coq object is listed in CLAIMS.md. "Here is the mathematical definition. Here is the recipe to verify it yourself (AUDIT.md). Here is the explicit semantic coverage map (CLAIMS.md)."
Why "Zero Axioms" Is Difficult
The strict adherence to constructive logic — rejecting the Law of Excluded Middle, Axiom of Choice, and axiomatic real numbers — forces a fundamentally harder engineering approach. Most formal verification projects accept axioms for expedience; refusing them means every proof must be algorithmically executable.
Why this is rare: Achieving fully axiom-free foundations in constructive logic for real-world constructs—safe division, constructive reals, geometric relational structures—is exceptionally rare in applied settings. Even prominent high-assurance verified systems (e.g., in avionics and cryptography) typically accept axioms for practicality; well-regarded efforts like CompCert (verified compiler), seL4 (microkernel), and Amazon's s2n (TLS implementation) include axiomatic or classical foundations. The strict constructive discipline significantly increases proof difficulty but provides stronger guarantees: every result is algorithmically executable with constructive witnesses, not just logically consistent under classical assumptions.
Constructive Reals vs. Axiomatic Reals: Standard libraries simply assert that real numbers exist. The UCF/GUTT foundation builds them. The certified R_cauchy type (CLAIMS.md) implements real numbers as Cauchy sequences of rationals. Every arithmetic operation carries constructive convergence guarantees — no appeals to completeness axioms.
Division by Zero: Handling mathematical singularities without axioms is a stress test. The certified Q_safe_div (CLAIMS.md) handles division by zero through boundary markers rather than axioms or runtime crashes — turning what would normally require special pleading into a well-defined relational transition.
Dimensional Sphere of Relation (DSoR): The certified DSoR type (Proposition 2 in CLAIMS.md) provides geometric structure constructed from relational intensity rather than assumed Cartesian coordinates. This is the foundation for representing relations as points on multi-dimensional spheres.
Why this matters for replication: A competitor can't simply "code faster." They must solve the same foundational problems — building real numbers constructively, handling singularities without axioms, and maintaining logical coherence across domains. The $10–30M estimate prices the theoretical work, not just the typing.
What "Artifact-Grade Packaging" Means
The UCF/GUTT library follows artifact-grade packaging practices — the standards used at peer-reviewed formal methods venues (POPL, PLDI, CAV, ITP) for reproducible verification artifacts.
This means:
Reproducible builds: An evaluator with no prior relationship to the project can download the source, follow documented instructions, and rebuild everything from scratch. Toolchain versions are pinned (Coq 8.18–8.20, OCaml 4.14.1). A canonical 6-command verification recipe is provided in AUDIT.md.
Structured library release: The 21 source files follow a layered dependency architecture. Public APIs are marked stable with semantic versioning. The library compiles with standard Coq tooling. (Extraction to OCaml available; not covered by current audit.)
Explicit semantic coverage: CLAIMS.md maps each informal claim to specific Coq theorem names with verification status. Currently certified: 5 of 52 core propositions plus 9 infrastructure components (number systems, weighted relations, categorical structure) = 14 certified items total. We're explicit about what's proven and what's not.
The practical consequence is trust. When someone asks "how do you know this is correct?", we point to machine-checked proofs that compile, verification commands anyone can run, and documentation that specifies exactly what those proofs establish.
Cost to Replicate (estimated): $10–30M and 5+ Years
Personnel (the big cost driver):
- Senior formal verification engineers: $250-400K/year fully loaded
- Coq engineers with deep library-building and audit discipline are scarce
- You'd need 3-5 of them working for several years
- Plus domain experts (relational ontology isn't standard curriculum)
Timeline reality:
- Learning Coq to proficiency: 1-2 years for an experienced mathematician
- Developing novel proof strategies (not just verifying known theorems): iterative, unpredictable
- The "zero axioms" constraint is punishing — many formal projects accept axioms for expedience; refusing them dramatically increases difficulty
What they'd actually be replicating:
- Not just 18,153 lines of code — the conceptual framework itself
- Novel definitions and certified infrastructure (DSoR, weighted relations, constructive number systems)
- Advanced structures like Nested Relational Tensors (NRT) for multi-scale modeling
- Cross-domain coherence (the same framework spanning organizational dynamics and number theory)
Back-of-envelope:
- 4 senior engineers × $350K × 5 years = $7M labor alone
- Add management, infrastructure, iteration dead-ends, domain consulting
- $10-30M becomes defensible as a range
The honest framing: "This is what it would cost a well-funded team starting from scratch to reach equivalent verified foundations." This estimate prices the invention of the theory and the solving of foundational problems (constructive reals, singularity handling, relational geometry), not just the typing of code. Actual costs vary by scope and constraints.
Licensing
The Demo tier is free for evaluation — explore the approach, test fit, and understand the concepts.
For production use, licensing scales with your organization size and deployment needs:
Startup ($8,000–$15,000/year): For companies with <$5M annual revenue (or pre-revenue). Includes complete Coq source (18,153 lines), OCaml extraction (available, not audit-covered), and technical support (integration guidance and build assistance).
Enterprise ($50,000–$120,000/year): For companies with $5M–$500M annual revenue (or ≥50 employees). Unlimited internal deployment with no seat restrictions. Includes training (up to 40 hours), priority support, and scoped custom development to adapt the framework to your domain models. Pilot engagements available for proof-of-concept evaluation.
OEM ($150,000+/year or revenue share): For companies with >$500M annual revenue, or those embedding UCF/GUTT into a commercial product distributed to third parties (SaaS, on-prem, OEM bundles, or white-label). Includes redistribution rights and negotiated terms based on deployment scale.
Government & Research: Academic licensing starts at $3,000/year for non-commercial research with publication rights. Government and defense contracts are negotiated for compliance and procurement requirements — typically $75,000–$250,000 depending on scope.
All paid tiers include the right to represent the licensed-mode implementation as formally verified when deploying the audited Coq library (i.e., the audited Coq library artifact itself; any non-extracted wrappers such as Python/Streamlit interfaces are not covered by the audit unless separately verified). This capability typically requires multi-year, multi-million-dollar investment and specialized expertise to reproduce independently.
Contact & Next Steps
Michael_Fill@protonmail.com
Happy to discuss verification scope or audit process pre-license under NDA.
Pilot programs available — typical scope: single team (5–20 people), 2–4 week turnaround, $5,000 fixed fee (credited toward annual license if signed within 90 days). Defensible, auditable methodology that holds up under scrutiny — when the decision matters.
What you get with a license:
- Complete Coq source code (audited per AUDIT.md)
- OCaml extraction (available, not audit-covered)
- Advanced structures (NRT, DSoR, temporal evolution, scenario modeling, cascade simulation)
- Commercial use rights
- Technical support and integration guidance
- AUDIT.md / CLAIMS.md documentation
FAQ
"Can I just copy the demo code?" — Yes, but it won't give you the guarantees. The demo logic is intentionally simple (has_positive AND has_negative). The value is the audited Coq library artifact, reproducible verification (AUDIT.md), and explicit semantic scope (CLAIMS.md). Where a predicate is certified, CLAIMS.md lists the exact Coq object.
"What if I reverse-engineer the algorithms?" — There's nothing to reverse-engineer at the demo level — the predicates are intentionally transparent. The IP is the formalized framework plus an audited Coq artifact and coverage map; competitors would need to reproduce the same verified foundations and documented scope.
"Why should I pay for something this simple?" — You're not paying for the simple predicates. You're paying for the audited Coq library artifact that grounds those predicates, an audit trail to formal proofs (AUDIT.md), explicit semantic scope (CLAIMS.md), advanced capabilities (NRT, temporal, scenarios) that aren't simple, commercial rights to use and claim verification, and a competitive moat your competitors can't easily replicate.
"Is the math real or marketing?" — The math is real. The Coq proofs compile. Zero axioms used by audited exports, zero admits. You can verify this yourself with the licensed version using the 6-command recipe in AUDIT.md. This isn't "AI-powered" hand-waving — it's computer-verified mathematics that either compiles or it doesn't.
"How is this different from social network analysis tools?" — Traditional SNA tools use heuristics and statistical methods. They tell you "this relationship looks like it might have tension." UCF/GUTT uses formal mathematics. It tells you "this relationship satisfies the formal definition of conflict or harmony" — and in the licensed version, the framework's certified components are traceable via CLAIMS.md. The difference is deterministic definitions versus probabilistic estimates.
"Can this really apply to geopolitics?" — Yes. The same mathematical framework works at any scale. A "conflict" between Bob and Carol (positive collaboration, negative trust) is structurally identical to a "conflict" between Nation A and Nation B (positive trade, negative military). The predicates are scale-invariant. The licensed version includes Nested Relational Tensors for modeling complex multi-level systems.
"What exactly has been proven?" — CLAIMS.md maps every informal claim to specific Coq theorem names with verification status. Currently: 5 of 52 core propositions certified (universal connectivity, DSoR, graph representation, composition, direction), plus 9 infrastructure components — Relational Math (ℕ, ℤ, ℚ, ℝ, irrationals, division, clock hierarchy, weighted relations, adjunction) = 14 certified items total. We're explicit about what's proven and what's still in progress.
Download and Run
Download the interactive demo and run it locally. You need Python 3.8+ and Streamlit. Install with pip install streamlit pandas, then navigate to the ucf_gutt_demo_enhanced folder and run streamlit run app.py.
© 2023-2026 Michael Fillippini. All Rights Reserved.
UCF/GUTT™ — Unified Conceptual Framework / Grand Unified Tensor Theory
"Relations are not connections between pre-existing entities. Relations are the fundamental fabric from which entities emerge."